麻省理工18年春软件构造课程阅读07“设计规格说明”
本文內容來自MIT_6.031_sp18: Software Construction課程的Readings部分，采用CC BY-SA 4.0協議。
由于我們學校（哈工大）大二軟件構造課程的大部分素材取自此，也是推薦的閱讀材料之一，于是打算做一些翻譯工作，自己學習的同時也能幫到一些懶得看英文的朋友。另外，該課程的閱讀資料中有許多練習題，但是沒有標準答案，所給出的答案均為譯者所寫，有錯誤的地方還請指出。
譯者：李秋豪
審校：
V1.0 Tue Mar 20 00:49:34 CST 2018
本次課程的目標
- 理解待決定（underdetermined）規格說明，并能夠辨別評估待決定的規格說明。
- 理解聲明性的規格說明和操作性的規格說明之間的區別，并能夠寫出聲明性的規格說明。
- 理解前置條件、后置條件、及規格說明的“強度”，并能夠比較兩個規格說明之間的強度。
- 能夠寫出邏輯嚴密、前后連貫的規格說明。
介紹
在這篇閱讀中我們會比較相似行為的不同規格說明，并從三個維度探討它們之間的區別：
- 這個規格說明的決定性：它對輸入輸出的空間是否有嚴格的限制？例如要求輸出只有一種可能，或者可以有多種可能性。
- 這個規格說明的聲明性：它是否僅僅聲明了輸出應該是什么，或者還要求了實現的方法（輸出是如何計算出的）。
- 這個規格說明的強度：它的實現方法是否僅限于一個小集合，或者有很多種滿足要求的實現方法。
對于一個特定的模塊，不同的規格說明會產生不同的效果，接下來我們就探討如何設計出最好的的規格說明。
決定性的 vs. 待決定性的規格說明
回憶之前的閱讀中我們定義的兩個find函數：
static int findFirst(int[] arr, int val) {for (int i = 0; i < arr.length; i++) {if (arr[i] == val) return i;}return arr.length; } static int findLast(int[] arr, int val) {for (int i = arr.length - 1 ; i >= 0; i--) {if (arr[i] == val) return i;}return -1; }這里提一下，函數名中的后綴 First and Last 只是為了區分開它們實現方法，當被應用到實際的代碼中時，它們都叫做find.
以下是find的一種可能的規格說明：
static int findExactlyOne(int[] arr, int val) - requires:val occurs exactly once in arr - effects:returns index i such that arr[i] = val這里的后綴名 ExactlyOne也僅是一種提示符，為了區分開同一模塊的不同規格說明設計。
我們說，findExactlyOne是完全決定性的（fully deterministic）：當輸入滿足前置條件后，輸出能夠完全確定——僅僅只有一種可能的返回情況。不存在一個輸入對應多種輸出。
findFirst 和 findLast 的實現方法都滿足這個規格說明的要求，所以如果有一個客戶使用了這個規格說明的find模塊，我們可以用 findFirst 和 findLast 進行等價替換。
下面是find的另一種規格說明：
static int findOneOrMore,AnyIndex(int[] arr, int val) - requires:val occurs in arr - effects:returns index i such that arr[i] = val這個規格說明就不是決定性的——當val出現多次時，它沒有要求返回哪一個的下標。即它僅僅承諾了你可以根據返回的下標找到對應的val 。對于一個輸入，這個模塊有多種輸出的可能性。
這里要注意一點，當我們說“非決定性”（underdetermined）的時候，并不是指“不確定性”（nondeterministic）。不確定性的代碼是指一會的行為是這樣，過一會又變成了那樣（即使對于同一個輸入）。有很多不確定的例子：例如一個依賴于隨機數的函數，或者一個依賴于當前時間的程序。但是一個非決定性的規格說明并不一定代表對應的模塊的行為是非確定性的，模塊可以是由完全確定行為（一個輸入就對應一個確定的輸出）的代碼寫的。
在上面的例子中，規格說明沒有要求返回值是多種可能的哪一個，我們既可以使用 findFirst 又可以使用 findLast實現這個模塊，但是這兩個實現方法本身是確定性的（譯者注：確定性在算法層面，對于同一個輸入，有同一個輸出）。甚至，我們可以使用非確定性的代碼滿足規格說明，例如每次使用隨機數決定返回多個下標中的哪一個。而使用者只會關注規格說明，他們無法確定模塊會返回哪一種結果（譯者注：決定性在使用者應用層面，他只能依賴規格說明的描述）。在大多數情況下，非決定性的規格說明會給實現者更多實現的自由，另外，一個非決定性的規格說明對應的模塊大多是用確定性的代碼實現的。
閱讀小練習
Distinguished
對于findFirst和findLast兩種對find的實現方法：
static int findFirst(int[] arr, int val) {for (int i = 0; i < arr.length; i++) {if (arr[i] == val) return i;}return arr.length; } static int findLast(int[] arr, int val) {for (int i = arr.length - 1 ; i >= 0; i--) {if (arr[i] == val) return i;}return -1; }考慮下面這個規格說明：
static int find(int[] arr, int val) effects:returns largest index i such that arr[i] = val, or -1 if no such i以下哪一種輸入會使findFirst 不滿足規格說明？
[x] [ 1, 2, 2 ], 2
[ ] [ 1, 2, 3 ], 2
[x] [ 1, 2, 2 ], 4
[ ] 對于以上輸入 findFirst 都可以滿足規格說明!
以下哪一種輸入會使findLast不滿足規格說明？
[ ] [ 1, 2, 2 ], 2
[ ] [ 1, 2, 3 ], 2
[ ] [ 1, 2, 2 ], 4
[x] 對于以上輸入 findLast都可以滿足規格說明!
Over/under
在上文中我們提到了 find 的一種非決定性的規格說明:
static int findOneOrMore,AnyIndex(int[] arr, int val) - requires:val occurs in arr - effects:returns index i such that arr[i] = val當數組中含有多個val時，這個規格說明允許多種返回情況。
對于下面的每一個規格說明，判斷它的決定性大于或小于 findOneOrMore,AnyIndex 的決定性，或者它是完全決定性的。
1
static int find(int[] arr, int val) - requires:val occurs exactly once in arr - effects:returns index i such that arr[i] = val[x] 完全決定性的
[ ] 大于 findOneOrMore,AnyIndex, 但是不是完全決定性的
[ ] 小于 findOneOrMore,AnyIndex
2
static int find(int[] arr, int val) effects:returns largest index i such that arr[i] = val, or -1 if no such i[x] 完全決定性的
[ ] 大于 findOneOrMore,AnyIndex, 但是不是完全決定性的
[ ] 小于 findOneOrMore,AnyIndex
3
static int find(int[] arr, int val) - requires:val occurs in arr - effects:returns largest index i such that arr[i] = val[x] 完全決定性的
[ ] 大于 findOneOrMore,AnyIndex, 但是不是完全決定性的
[ ] 小于 findOneOrMore,AnyIndex
18.6.16更新：這里應當是完全決定性的，xjf指出
聲明性的 vs. 操作性的規格說明
籠統的說，規格說明分為兩種：操作性的（Operational）規格說明給出了實現過程的步驟（就像偽代碼一樣），而聲明性的（Declarative）規格說明不對實現過程進行要求，它們僅僅給出最后輸出的屬性和意義，以及它們和輸入之間的關系。
在絕大多是情況下，聲明性的規格說明更合適。它們通常會更簡潔、更易懂、并且最重要的是，它們不會讓使用者嘗試依賴特定的實現方案（很多時候一個模塊的實現方案會不得不改變）。例如，如果我們想要允許多種方案來實現find ，我們就不會在規格說明要求“從數組低位開始向上遍歷搜索”。
有些時候，程序員想要給維護者（maintainer）模塊的實現信息，于是他們將實現描述寫在了規格說明中。要記住，規格說明是給使用者而非模塊的開發者使用的，如果你想要用描述模塊的實現方法，將它們注釋在模塊里面。
另外，對于一種聲明性的規格說明，可以有多種描述方法，例如下面這幾個聲明性的規格說明都是等價的：
static boolean startsWith(String str, String prefix) effects:returns true if and only if there exists String suffix such that prefix + suffix = str static boolean startsWith(String str, String prefix) effects:returns true if and only if there exists integer i such that str.substring(0, i) = prefix static boolean startsWith(String str, String prefix) effects:returns true if the first prefix.length() characters of str are the characters of prefix, false otherwise我們要做的就是給使用者選擇一個最清晰易懂的。
閱讀小練習
Joint declaration
給出下面這個規格說明：
static String join(String delimiter, String[] elements) effects:append together the strings in elements, but at each step, if there are more elements left, insert delimiter重寫這個規格說明，使得它是聲明性的而非操作性的。
[ ] effects: 將所有的元素通過 new StringJoiner(delimiter)相加
[ ] effects: 通過一個循環將各個元素和分隔符疊加起來
[x] effects: 返回一個元素的連接體（元素保持原有順序），并在各個元素中插入分隔符。
更強或更弱的規格說明
假設你想要改變一個方法——不管是它的實現方法還是規格說明本身。并且現在已經有使用者在依賴你之前的規格說明來使用方法了，你該怎么確定新的規格說明可以安全的替換原有的規格說明呢？
定義：規格說明S2強于（等于）規格說明S1，如果：
- S2的前置條件弱于或等價于S1的
- S2的后置條件強于或等于S1的后置條件。
如果S2強于S1，那么任何S2的實現方法都可以拿來實現S1，并且在程序中可以安全的用S2的模塊替換S1模塊。
這兩個條件實際上表現了一種思想：你可以弱化前置條件（譯者注：即更容易滿足前置條件，或者說滿足前置條件的集合擴大了），這會讓使用者的限制更少（譯者注：例如不用對模塊的輸入先進行一些檢查），也可以強化后置條件（譯者注：在使用者看來，就是模塊的返回更清晰，更有保證性，不用對多種可能情況進行處理）。
例如，對于 find的規格說明：
static int findExactlyOne(int[] a, int val) - requires:val occurs exactly once in a - effects:returns index i such that a[i] = val可以被替換為：
static int findOneOrMore,AnyIndex(int[] a, int val) - requires:val occurs at least once in a - effects:returns index i such that a[i] = val可以看到，他的前置條件變弱了。而這個規格說明可以繼續加強：
static int findOneOrMore,FirstIndex(int[] a, int val) - requires:val occurs at least once in a - effects:returns lowest index i such that a[i] = val即強化了后置條件。
那么下面這個規格說明呢？
static int findCanBeMissing(int[] a, int val) - requires:nothing - effects:returns index i such that a[i] = val, or -1 if no such i我們試著將它和 findOneOrMore,FirstIndex比較，它的前置條件更弱。但是它的后置條件也更弱——對于滿足 findOneOrMore,FirstIndex的輸入， findOneOrMore,FirstIndex承諾返回最小下標，但是findCanBeMissing沒有做任何承諾。所以它們是不可比較的。
在下面的練習中我們會繼續用 findCanBeMissing 和其他的規格說明進行比較。
圖示化規格說明
I試著將Java中的全部方法想象成一個太空，太空中的每一個星星就是一個方法。在這里我們先將上面提到的 findFirst 和 findLast 畫出來。記住，對于 findFirst 和 findLast ，它們的算法/行為是固定的，不能在這個空間中表示一個范圍，所以我們用點來表示實際的方法。
而一個規格說明會在這個太空中描述出一個范圍，在這個范圍中的實現方法都滿足規格說明的要求（即前置條件和后置條件），而在范圍之外的不滿足規格說明的要求。
findFirst 和 findLast 都是滿足 findOneOrMore,AnyIndex的，所以它們都在 findOneOrMore,AnyIndex描述的范圍內：
我們可以想象使用者站在地上向天空望去：規格說明就好像星云的規定邊界一樣
- 實現者可以自由的在一個星云中移動（即改變實現方案/代碼），例如提升原有算法的性能或修復一個bug，而不必擔心這種改變會導致使用者的不變。
- 使用者只選取某一個星云，而不在意或依賴到底是其中的哪一個星星。他們可以自由的將模塊應用在各個環境（只要滿足規格說明）。
該如何描述兩個規格說明之間的關系呢？現在假設有S1和S2兩個規格說明，它們一開始的強度是一樣的：
我們先從加強后置條件考慮，如果S2的后置條件變的強于S1的后置條件。那么S2就是強于S1的。
想一想強化后置條件對于實現者來說意味著什么：更少的自由度，因為輸入的空間變小了。例如之前的規格說明是findOneOrMore,AnyIndex ，而更改后的規格說明變成了 findOneOrMore,FirstIndex 。所以以前在“星云”內的實現方案現在可能在新的星云之外了。
那么，是否存在一種實現方案，它在 findOneOrMore,FirstIndex 之內但是在findOneOrMore,AnyIndex之外呢？這是不可能的，因為所有滿足findOneOrMore,FirstIndex 的實現方案都強于 findOneOrMore,AnyIndex 的要求。
接著想一想弱化前置條件，這也會使S2變得更強。實現方案需要處理更多的可能輸入空間，如果之前它們沒有在意這寫數據范圍，現在可能就會暴露出一些bug。
對于一個更強的規格說明，它在圖示中能描繪的實現范圍更小，而一個更弱的規格說明描述的實現范圍更大：
在上圖中，由于findLast 是從數組的最后一個元素開始遍歷，所以它不符合findOneOrMore,FirstIndex的后置條件，即它會在findOneOrMore,FirstIndex描繪的范圍之外。
而對于一個既不強于S1也不弱于S1的規格說明S3，它和S1的范圍可能是有重疊的（即存在實現方案即滿足S1，也滿足S3），也可能是沒有重疊的。在這兩種情況下，S1和S3都是不可比較的。
閱讀小練習
Bulking up
當一個規格說明被強化后：
[x] 滿足它的實現方案會變少
[ ] 滿足它的實現方案會變多
[ ] 更少的使用者
[x] 更多的使用者
[ ] 以上都不是
Strength is truth
以下關于A和B規格說明的關系的描述哪一個是對的？
[x] A強于B，且A的前置條件更弱
[x] A強于B，且前置條件相同
[ ] A強于B，且A的前置條件更強
[ ] A強于B，且前置條件不可比較
[x] A和B不可比較
Finding findExactlyOne
下面是 find 的各種規格說明：
static int findExactlyOne(int[] a, int val) - requires:val occurs exactly once in a - effects:returns index i such that a[i] = val static int findOneOrMore,AnyIndex(int[] a, int val) - requires:val occurs at least once in a - effects:returns index i such that a[i] = val static int findOneOrMore,FirstIndex(int[] a, int val) - requires:val occurs at least once in a - effects:returns lowest index i such that a[i] = val static int findCanBeMissing(int[] a, int val) - requires:nothing - effects:returns index i such that a[i] = val, or -1 if no such i對于前三個規格說明，下面哪一個圖的描述是正確的？
[ ] 1.
[ ] 2.
[x] 3.
[ ] 4.
Finding findCanBeMissing
findCanBeMissing和 findExactlyOne是何種關系？
[ ] findCanBeMissing 弱于 findExactlyOne
[x] findCanBeMissing 強于 findExactlyOne
[ ] findCanBeMissing 和 findExactlyOne 不可比較
How does findCanBeMissing compare to findOneOrMore,AnyIndex?
[ ] findCanBeMissing 弱于 findOneOrMore,AnyIndex
[x] findCanBeMissing 強于 findOneOrMore,AnyIndex
[ ] findCanBeMissing 和 findOneOrMore,AnyIndex 不可比較
How does findCanBeMissing compare to findOneOrMore,FirstIndex?
[ ] findCanBeMissing 弱于 findOneOrMore,FirstIndex
[ ] findCanBeMissing強于 findOneOrMore,FirstIndex
[x] findCanBeMissing 和 findOneOrMore,FirstIndex 不可比較
Found
下面關于 findCanBeMissing 的描述哪一個是正確的？
[ ] 1.
[ ] 2.
[ ] 3.
[x] 4.
[ ] 5.
設計好的規格說明
什么因素對一個方法的設計最重要？毫無疑問是初期該方法的規格說明設計。
一個好的規格設計應該簡潔清楚、結構明確、易于理解的。
但是，規格說明的具體內容是很難用一套固定的設計規則描述的，不過這里我們有一些有用的指導方針。
規格說明應該邏輯明確
規格說明不應當有很多種情況（或者if-else判斷）、也不應該有很多參數，布爾類型1的標志也是不好的。思考下面這個規格說明：
static int sumFind(int[] a, int[] b, int val) effects:returns the sum of all indices in arrays a and b at which val appears這個設計合理嗎？可能不是：它的邏輯不明確，因為它嘗試將兩個毫不相干的事情一起完成（在兩個數組里面查找并將下標相加）。將這兩件事情用兩個分別的模塊來完成會更合理。一個在兩個數組中查找對應的下標，另一個將這兩個下標相加然后輸出結果。
下面是另外一個例子，“代碼評審”中的 countLongWords 方法：
public static int LONG_WORD_LENGTH = 5; public static String longestWord;/*** Update longestWord to be the longest element of words, and print* the number of elements with length > LONG_WORD_LENGTH to the console.* @param words list to search for long words*/ public static void countLongWords(List<String> words)除了槽糕的使用全局變量和打印而非返回結果（譯者注：這兩個問題都在“代碼評審”這個閱讀中談到了）。這個規格說明的邏輯也是有問題的——它試著同時完成兩件事：找到最長的詞和統計符合長度要求的詞的個數。
將這兩件事情用兩個不同的方法完成不僅會更加簡單（易于理解），也會在其他的上下文中方便復用。
調用的結果應該清晰
思考下面這個規格說明，它將一個值放在一個映射中：
static V put(Map<K,V> map, K key, V val) - requires:val may be null, and map may contain null values - effects:inserts (key, val) into the mapping, overriding any existing mapping for key, and returns old value for key, unless none, in which case it returns null注意到前置條件中并沒有規定key鍵對應值不能是null 。但是后置條件中將null作為一個特殊條件來返回。這意味著如果返回值是null ，那么使用者就不能判斷到底是這個key對應的值是null ，還是這個key值以前不存在。因此，這不是一個好的設計，它會產生歧義。
規格說明應該足夠“強”
譯者注：這里的強主要指后置條件的強度
當然，規格說明應該保證對于一般的輸入（滿足前置條件的空間）它會滿足要求，這里要說的是對于一些前置條件之外的特殊情況的處理。
例如，對于一個錯誤的輸入，拋出異常并且允許任意的更改就是毫無意義的。因為使用者無法確定模塊在拋出異常前對對象做了哪些更改。這里有一個規格說明就描述了這樣的缺項（并且它的描述是操作性的，這也不好）：
static void addAll(List<T> list1, List<T> list2) effects:adds the elements of list2 to list1, unless it encounters a null element, at which point it throws a NullPointerException如果異常 NullPointerException 被拋出，使用者就得想方設法找到是list2中的哪一個null元素導致了異常的發生（list1被做了哪些改變）。（譯者注：這些應該在拋出時進行描述）
規格說明也應該足夠“弱”
譯者注：這里的強度主要指前置條件的強度
思考下面這個規格說明，該模塊試著打開一個文件：
static File open(String filename) effects:opens a file named filename這是一個不好的規格說明。它缺乏一些重要的細節：這個文件打開后是進行寫還是讀操作？這個文件是已經存在的嗎？（如果不存在的話，這個模塊會進行創建嗎？）并且它的強度太大了（譯者注：前置條件過弱），畢竟這個模塊是不能保證正確打開一個文件的。例如，模塊所在的進程可能沒有打開這個文件權限，或者這個文件的已經損壞了，操作系統拒絕打開它（譯者注：即有很多程序不能控制的因素決定的打開是否成功）。所以，這個規格說明應該更弱一些，例如說明使用者應該具有該文件的讀/寫權限，這個文件存在等等。
規格說明應該盡可能使用抽象的數據類型
我們之前在“Java基礎”中談到了Java的聚合類型，里面說到了對數據抽象的要求說明例如 List 和 Set 以及具體的實現方法例如 ArrayList 和 HashSet.
在規格說明中使用抽象的數據類型會給使用者和實現者更多的自由。在Java中，這通常意味著使用接口類型，例如 Map 或 Reader 而不是具體的實現類型例如 HashMap 或 FileReader 。現在考慮下面這個規格說明：
static ArrayList<T> reverse(ArrayList<T> list) effects:returns a new list which is the reversal of list, i.e. newList[i] = list[n-i-1] for all 0 ≤ i < n, where n = list.size()這個規格說明強制使用者傳入一個 ArrayList ，并且強制實現者返回一個 ArrayList ，即使List實現方法有很多種。從描述上看，對應模塊的行為應該不會依賴于 ArrayList的實現特性。所以這里最好寫成更抽象的數據類型List 。
使用前置條件還是后置條件
另一個設計的問題就是是否使用前置條件，如果使用的話，是否需要模塊在一開始對參數進行檢查，判斷其符合前置條件后再進行后續工作。事實上，使用前置條件的一個最常見的要求就是輸入必須精確滿足前置條件，因為模塊檢查參數的資源代價可能會很大。
正如上面所提到的，“重量級”的前置條件會讓使用者不方便，因為他們必須確保輸入不違反前置條件的要求，如果違反了，從錯誤中恢復的方法將是不可預測的。所以使用者大多不喜歡前置條件，這也是為什么Java API 類趨向于（作為后置條件）在參數不合法的時候拋出一個非檢查的異常。這樣的手段使得發現bug更加容易。通常情況下，快速失敗/報錯總是更好的（即離bug越近越好），而不是讓錯誤的參數繼續參與剩下的運算。例如，atan(y, x)可能會要求輸入不能是(0,0)（但不是前置條件），但是它依然會接受這種參數并拋出一個明確的異常，而不是讓這個參數參與剩下的計算并返回一個“垃圾值”。
有時候，檢查參數是不可行的，這個時候前置條件就是必須的了。例如我們想用二分查找的辦法實現find ，我們會要求這個數組是已經排序過的了。如果強制要求模塊檢查這個數組是否已經排好序，這個帶來的線性復雜度相對于我們要實現的目標是承受不起的。
關于是否使用前置條件是一個工程上的判斷。關鍵點在于檢查需要使用的資源量以及這個模塊被使用的范圍。當這個模塊僅僅在類的內部使用時，我們設置前置條件，仔細檢查所有的調用是否合理。但是如果這個方法是公開的，并且會被其他的開發者使用，那么使用前置條件就不那么合理。像Java API一樣，你應該拋出一個異常。
關于訪問控制
閱讀: Packages
閱讀: Controlling Access
在之前的閱讀中，我們一直在使用public的方法，也沒有對此進行特別的考慮。一個方法是public還是private取決于這個類的功能。公共的方法可以被程序中其他的部分訪問。將一個方法公開就相當于你想讓方法所在的類為其他的類提供對應的服務。如果你將所有的方法設置為公開訪問的——包括那些本來只設計在內部使用的方法，未來更改這個類就會變得很困難，因為外部可能會依賴這個類的內部實現。總之，這會讓你的代碼不具備可改動性 。
將一個內部使用的方法設置為公開訪問也會讓類的接口變得復雜。保持內部方法私有會讓接口簡潔而且符合邏輯，這會讓你的代碼易于理解 。
在接下來的幾個閱讀中，當我們開始使用類的內部狀態時，我們會看到更多的使用private修飾的理由，這會讓你的代碼遠離bug 。
類方法和實例方法（static vs. instance）
閱讀: the static keyword
同時，我們也一直在使用static方法而沒有過多的考慮。類方法是指那些不與特定的類實例（對象）相關聯的方法（譯者注：或者說沒有this指針），而實例方法（沒有static修飾）必須通過特定的對象來調用。
實例方法的規格說明和類方法的規格說明是一樣的，但它們通常會利用實例對應的具體屬性。
例如，下面這個非常熟悉的規格說明：
static int find(int[] arr, int val) - requires:val occurs in arr - effects:returns index i such that arr[i] = val如果這里不是使用 int[]，而是一個IntArray 對象呢？那么IntArray 必須提供一個實例方法，對應的規格說明就會是：
int find(int val) - requires:val occurs in this array - effects:returns index i such that the value at index i in this array is val在以后的課程中我們會討論很多關于實例方法的規格說明的內容。
閱讀小練習
Show me a sign
下面哪一些選項代表了好的規格說明的屬性？
- [x] 該規格說明是聲明性的
- [ ] 該規格說明是操作性的
- [ ] 規格說明的強度應該越大越好
- [ ] 規格說明的強度應該越弱越好
- [ ] 模塊的實現應該允許忽略錯誤的參數
- [x] 模塊的實現應該允許根據具體的參數選擇不同的算法
- [ ] 規格說明應該強調使用者對于模塊具體實現的理解
That’s an odd way of looking at it
關于上面這個規格說明，以下哪一些批評是合理的？
- [x] 這個規格說明的定義有問題，我們無法實現它（譯者注：當輸入的數組只有一個元素的時候）
- [x] 這個規格說明的邏輯不對（譯者注：odd number、2nd-largest都不合理，應該使用更一般化的要求）
- [ ] 這個規格說明不是決定性的
- [ ] 這個規格說明不是操作性的
Behavioral oddities
public static int secondToLastIndexOf(int[] arr, int val)- requires:val appears in arr an odd number of times- effects:returns the 2nd-largest i such that arr[i] == val思考下面這些對于 secondToLastIndexOf的測試用例：
[ 1, 3, 4 ], 3 返回 1
- [ ] 合理的測試用例
- [ ] 如果前置條件變弱，這個測試用例就是合理的
- [ ] 如果前置條件變弱，后置條件變強，這個測試用例就是合理的
- [x] 如果后置條件變弱，這個測試用例就是合理的
[ 1, 3, 3, 4 ], 3 返回 1
- [ ] 合理的測試用例
- [x] 如果前置條件變弱，這個測試用例就是合理的
- [ ] 如果前置條件變弱，后置條件變強，這個測試用例就是合理的
- [ ] 如果后置條件變弱，這個測試用例就是合理的
[ 1, 3, 3, 3, 4 ], 3 返回 2
- [x] 合理的測試用例
- [ ] 如果前置條件變弱，這個測試用例就是合理的
- [ ] 如果前置條件變弱，后置條件變強，這個測試用例就是合理的
- [ ] 如果后置條件變弱，這個測試用例就是合理的
[ 3, 3, 3, 3 ], 3 拋出一個異常
- [ ] 合理的測試用例
- [ ] 如果前置條件變弱，這個測試用例就是合理的
- [x] 如果前置條件變弱，后置條件改變，這個測試用例就是合理的
- [ ] 如果后置條件變弱，這個測試用例就是合理的
Odd doc
public static int secondToLastIndexOf(int[] arr, int val)- requires:val appears in arr an odd number of times- effects:returns the 2nd-largest i such that arr[i] == val（首先這是一個糟糕的規格說明）在下面選取合適的行組成這個規格說明在代碼中的注釋：
- [x] /*
- [ ] /**
- [x] * Finds the second-to-last occurrence of a value in an array.
- [ ] * Find j, the largest index such that arr[j] == val.
- [ ] * Then find i, the largest index such that i < j and arr[i] == val.
- [x] * @param arr array to search
- [ ] * @param arr fixed-size array of integers to search
- [ ] * @param val value to search for
- [x] * @param val value to search for, requires val appears in arr an odd number of times
- [ ] * @return index i
- [x] * @return second-largest index i such that arr[i] == val
- [x] */
總結
規格說明在使用者和實現者之間起著一道防火墻的作用——對于人和代碼之間也是一樣。正如上篇閱讀談到的（譯者注：“規格說明”），這使得獨立開發成為可能：使用者可以在不閱讀模塊源碼的情況下將源碼應用到各個地方，使用者可以不在意模塊被使用的環境（只要他們都遵循規格說明的要求）。
在實際使用中，聲明性的規格說明是最重要的。前置條件（弱化規格說明）使得使用者更困難（確保輸入合法），但是合理的使用會使得實現者能夠做出一些假設，從而選擇更合適的實現方案。
和往常一樣，試著將這篇閱讀的知識點和我們的三個目標聯系起來：
- 遠離bug. 如果沒有規格說明，即使是最小的更改都有可能使得整個程序崩潰，改動起來也是很麻煩的。一個結構良好、邏輯明確的規格說明會最小化使用者和實現者之間的誤解，并幫助我們進行靜態檢查、測試、代碼評審等等。
- 易于理解. 一個好的規格說明會讓使用者不必去閱讀源碼也能正確安全地使用模塊。例如，你可能永遠不會去閱讀Python dict.update ，但是通過閱讀對應的聲明性規格說明你就能很好的應用它。
- 可改動性. 一個合理的“弱”規格說明會給實現者一定的自由，而一個“強”的規格說明會給使用者一定的自由。我們甚至可以改變規格說明本身：只要我們是加強了它而不是削弱了它（減弱前置條件或者增強后置條件）。
轉載于:https://www.cnblogs.com/liqiuhao/p/8606687.html
總結
以上是生活随笔為你收集整理的麻省理工18年春软件构造课程阅读07“设计规格说明”的全部內容，希望文章能夠幫你解決所遇到的問題。
- 上一篇： linux验证cuda安装成功_Linu
- 下一篇： 顶级数据库行会Percona阿里全面解析