KRust:Rust形式化可执行语义

Journal of Frontiers of Computer Science & Technology（2019）

引用 7|浏览7

暂无评分

摘要

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

查看译文

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要