使用SPARK和Ada进行代码清理

您能以多快的速度将软件推出并准备好？

长期以来，这个单一的问题推动了大部分嵌入式工业行业。按时发布此年度版本，满足该功能里程碑。只要软件功能相对简单或次于系统功能，就可以了。

但随着系统复杂性和互连性的日益增加，曾经是良性的小故障或“故障”现在正在造成威胁，有时甚至危及人的生命。无人机、自动驾驶汽车和医疗设备是这一趋势的三个非常重要的代表。那么问题就不再是软件能否按时交付，而是正确、安全、可靠的软件能否及时交付。这是一个完全不同的野兽。

除了验证它正在做它应该做的事情之外，没有太多可以做的事情来交付正确的软件。不幸的是，传统的软件开发方法并不是为了简化正式规范或优化验证成本而设计的。而且越晚检测到问题，修复的成本就越高，以至于在第一天需要几分钟才能解决的问题可能会在集成过程中持续数月。是的，使用传统语言和环境编写极其强大的软件是可能的，但成本高得离谱。

特别是对于在微控制器 （MCU） 上运行的嵌入式应用程序，一个更加复杂的因素是编写测试的难度。当涉及低级嵌入式功能时，编写甚至运行广泛的测试活动可能是不切实际的。任何可以在这些程序之前帮助清除问题或确保正确性的东西都可以节省大量成本。

另一方面，从一开始就利用表达性和正式的规范，使实施者更容易尊重需求，提供自动验证，从而防止问题或在开发周期的早期发现问题。

Ada 和 SPARK 语言在这方面提供了独特的解决方案，将规范、编码和验证集成到一个通用的形式中。这些语言的核心原则是在软件级别尽可能多地指定，以便在实现时可以验证尽可能多的组件。

下面逐步检查实际的 Ada 或 SPARK 实现。

规格

在将 Ada 和 SPARK 语言与替代语言进行比较时，突出的一件事是可以添加到软件源代码中以捕获除实际功能之外的约束和意图的信息量。数据类型不仅仅是一个整数或浮点数：它是一个语义实体，可以与一组有效值、一组操作、最小精度、内存表示，甚至物理维度相关联。同样，函数不仅仅是一种从参数计算值的方法：它有一组可以调用的条件，在它返回时提供一组保证，并对它的环境（参数和全局变量）产生影响）。

Ada 和 SPARK 有很多特性可以用来丰富规范，但是为了本文的目的，我们选择一个例子：

这个简单的过程在其属性和行为方面揭示了很多：

首先，C 是一个in out参数，所以它必须在被调用之前被初始化，并且它的值在子程序中被修改。请注意，没有指示它是通过复制还是引用传递，这是由编译器根据语言约束和效率自动决定的。

E 是输入参数，或不打算修改的输入值。一个前提条件是在调用之前容器未满。就设计而言，这是一个极其重要的转变，就像在其他语言中的Push过程可能负责检测错误的调用上下文（如果容器已满）并实施缓解技术（或防御性代码）。另一方面，使用先决条件，该过程可以安全地假设容器未满（否则它会被静态或动态检测到，但稍后会详细介绍）并避免这些额外的代码。验证输入的责任隐含在调用者身上，然后调用者可以将其提升给自己的调用者，直到到达代码中数据验证确实有意义的地方。

后置条件提供了有关过程行为的关键属性——这里，E 包含在修改后的容器中并且计数增加的事实。

查看与嵌入式开发相关的一些约束，另一个有用的方面是指定内存映射约束。Ada 允许声明式表示法来指定数据结构在内存中的布局方式和地址，从而避免容易出错的按位操作和一致性检查。例如：

上面声明了一个数据结构以及一些与边界相关的字段：

数据的大小固定为 16 位，接下来的两个方面（具有值High_Order_First）基本上告诉编译器使用大端表示。

下一个子句提供特定的位表示（例如，Size从索引位1到4的字节0开始。

最后，为R提供了它在内存中的地址。

实施（在 SPARK/Ada 或 C 中）

Ada 和 SPARK 语言提供了现代命令式语言的大部分功能。这些功能如何实现的最显着特性是它们为编译器解释提供的空间很小并且避免了捷径。例如，没有隐式转换，并且轻松地执行指针运算之类的操作需要 5 行代码。但是，在实际编码阶段花费的额外时间很容易通过易于验证来重新获得，无论是用于代码阅读、测试还是静态分析。

在讨论的这一点上，值得一提的是房间里的大象：对于新开发的代码来说，使用一种新语言可能是一个好主意，但通常存在一个不容忽视的预先存在的环境。这通常是来自其他项目或现成库的代码。这段代码可能是用 C 语言或 C++ 创建的。仅此一项就经常驱动开发语言的选择。

幸运的是，SPARK 和 Ada 已被设计为与 C 环境很好地集成。一些指令可以将 C 直接映射到 Ada，反之亦然，而无需任何包装代码的开销。这种映射甚至可以自动生成。

因此，如果不推荐的话，在 SPARK 或 Ada 中仅开始开发几个组件，而在其他情况下保留在 C 环境中是完全合理的。

目前可用于 Ada 和 SPARK 的主要编译器技术是 GCC，但也可以提供其他编译器技术。这意味着 SPARK 和 C 代码可以使用相同的技术进行编译，具有相同的优化和代码生成通道。结果，C 和 SPARK 代码之间的性能几乎没有差异，并且没有从一种语言到另一种语言的控制流的损失。

谈到我们之前的一个例子，让我们假设正在使用一个用 C 实现的容器。我们试图与之交互的 C 代码如下所示：

除了来自 C 的实现声明之外，规范在 Ada/SPARK 中完全相同。

Ada 或 SPARK 代码可以像在 Ada 中实现一样使用此过程。与导入类似，导出允许 C 调用用 Ada 编写的子程序。如果需要，这些接口层可以通过绑定生成器自动生成。

尽管将 SPARK 和 C 一起编译解决了许多用例，但仍然存在最终代码必须是 C 的情况。确实，一些用户虽然对使用 SPARK 进行开发感兴趣，但仍需要将 C 代码交付给他们的客户。

可以使用一个特殊的编译器来覆盖这个用例，即“GNAT 通用代码生成器”。它本质上将 Ada 语言的一个子集编译为 C。借助这项技术，SPARK 几乎成为一种建模语言，其输出集成在 C 环境中。它也可以被视为一种交付形式验证的 C 代码的方式，验证在 SPARK 级别执行。

在数据表示示例（寄存器案例）中，在代码中使用这段数据非常简单。分配一个值如下所示：

这里不需要按位运算，因为编译器会在后台自动生成适当的代码。

确认

Ada 和 SPARK 在源代码中提供了大量信息，可供各种检查器使用。例如，作为第一道防线，编译器将检测到许多不一致之处，并可以在测试阶段自动在可执行文件中插入动态验证。有了这个级别的信息，就可以超越经典的静态分析并应用程序验证技术来演示整个应用程序的属性。

对于较低级别的数据结构，也会进行自动一致性验证。编译器验证特定大小是否足以实现所需的数据范围，没有数据重叠等。此外，形式证明可用于验证分配的值是否始终在任何分配的范围内。

继续前面的另一个示例，假设在我们想要验证的一段代码中调用了Push 。例如，我们可以让以下语句从输入文件中读取数字，直到它达到 0：

这个Push调用将被 SPARK 工具标记为不正确，因为无法知道循环不会达到容器 C 的最大容量。证明者无法证明Push的前提条件，这显然应该在调用，而不是在被调用的过程中。如果到达文件末尾而没有击中0 ，则示例代码中可能会出现另一个潜在错误。如果指定了适当的先决条件，证明者将能够判断循环中缺少检查以验证是否仍需要读取输入。

这种问题通常会在某个时候发生。如果覆盖极端案例的单元测试足够广泛，那么问题将在该级别得到解决。然而，当真正的数据开始输入系统时，他们可以找到自己的方式进行集成测试，或者当用户试图破坏系统时进行 beta 测试。在最坏的情况下，其中一些错误会通过部署找到并需要在客户报告后进行追踪。问题不是它们是否会被发现，而是当它们被发现时修复它们的成本会有多高。越晚发现，越多的人参与到链条中，需要更多的调查来确定源头、修复问题、证明修复的合理性、测试修复、重新交付产品等。使用技术早期集成验证 - 在这种情况下，

旧的又是新的

Ada 和 SPARK 方法的独特之处在于它集成了软件规范、实现和验证，提供了一种以现代系统所需的完整性级别生产软件的经济高效的方法。医疗、汽车和工业物联网 （IIoT） 等行业一直在寻找传统 C 语言开发的替代方案，Ada 和 SPARK 提供了经过验证的解决方案。

作为 Ada 语言的提供者，AdaCore 在过去几年中观察到对该技术的新兴趣。今天的限制提供了一个尝试新事物的好机会——或者正在卷土重来的旧事物。

审核编辑：郭婷