开题报告

一、选题的背景及意义

Rust是一种新的系统级编程语言，第一个正式版本于2015年5月发布，它有三大特点：运行快，防止段错误，保证线程安全[1]。Rust目前已被用于实现操作系统[2]，并行浏览器引擎[3]，英特尔SGX Enclave[4]等。在传统的系统级编程语言（C/C ）的开发过程中，经常出现因为各种内存错误引起的崩溃或bug，比如空指针、野指针、内存泄漏、内存越界、段错误、数据竞争、迭代器失效等，C/C 对静态检查不友好，只能查出一部分问题，事后debug解决问题的代价过高。鉴于此，先辈们发明了一种自动垃圾回收机制(Garbage Collection)，程序员们在大多数情况下不用再操心内存释放的问题，但到目前为止，不管使用哪种算法的GC系统，在性能上都要付出较大的代价。Rust对自己的定位是接近芯片硬件的系统级编程语言，Rust可以保证内存安全，这是它自己独有的优势。Rust很好地支持了并发编程，在编译阶段就将数据竞争解决在了萌芽状态，保障了线程安全；Rust还摒弃了手动内存管理带来的各种不安全的弊端，同时也避免了自动垃圾回收带来的效率损失和不可控性，执行效率上可与C语言相媲美，且具备很好的跨平台性。概括地说，Rust与C和C 的定位类似，但是增加了安全性。

Rust实现上述承诺的关键是其特有的所有权、移动语义、借用和生命周期机制。对象的所有权是对变量的绑定。当变量生命周期结束时，Rust将释放其拥有的资源。也可以移动对象的所有权，之后就无法通过过期的所有者访问该对象。这可确保任何对象同一时间只有一个绑定。有时，Rust提供借用，允许多个引用共享一个对象。Rust中有两种借用：可变引用和不可变引用。可变引用可对引用对象的值进行修改，不可变引用则不行。Rust强制执行的基本所有权纪律是说“共享不可变，可变不共享”。此属性消除了各种常见的低级编程错误，例如释放后使用，数据竞争和迭代器失效。这些特定的语义规则是不寻常的，因此其它现代编程语言（如C / C ，Java和Javascript）的语义不能直接适用于Rust。

Isabelle是一种通用的定理证明器,它为证明系统的开发提供了一个通用框架[5]。Isabelle使用自然演绎规则来进行定理证明，它支持对数学公式的形式化描述,并为这些公式的逻辑演算提供了证明工具。一方面,它可以作为快速原型推理系统的通用框架;另一方面,它所支持的对象逻辑,为用户提供了一个良好的定理证明环境。与其它的定理证明辅助工具相比,Isabelle逻辑系统的特点突出表现在以下两个方面:

1 支持多种对象逻辑，包括直觉主义一阶逻辑(IFOL),建设性类型理论(CTT),高阶逻辑 (HOL),基于序列演算的一阶逻辑(LK)和模态逻辑等。

2 支持定义新逻辑，通过在Isabelle系统中定义对象逻辑具体和抽象的句法以及推理规则,我们就可以实现一个新的逻辑系统。

Isabelle/HOL即Isabelle for HOL[6]，HOL是Higher-Order Logic的简称，是一种高阶逻辑，也是Isabelle中的一门函数式编程语言。Isabelle/HOL已经应用在定理证明、语义定义[18]、OS内核硬件抽象模型[7]、操作系统形式化验证方法[8]等多个领域。

本课题拟在Isabelle/HOL环境中，采用数理逻辑定义Rust语言较精确的语法和语义，即构造Rust的形式化模型，实现对Rust的可信编译，并将其作为以形式化方法推理Rust程序和开发相关计算机辅助工具的基础。