关键词: 编程语言, Rust, 语义, K框架

Abstract: Rust is a promising high-level system programming language, aiming at achieving memory safety while maintaining high performance. A formal semantics for Rust is the first step to prove memory safety and develop formal analysis tools for Rust. Since there is no formal semantics describing the exact behavior of Rust, this paper presents the first formal executable operational semantics for Rust, called KRust. KRust is implemented using K framework to make sure the semantics is both executable and applicable. Currently, KRust covers common syntax and semantics of Rust, including 3 core features of Rust: ownership, borrowing and lifetime. KRust has been validated by testing with 191 tests, including 157 tests from the official Rust test suite. The conformance test for semantics shows a bug of Rust compiler. In addition, KRust can be further exploited to construct formal analysis tools of Rust.

Key words: programming language, Rust, semantics, K framework