Ada 编程/基于契约的编程

计算 » 计算机科学 » 计算机编程 » Ada 编程

---

此语言特性是在 Ada 2012 中引入的。

Ada 2012 中的基于契约的编程

在 Ada 2012 的新增功能中，许多方面遵循“类型和子程序形式”契约的共同主题。这里的形式是指与 Ada 的现有特性相结合的符号逻辑。契约赋予语言类似于 Eiffel 的 Design by Contract™、SPARK 或与 LSP 相关的那些表达性特性。

由于指定契约涉及 Ada 语言的几个部分，并且由于编译器遵守契约也是如此，因此契约主题在语言参考的几个部分中都有涉及。最新版 Ada 概述提供了一个全面且更集中的视角。^[[1]]

契约的部分内容可以是关于程序的静态已知属性，而其他部分则仅在运行时进行检查。在第一种情况下，契约的形式部分不仅可以由 Ada 编译器分析，还可以由证明工具分析。分析得到的结果可以保证程序中不存在某些不良特性。例如，程序可以被认为不会引发异常。

本概述将仅通过示例概述语法和变体，同时参考现有的维基教科书条目和其他资源来解释一般契约。

子程序的前置条件和后置条件

例如，考虑函数，它们的规范在参数概要中给出了返回值的类型。通知函数返回值的具体信息的一种方法是提供一个数学（风格）结果表达式，因此该表达式由契约的该条款保证。契约还可以指定条件，说明什么必须是进入计算的对象的真值才能使函数产生其结果。在契约中，返回值被命名为function_name'Result.

  function Sum (A, B : Number) return Number
  with
    Post => (if
               A <= 0.0 and B >= 0.0
             then
               Sum'Result = A + B);

一种替代的表达方式强调先决条件，

  function Sum (A, B : Number) return Number
  with
    Pre  => A <= 0.0 and B >= 0.0,
    Post => Sum'Result = A + B;

第一个示例没有说明条件计算结果为 False 时会发生什么。默认情况下，当断言失败时，如果当前的 Assertion_Policy 为 Check，则会引发 Assertion_Error。（Ada 的当前修订过程正在考虑“引发表达式”（8652/0117）：如果条件不为 True，则这些表达式允许引发特定异常作为else 部分，并提供相应的特定消息，而不是默认如上所述。）第二个示例明确要求，在Pre中，调用者确保 bothA和B将具有指定的属性，分别为Numbers 且不超过 0.0 且不小于 0.0。这样，Pre 方面就表明，如果条件为 False，则函数将无法履行其在Post.

中给出的契约义务。

[编辑 | 编辑源代码]

  type Stack is private
      with Type_Invariant => Count(Stack) >= 0;

Ada 类型可以被声明为具有类型不变式。这种谓词适用于私有类型。因此，它的表达式只能引用类型的其他公开可见特性。此处的类型名称表示类型的当前实例。如 3.2.4: 类型不变式 ^{[带注释的]} 所述，不变式也可以用于类型的派生类，使用方面名称Type_Invariant'Class

，应用于层次结构中的所有类型。在声明子类型时也可以提供谓词。在这种情况下，表达式（布尔类型）说明了子类型的属性（有关详细信息，请参阅 3.2.4: 子类型谓词 ^{[带注释的]}），并且它的真值会在某些点进行检查。当谓词应该由编译器测试时，它的方面名为Static_Predicate，否则为Dynamic_Predicate

。大致来说，当类型转换发生时，或当参数传递时，或当对象创建时，就会执行检查。

当派生子类型时，应用的谓词是所涉及的子类型的谓词的合取。

[编辑 | 编辑源代码]语言参考手册扩展了Assertpragma 及其关联的Assertion_Policy

  pragma Assertion_Policy (Pre => Check);

，也涵盖了 11.4.2: Pragma Assert 和 Assertion_Policy ^{[带注释的]} 中基于契约的编程方面。契约的每个“部分”，例如 Pre，都可以打开和关闭以进行检查。这可以通过指定所需的 Assertion_Policy 来完成，无论是在本地还是全局，只要需要都可以。以下行将方面标记 Pre 的检查打开Ada 的实现可以自由地提供比语言定义的两个标识符更多的策略标识符，和Check.

Ignore

  pragma Assertion_Policy (Check);