Page 190 - 《软件学报》2025年第8期

张卓若 等: 面向 Rust 语言的形式化验证方法研究综述 3613

RustBelt 提出生命周期逻辑 (lifetime logic), 其支持很多 NLL 的示例, 但和 NLL 借用检查规则有所不同, 例
如, 其对共享引用的处理更加严格.

3.1 Rust 类型系统
类型系统 [27] 是编程语言设计中的一个基础性概念, 它为程序中的数据提供了一种结构化的规范, 确保了数据
操作的合理性和安全性. 在类型理论的框架下, 类型系统不仅定义了数据的静态结构, 还规定了数据在程序执行过
程中的动态行为. 一个成熟且严谨的类型系统能够有效地预防诸如类型错误、内存泄漏、数组越界等常见的编程
错误, 从而提高软件的可靠性和稳定性. 线性类型 (linear types) 和仿射类型 (affine types) 是编程语言理论中的概
念, 它们在类型系统中引入了严格的约束. 线性类型系统强制要求每个资源只能被使用一次, 而仿射类型则进一步
放宽了这一限制, 允许资源可以被使用一次或不被使用, 即允许资源在没有被使用的情况下可以安全地存在. 它们
都规定一个值只能拥有一个所有者, 并且在所有者超出作用域时, 该值会被自动释放. 这样的设计宗旨在于确保资
源在编译时得到安全和高效的管理, 预防内存双重释放、使用未初始化变量等常见错误. 这些概念在函数式编程
语言中得到了广泛应用, 它们通过限制变量的使用次数来增强程序的表达能力, 同时保持了程序的安全性.
类型检查是类型系统的核心机制之一, 它在编译阶段对程序代码进行分析, 负责确保程序的类型安全. 类型安
全是指程序在运行时不会出现违反类型规则的错误, 例如尝试将一个整数与字符串相加, 或者访问一个空指针. 类
型检查通过静态分析源代码来预防这类错误, 从而避免了潜在的运行时异常或安全漏洞. 在类型检查过程中, 编译
器会遍历程序的每个表达式, 验证其中的变量和操作是否符合它们的声明类型. 这包括检查变量的声明和使用是
否一致, 确保函数调用时提供的参数类型与函数签名中定义的参数类型相匹配, 以及确保返回值的类型与预期的
返回类型相符. 类型检查还涉及更复杂的场景, 如类型转换、类型推断 (type inference) 和泛型编程中的类型约束.
类型推断即通过类型系统中定义的类型规则 (typing rules) 推测出某表达式的类型. 在许多编程语言中, 编译器能
够根据上下文自动推断出变量的类型, 减少了程序员显式声明类型的需要. 这种类型推断不仅简化了代码的编写,
而且有助于提高代码的可读性和可维护性, 同时也减少了因类型声明错误而导致的编译错误. 此外, 类型检查还与
程序的优化紧密相关. 编译器利用类型信息来优化程序的执行效率, 例如通过消除冗余的类型转换, 或者应用特定
类型的高效算法实现. 在某些情况下, 类型检查还能够揭示程序中的潜在性能瓶颈, 指导程序员进行代码优化. 总
之, 类型检查为程序的正确性、安全性和性能提供了坚实的保障. 通过类型检查, 程序员可以在编写代码时获得即
时的反馈, 提高了开发效率和代码质量.
Rust 类型系统是该语言的核心特性之一, 以其独特的设计和对安全性的强调而著称. Rust 语言并未直接采用
线性类型或仿射类型的概念, 而是通过所有权和借用规则隐式达成了相似的编程目标, 为程序员提供了一种在编
译时确保内存安全的方法. Rust 的所有权模型规定, 一个值在任何时候只能有一个所有者, 这个所有者负责管理该
值的生命周期. 借用机制则允许在不转移所有权的情况下临时访问数据, 并通过借用规则保证该访问不会引发数
据竞争和悬挂指针等问题. 在 Rust 中, 类型检查过程可以划分为两个阶段: 首先是传统的类型检查, 确保代码符合
基本的类型安全规则; 其次是借用检查器的借用检查, 这一独特的机制确保程序符合所有权模型的规定和借用检
查规则, 为数据的访问和修改提供了精细的控制. 这两个阶段的结合构成了 Rust 类型系统的基础, 有效预防了诸
如使用后释放、双重释放以及数据竞争等普遍存在的编程错误, 保障了 Rust 代码的内存安全性, 同时避免了对垃
圾收集器的依赖. Rust 类型系统的另一个显著特点是其对泛型 (generics) 和特质 (traits) 的支持. 泛型允许程序员
编写与特定数据类型无关的通用代码, 而 traits 则定义了一组行为的契约, 确保了类型的多态性和可替换性. 这些
特性使得 Rust 的类型系统不仅在安全性上表现出色, 而且在表达力上也具有显著优势.

3.2 基于类型系统的 Rust 语义研究
随着 Rust 语言的蓬勃发展和其在实际应用中的深入实践, 其核心的类型系统也在持续地演进与完善. 在传
统的形式化研究中, 类型系统的可靠性往往通过证明其进展 (progress) 和保持 (preservation) 性质来确立, 即语
法类型良好 (well-typed) 的程序不会陷入无法继续执行的僵局. 该方法称之为语法类型可靠性 (syntactic type
soundness). 然而, 这种类型系统证明的标准方法不容易扩展到混合安全和 unsafe 代码的情况, 因为不安全的代码