KRust:Rust形式化可执行语义

• 作者: 张俊 王丰
• 来源期刊: 计算机科学与探索
• 学科: 工学
• 关键词: 编程语言 Rust 语义 K框架
• 年，卷（期）: 2019,（12）
• 所属期刊栏目: 学术研究
• 页码范围: 2008-2014
• 页数: 7页
• 分类号: TP312
• 字数: 5831字
• 语种: 中文
• DOI: 10.3778/j.issn.1673-9418.1901029

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王丰	中国科学院上海微系统与信息技术研究所	6	23	3.0	4.0
7	张俊	中国科学院上海微系统与信息技术研究所	74	745	15.0	26.0