摘要：Rust是新興的系統(tǒng)級(jí)編程語言,旨在提供內(nèi)存安全的同時(shí)保證極高的性能。Rust形式化語義是用來證明其內(nèi)存安全和開發(fā)Rust程序分析工具的基礎(chǔ)。鑒于目前沒有直接描述Rust的形式化語義,提出了針對(duì)Rust語言的形式化可執(zhí)行語義KRust。為了確保語義的可執(zhí)行性和應(yīng)用性,使用了K框架進(jìn)行語義的開發(fā)。KRust目前涵蓋了Rust常見的語法和語義,包括了Rust的3個(gè)核心特性:所有權(quán)、借用和生命周期。KRust通過了191個(gè)測試樣例,其中157個(gè)都是來自Rust官方的測試集。語義對(duì)比測試實(shí)驗(yàn)發(fā)現(xiàn)了Rust編譯器的缺陷。此外,KRust的語義還可以被應(yīng)用于開發(fā)Rust程序分析工具。