第三章第二節 軟件規約

　　這一節我們轉向關註“方法/函數/操作”是如何定義的，即討論編程中的動詞，規約。

Outline

• 一個完整的方法
• 什麽是設計規約，我們為什麽需要他
• 行為等價性
• 規約的結構：前置條件與後置條件
  • 規約的結構
  • 可變方法的規約
• 規約的評價
  • 規約的確定性
  • 規約的陳述性
  • 規約的強度
  • 如何設計一個好的規約
  • 是否使用前置條件

Notes

## 一個完整的方法

• 一個完整的方法包括規約spec和實現體implementation；
• "方法"是程序的積木，它可以被獨立的開發、測試、復用；
• 使用“方法”的客戶端，無需了解方法內部如何工作，這就是抽象的概念；
• 參數類型和返回值類型的檢查都是在靜態類型檢查階段完成的。
• 更多關於方法的內容，請參考 RUNBOOB Java 方法

## 什麽是設計規約，我們為什麽需要他

• 為什麽要有設計規約
  • 很多bug來自於雙方之間的誤解；沒有規約，那麽不同開發者的理解就可能不同
  • 代碼慣例增加了軟件包的可讀性，使工程師們更快、更完整的理解軟件
  • 可以幫助程序員養成良好的編程習慣，提高代碼質量
  • 沒有規約，難以定位錯誤
• 使用設計規約的好處
  • 規約起到了契約的作用。代表著程序與客戶端之間達成的一致；客戶端無需閱讀調用函數的代碼，只需理解spec即可。
  • 精確的規約，有助於區分責任，給“供需雙方”確定了責任，在調用的時候雙方都要遵守。
• 實例

  

  • 規約可以隔離“變化”，無需通知客戶端
  • 規約也可以提高代碼效率
• 實例參考 阿裏Java開發手冊之編程規約

## 行為等價性

行為等價性就是站在客戶端的角度考量兩個方法是否可以互換

參考下述兩個函數：

 1 static int findFirst(int[] arr, int val) {
 2     for (int i = 0; i < arr.length; i++) {
 3         if (arr[i] == val) return i;
 4     }
 5     return arr.length;
 6 }
 7 
 8 static int findLast(int[] arr, int
 
 val) {
 9     for (int i = arr.length - 1 ; i >= 0; i--) {
10         if (arr[i] == val) return i;
11     }
12     return -1;
13 }

• 行為等價性分析：
  • 當val不存在時，findFirst返回arr的長度，findLast返回-1;
  • 當val出現兩次時，findFirst返回較低的索引，findLast返回較高的索引。
  • 但是，當val恰好出現在數組的一個索引處時，這兩個方法表現相同。
  • 故，如果調用方法時，都傳入一個 正好具有一個val的arr ，那麽這兩種方法是一樣的。
• 另外，我們也可以根據規約判斷是否行為等價註：規約與實現無關，規範無需討論方法類的局部變量或方法類的私有字段。

  • static int findExactlyOne(int[] arr, int val)
      requires: val occurs exactly once in arr
      effects:  returns index i such that arr[i] = val

  • 兩個函數附和同一個規約，故二者等價

## 規約的結構：前置條件與後置條件

【規約的結構】

• 一個方法的規約常由以下幾個短句組成契約：如果前置條件滿足了，後置條件必須滿足。如果沒有滿足，將產生不確定的異常行為
  • 前置條件(precondition)：對客戶端的約束，在使用方法時必須滿足的條件。由關鍵字 requires 表示；
  • 後置條件(postcondition)：對開發者的約束，方法結束時必須滿足的條件。由關鍵字 effects 表示
  • 異常行為(Exceptional behavior)：如果前置條件被違背，會發生什麽

• 

• 靜態類型聲明是一種規約，可據此進行靜態類型檢查。
• 方法前的註釋也是一種規約，但需人工判定其是否滿足。
  • 參數由@param 描述
  • 子句和結果用 @return 和 @ throws子句 描述
  • 盡可能的將前置條件放在 @param 中
  • 盡可能的將後置條件放在 @return 和 @throws 中
  • 

【mutating methods(可變方法)的規約】

• 除非在後置條件裏聲明過，否則方法內部不應該改變輸入參數。
• 應盡量遵循此規則，盡量不設計 mutating的spec，否則就容易引發bugs。
• 程序員之間應達成的默契：除非spec必須如此，否則不應修改輸入參數 。
• 盡量避免使用可變(mutable)的對象 。
  • 對可變對象的多引用，需要程序維護一致性，此時合同不再是單純的在用戶和實現者之間維持，需要每一個引用者都有良好的習慣，這就使得簡單的程序變得復雜；
  • 可變對象使得程序難以理解，也難以保證正確性；
  • 可變數據類型還會導致程序修改變得異常困難；

## 規約的評價

規約評價的三個標準

• 規約的確定性
• 規約的陳述性
• 規約的強度

【規約的確定性】

　　確定的規約：給定一個滿足前置條件的輸入，其輸出是唯一的、明確的

1 static int findExactlyOne(int[] arr, int val)
2   requires: val occurs exactly once in arr
3   effects:  returns index i such that arr[i] = val

　　欠定的規約：同一個輸入可以有多個輸出

1 static int findOneOrMore,AnyIndex(int[] arr, int val)
2   requires: val occurs in arr
3   effects:  returns index i such that arr[i] = val

　　未確定的規約：同一個輸入，多次執行時得到的輸出可能不同；但為了避免分歧，我們通常將不是確定的spec統一定義為欠定的規約。

【規約的陳述性】

• 操作式規約（Operational specs）：偽代碼 。
• 聲明式規約（Declarative specs）：沒有內部實現的描述，只有 “初-終”狀態 。
• 聲明式規約更有價值 ； 內部實現的細節不在規約裏呈現，而放在代碼實現體內部註釋裏呈現。

舉一個栗子：

static String join(String delimiter, String[] elements)
effects : returns the result of adding all elements to a new : StringJoiner(delimiter) // Operational specs

effects:returns the result of looping through elements and alternately appending an element and the delimiter // Operational specs

effects: returns concatenation of elements in order, with delimiter inserted between each pair of adjacent elements // Declarative specs

【規約的強度】

• 通過比較規約的強度來判斷是否可以用一個規約替換另一個；
• 如果規約的強度 S2>=S1，就可以用S2代替S1，體現有二：一個更強的規約包括更輕松的前置條件和更嚴格的後置條件；越強的規約，意味著實現者(implementor)的自由度和責任越重，而客戶(client)的責任越輕。
  • S2的前置條件更弱
  • S2的後置條件更強

舉一個栗子：

• Original spec：

1 static int findExactlyOne(int[] a, int val)
2   requires: val occurs exactly once in a
3   effects:  returns index i such that a[i] = val

• A stronger spec:

1 static int findOneOrMore,AnyIndex(int[] a, int val)
2   requires: val occurs at least once in a
3   effects:  returns index i such that a[i] = val

• A much stronger spec:

1 static int findOneOrMore,FirstIndex(int[] a, int val)
2   requires: val occurs at least once in a
3   effects:  returns lowest index i such that a[i] = val

【如何設計一個好的規約】

• 規約應該是簡潔的：整潔，具有良好的結構，易於理解。
• 規約應該是內聚的：Spec描述的功能應單一、簡單、易理解。
• 規約應該是信息豐富的：不能讓客戶端產生理解的歧義。
• 規約應該是強度足夠的：需要滿足客戶端基本需求，也必須考慮特殊情況。
• 規約的強度也不能太強：太強的spec，在很多特殊情況下難以達到。
• 規約應該使用抽象類型：在規約裏使用抽象類型，可以給方法的實現體與客戶端更大的自由度。

【是否使用前置條件】

• 是否使用前置條件取決於如果只在類的內部使用該方法(private)，那麽可以不使用前置條件，在使用該方法的各個位置進行check——責任交給內部client。
  • check的代價；
  • 方法的使用範圍；
• 如果在其他地方使用該方法(public)，那麽必須要使用前置條件，若client端不滿足則方法拋出異常。

【軟件構造】第三章第二節 設計規約