KRust: A Formal Executable Semantics of Rust

摘要: Rust is a new and promising high-level system programming language. It provides both memory safety thread through its novel mechanisms such as ownership, moves borrows. Ownership ensures that at any point there only one owner of given resource. The ownership resource can be moved or borrowed according to the lifetimes. establishes clear lifetime for each value hence does not necessarily need garbage collection. These features bring high performance, fine-grained low-level control over without collection, which differentiate from other existing prevalent languages. For formal analysis programs helping programmers learn features, semantics desired useful fundament developing related tools. In this paper, we present executable operational subset Rust, called KRust. defined in K, rewriting-based semantic framework yields automatically interpreter verification tools programs. KRust has been validated by testing with 182 tests, including 157 tests official