计算机科学与探索

作者：王丰，张俊

单位：1.中国科学院 上海微系统与信息技术研究所，上海 2000502.上海科技大学 信息科学与技术学院，上海 2012103.中国科学院大学，北京 100049

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

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

来源：2019年第12期

《计算机科学与探索》期刊编辑部

查看计算机科学与探索杂志2019年第12期