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);