method/function spec -- 如何寫好 JavaDoc

寫Java寫了那麼久，一直不知道怎麼寫JavaDoc會比較好，最近剛好在看MIT的線上課程，其中有關於function/method規格的部份，發現如果依據這種方式來寫的話，既可以清楚的表達function/method的行為，又不會把太多的實作細節寫出來，是一個很好的寫JavaDoc的格式。

規格定義

規格同時定義了使用者以及實作者雙方的責任 -- 在使用者滿足規格中所定義的條件下，實作者保證能達到規格中要求的結果。

一個function/method的規格，包含了三個部份

• precondition -- 一般用關鍵字 requires來表示
• postcondition -- 一般用關鍵字 effects來表示
• frame condition -- 一般用關鍵字 modifies來表示

precondition 規範了使用者的責任，如果precondition中的條件沒有滿足的話，實作者可以用任意的方式來完成實作 (包含終止整個程序)。

postcondition 則是規範了實作者的責任，在precondition滿足的條件下，實作必需要滿足postcondition中所規範的條件。

frame condition 和 postcondition有關，讓寫規格的人能夠比較簡單、清楚的表達其他的 postcondition。在frame condition中必需明確指出其他會受要變動的物件，所有沒有列在frame condition中的物件，預設狀態都是靜態的，也就是在function/method執行期間，不會受到任何改變。

不同的軟體規格寫法

規格的寫法可分為兩大類: operational specification 跟 declarative specification，虛擬碼就是 operational specification最常見到的做法。declarative specification 並不明確定義實際達行的步驟，而是把執行前後的狀況明確的定訂下來。

在大部份的狀況下，declarative specification是比較好的寫法，因為他比較短，比較容易了解，更重要的是，declarative specification 不會提到實作的細節，讓實作的人有更大的空間，也避免使用者過度依賴特定方式的實作。

規格的強度

A specification A is at least as strong as specification B if

• A's precondition is no stronger than B's
• A's postcondition is no weaker than B's, for the stats that satisfy B's precondition

規格的強度，在考慮繼承的時候，更能顯示出他的重要性。