契约驱动的编程使规范超越了石器时代

2013年2月4日

合同编程的工业化时代开启了软件开发的新时代。正如开发技术从汇编到结构化语言，从结构化语言到面向对象，基于契约的编程为软件设计提供了又一种抽象。

昆汀Ochem

相关: AdaCore

这篇文章是嵌入式软件系列:使用Ada契约强制编码

拿你日常工作中使用的任何界面来说。它可能是来自标准组件的应用程序编程接口(API)、公司内部共享的一些库，或者是隔壁隔间的某个人正在为你开发的一段代码。你怎么知道该叫它什么?

现代语言通过类型、函数声明或参数说明提供了标识服务的各种方法，以及引用这些服务的各种方法。某些语言可能会给你更多。Java指定可能抛出的异常，Ada允许你指定类型范围，C允许…嗯，算了。

但是，这种级别的规范几乎没有揭示应用程序的行为，因此需要一些其他的、非正式的、不需要任何工具检查的东西:臭名昭著的文档，几乎只以注释的形式存在。“为什么这是个问题呢?”你可能会说。“让人们发表评论已经够难的了!”

在许多情况下，文档是一项成就。但当可靠性受到威胁时，它只是一个石器时代的规范。如何验证规格书是正确的?如何验证调用者以他们应该的方式进行调用以及他们依赖于他们应该依赖的属性?如何确保在项目的整个生命周期中，在各种修复、重构和重写之后，规范保持一致?

一些替代的技术超越了简单的注释来指定行为，并使用工具检查的形式主义。这里，我们将特别考虑三种语言:C、Java和Ada。我们还将展示，一旦编写了规范，它不仅可以用于文档，还可以直接用于测试和静态分析工具。

前置条件、后置条件和类型不变式

让我们首先介绍契约的概念。在编程语言中，契约通常是一个布尔表达式，在程序中的某些点进行验证。最有趣的契约可能是后置条件。它定义了函数调用后必须为真的属性。通常，它可以是指定该函数的行为或需求的一种方法。它是对实现者的约束(实现者必须在实现中满足后置条件)和对调用者的保证(调用者可以在调用后依赖后置条件)。

为了实现后置条件，我们通常需要两件事:函数的正确实现和在调用之前需要满足的一组属性。这些属性称为先决条件。先决条件是对调用者的约束(调用者必须在调用之前完成它，以确保正确的行为)和对实现者的保证(实现者可以依赖于其实现中的先决条件)。后置条件是给予调用者的保证(调用后环境的状态)和对实现者的约束(函数必须执行的内容)。

类型不变式是一个属性，对于给定类型的每个对象，它必须始终为真。它可以描述值范围、字段之间的关系和类似的属性。

在这里，我们将考虑一个简单的系统，其中物理对象在二维环境中移动。每个对象都与X和Y坐标、大小和标识符相关联。函数iterate在每个循环中被调用，它负责一步一步地更新对象的位置。对象将存储在列表中。

除了结构规范，我们还会添加一些行为需求:

X和Y必须在区间[-200.0,200]内。
Size必须在间隔[0 ..]内。100]。
除设置为特殊的未初始化值外，所有对象id必须唯一。
迭代只能在已经初始化的对象上调用。
迭代不能改变对象的大小或ID。
通过迭代所做的每次移动都必须小于对象大小的十分之一。

其中一些需求可以清楚地映射到类型不变量，即1、2和3，它们是类型和数据的专有属性，在程序的整个生命周期中都必须为真。其他的可以映射为先决条件，特别是4。最后，需求5和6描述了函数的行为，因此映射到后置条件。现在，可以使用基于Java、C和Ada的三种不同语言来实现上述规范。

Java和JML

Java建模语言(Java Modeling Language, JML)是Java的扩展，使用常规Java编译器，Java代码应该是可兼容的。因此，所有JML注释都是用特殊的java注释编写的，以//@或/*@开头。让我们先翻译并注释下面的代码。

public class Object {public static String NO_INIT = 0;public int id = NO_INIT;Public float x, y, size = 0;// @公共不变式x >= -200 && x <= 200;// @公共不变式>= -220 && y <= 200;// @公共不变式sie >= 0 && size <= 100;// @需要id /= NO_INIT;// @可分配的x // @可分配的y // @确保数学。√数学。pw (\old (x) - x, 2) // @ + Math。\旧的(y) - y, 2)) <= size / 10; public void iterate () ( { … } ) public static Object [] list = new Object [100]; // @ public invariant // @ (\forall int j; j >= 0 && j < list.size; // @ list [j].id.equals (NO_INIT) || // @ (\forall int k; k >= j + 1 && k < list.size; // @ !list [j].id.equals (list [k].id)));

ACSL和JML示例之间的第一个显著区别是，虽然JML允许引入可执行的契约，这些契约可以引用代码中的实际实体，但ACSL目前是纯形式化的。因此，ACSL不能调用“实”函数，只能调用正式函数，只能根据相应的正式属性进行推理。这就是Math公理的特殊目的，它引入了pow和sqrt形式函数。

Range_Object公理定义了一个对象的x, y和大小字段的值范围。然后在类型不变式中使用这个公理来验证对象类型的所有实例都遵守这个公理。还要注意\valid (v)结构，它指定指针必须是有效的(可以被解引用)。

除了这两个区别之外，这与JML示例非常接近。有关ACSL的更多信息，请访问http://frama-c.com/acsl.html．

艾达和艾达2012

Ada 2012语言的主要新特性之一是它能够在语言定义中包含重要的契约信息，而不需要外部工具以及相应的动态语义。下面的代码展示了如何在Ada 2012中编写前面示例中的相同规范。

包对象是No_Init:常量:= 0;type对象是记录Id: Integer:= No_Init;X, Y:浮动范围-200.0…200.0: = 0.0;尺寸:浮动范围0.0 ..100.0: = 0.0;结束记录;过程迭代(V: in out Object)， Pre => V. id /= No_Init, Post => V. size = V. size 'Old，然后V. id = V. id 'Old，然后Sqrt ((V. x = V. x 'Old) ** 2 + (V. y -V.Y'Old) **) <= V. size / 10.0;类型Arr是数组(整数范围<>)的对象Dynamic_Predicate =>(为所有J在Arr'Range => Arr (J).Id = No_Init或其他(为所有K在J + 1 ..Arr' => Arr (J).Id /= Arr (K.Id)); List : Arr (1 .. 100); end Object ;

这只是一个例子，说明了在试图引入强大的形式证明技术时所产生的各种约束。这类问题可以通过使用比低级指针(比如SPARK中的引用)约束更大的结构来检测。这里还有更多要说的，但它可能是即将发表的一篇论文的主题。