选择正确的Ada子集以获得强大的静态保证

　　虽然 Ada 提供了许多在运行时充当安全防护的功能，但在检测到违规时会引发异常，但其中一些功能可能过于复杂，无法保证在程序运行之前安全执行。例如指针就是这种情况，指针可用于在内存中创建任意复杂的共享数据结构。SPARK 是 Ada 的一个子集，它禁止这些功能，最明显的是指针，以便能够在编译时提供强有力的保证。SPARK的下一个修订版SPARK 2014的预览版以及相关的验证工具已经可用。

　　尽管SPARK的演进一直伴随着Ada的演进，每个新版本的Ada（SPARK 83，SPARK 95，SPARK 2005）都有一个新版本的SPARK，但新版本SPARK 2014在许多方面都有很大的不同。SPARK 2014 是 2010年启动的一个项目的结果，该项目旨在使使用形式验证而不是测试关键软件具有成本效益。就在几个月前，空中客车公司提出了采用正式方法的五个“必备”标准：健全性，代码的适用性，“普通”工程师在“普通”计算机上的可用性，对经典方法的改进，可认证性。在这三年中，我们非常牢记这五个标准，以下是SPARK 2014和相关验证工具GNATprove的结果。

　　稳健：

　　这是语言和工具的基石。它不仅限于说：“我们使用霍尔逻辑”。我们想要实现的是“最大”的健全性：当你适当地使用它们时，不仅工具不能陈述错误的属性，而且通过滥用工具（例如通过陈述错误的公理）来获得对软件的错误信心也不容易。为了确保最大的合理性，采取了许多决定，例如禁止用户陈述公理。

　　对代码的适用性：

　　SPARK 2014 是 Ada 的最大可能子集，它仍然可以进行形式验证。特别是，它包括泛型、标记类型、判别器、动态类型、早期回报以及 SPARK 2005 中排除的许多其他功能。对于代码中无法正式分析的部分，我们已经可以将形式验证与测试结合起来。因此，它不是一种全有或全无的技术，而是您可以在任何Ada项目中真正引入的技术。

　　普通工程师的可用性：

　　这是这些年来让我们最忙的问题。首先，我们已经实现了自动化水平，大多数证明都是自动通过的，特别是没有运行时错误的证明。其次，我们将工具紧密集成到开发人员工作流（例如，通过使用项目文件和自动计算的依赖项）和开发环境（例如，在特定子程序或代码行上运行GNATprove 的能力，以及显示有问题的程序路径）。

　　改进测试：

　　形式验证是详尽无遗的，这一事实使其成为关键软件所要求的昂贵单元测试活动的理想替代品。这方面的主要挑战是促进逐步采用正式核查。由于形式验证所需的子程序合同对于测试已经很有用，并且由于GNATproly可以单独应用于任何Ada程序中的各个SPARK子程序，因此切换到形式验证可以在几天内完成。

　　可认证性：

　　当我们开始这个项目时，航空电子标准DO-178的正式方法补充尚未最终确定。从那时起，它与新版本的标准DO-178C一起发布，因此今天，GNATprove 可以用于代替在最高级别A或B开发的平面中测试关键嵌入式程序。我们在IEEE软件上发表了一篇关于如何处理在这种情况下覆盖的微妙问题的论文。当然，已经认可形式化方法的其他领域的项目（例如铁路）也可以使用GNATprove。

　　该项目开发的工业案例研究的结果是公开的，供其他人了解新技术擅长什么以及当前发展阶段。当用户从以前的SPARK技术切换到新的SPARK 2014技术时，最常见的评论可能是执行规范的能力提供了令人难以置信的可用性改进。这种动态技术和静态技术的结合对于软件验证的未来无疑是有希望的。

　　审核编辑：郭婷