KRust:Rust形式化可执行语义

摘要：

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

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

所属期刊栏目：13

分类号：TP312(计算技术、计算机技术)

资助基金：The National Natural Science Foundation of China under Grant Nos.61532019,61761136011

在线出版日期：2019-12-26（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：2008-2014