SPARK：计算机编程语言Ada的演绎验证工具

SPARK既是语言的演绎验证工具，也是它所操作的Ada的子集。编程语言火花被设计为适合形式验证，最有影响力的设计选择之一是排除混叠。虽然这种选择大大简化了工具设计并提高了预期的校对性能，但这也意味着指针作为混叠的主要来源被排除在语言之外。虽然 SPARK 多年来已经添加了许多语言功能，但不违反非别名属性，添加指针似乎是不可能的。

Ada是一种通用的过程编程语言。Ada 语言的设计非常强调程序的安全性和正确性。此目标是通过使用可读语法来实现的，该语法在合理的情况下使用关键字而不是符号。类型系统强大而严格，编译器可以静态检测到许多潜在的类型约束冲突。如果没有，则会在程序中插入运行时检查，以确保检测到不正确的情况。

Ada 2012 向 Ada 引入了基于合约的编程。特别是，可以将前置条件和后置条件附加到子程序，这些条件可以在程序执行期间检查，就像断言一样。

SPARK 是为 Ada 提供形式验证的工具的名称。它使用用户提供的协定，并尝试证明运行时检查不会失败，并且后置条件由相应的子程序建立。由于整个 Ada 语言的形式验证将很棘手，SPARK 也是 SPARK 工具支持的 Ada 语言子集的名称。

此子集几乎包含 Ada 的所有功能，尽管有时以受限的形式出现。特别是，表达式应该没有副作用，并且禁止混叠（任何两个变量都不应共享相同的内存位置或在内存中重叠）。此限制大大简化了 SPARK 工具中使用的内存模型：任何程序变量都可以独立于其他变量进行推理。

Ada 中的指针称为访问类型。可以使用访问关键字声明访问类型。如果未提供初始值，则访问类型的对象为 null。可以使用关键字 new 在堆上分配对象。可以为分配的对象提供初始值。指针的取消引用被写为记录组件访问。

但使用关键字 all取消引用指针时，会引入运行时检查以确保它不为 null。Ada 不强制要求垃圾回收。用户可以使用名为 Unchecked_Deallocation 的泛型函数手动回收堆上分配的内存，该函数还将其参数指针设置为 null。

为了支持 SPARK 中的指针，我们设计了 Ada 访问类型的子集，它不会引入混叠并避免一些特定于指针的问题，同时保留尽可能多的表现力。我们选择的第一个限制是排除常规访问类型。

这意味着 SPARK 只能创建指针，指定在堆上分配的内存，而不是堆栈上的内存。因此，指针只能通过显式释放来使指针无效，并且有效指针的释放始终是合法的。为了消除（堆）指针之间的混叠，受 Rust 启发的所有权规则已添加到 Ada 的合法性规则之上。这些规则强制实施单个写入器/多个读取器策略。它们确保在修改指针指定的值时，可以将所有其他对象视为保留。

SPARK 所有权策略的基础是赋值的移动语义。将指针分配给变量时，赋值的源和目标都指定相同的内存区域：分配包含指针的对象会创建别名。为了缓解此问题，当分配包含指针的对象时，指针指定的内存区域被称为移动。赋值的源将失去指定数据的所有权，而赋值的目标将获得该数据。所有权系统确保不会通过分配源再次访问指定的数据。

指针在 SPARK 证明工具的验证模型中处理，或者选项类型：访问对象为 null，或者它们包含值。此外，访问对象还包含一个地址，该地址可用于处理比较（即使两个指针指定的值相等，它们也可能不相等）。取消引用指针时，将生成验证条件以确保指针不为 null，以便可以访问其值。

在 Ada 中，递归性只能通过指针引入。这个想法是首先声明一个类型，但不给出它的定义。此声明称为不完整声明，它为类型引入了一个占位符，该占位符只能在受限的情况下使用。特别是，此占位符可用于声明指定指向此类型值的指针的访问类型。使用此机制，可以声明递归数据结构，因为访问类型可以在之后的类型定义中使用。

Matsushita 等人提议将 Rust 程序翻译成 CHC。就像我们的方法一样，所有权政策施加的限制是其方法合理性的关键。然而，虽然我们引入了借用关系的概念以便能够使用标准的 WP 微积分，但他们提出了一个专门为 Rust 引用量身定制的新微积分。

SPARK 语言和工具集的最新扩展，以支持指针基于强制实施非锯齿的所有权策略。为了支持基于指针的递归数据结构，SPARK 中通过本地借用器引入了一种受限形式的别名，可用于以命令式方式遍历链接的数据结构。

至于未来的工作，我们希望扩展 SPARK 中支持的 Ada 指针子集。特别是，我们想引入用于模型回调的函数指针，指向具有更宽松所有权策略的常量的指针，以及堆栈上分配的对象的本地借用。