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

摘要： Rust是新兴的系统级编程语言，旨在提供内存安全的同时保证极高的性能。Rust形式化语义是用来证明其内存安全和开发Rust程序分析工具的基础。鉴于目前没有直接描述Rust的形式化语义，提出了针对Rust语言的形式化可执行语义KRust。为了确保语义的可执行性和应用性，使用了K框架进行语义的开发。KRust目前涵盖了Rust常见的语法和语义，包括了Rust的3个核心特性：所有权、借用和生命周期。KRust通过了191个测试样例，其中157个都是来自Rust官方的测试集。语义对比测试实验发现了Rust编译器的缺陷。此外，KRust的语义还可以被应用于开发Rust程序分析工具。

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