OO第三次單元總結

OO第三次單元總結

前言

第三單元的三次做業：JML規格化編程。根據已給的JML規格語言給出代碼實現。

梳理JML語言的理論基礎、應用工具鏈狀況

JML(Java Modeling Language)是用於對Java程序進行規格化設計的一種表示語言。JML是一種行爲接口規格語言（Behavior Interface Specification Language，BISL），基於Larch方法構建。BISL提供了對方法和類型的規格定義手段。所謂接口即一個方法或類型外部可見的內容。JML主要由Leavens教授在Larch上的工做，並融入了BetrandMeyer， John Guttag等人關於Design by Contract的研究成果。近年來，JML持續受到關注，爲嚴格的程序設計提供了一套行之有效的方法。經過JML及其支持工具，不只能夠基於規格自動構造測試用例，並整合了SMT Solver等工具以靜態方式來檢查代碼實現對規格的知足狀況。

理論基礎

JML以javadoc註釋的方式來表示規格，每行都以@起頭。有兩種註釋方式，行註釋和塊註釋。其中行註釋的表示方式爲 //@annotation ，塊註釋的方式爲 /* @ annotation @*/ 。
方法規格的核心內容包括三個方面，前置條件、後置條件和反作用約定。其中前置條件是對方法輸入參數的限制，若是不知足前置條件，方法執行結果不可預測，或者說不保證方法執行結果的正確性；後置條件是對方法執行結果的限制，若是執行結果知足後置條件，則表示方法執行正確，不然執行錯誤。反作用指方法在執行過程當中對輸入對象或 this 對象進行了修改（對其成員變量進行了賦值，或者調用其修改方法）。
\result表達式：表示一個非 void 類型的方法執行所得到的結果，即方法執行後的返回值。\result表達式的類型就是方法聲明中定義的返回值類型。
\old( expr )表達式：用來表示一個表達式 expr 在相應方法執行前的取值。該表達式涉及到評估expr 中的對象是否發生變化，聽從Java的引用規則，即針對一個對象引用而言，只能判斷引用自己是否發生變化，而不能判斷引用所指向的對象實體內容是否發生變化。
\forall表達式：全稱量詞修飾的表達式，表示對於給定範圍內的元素，每一個元素都知足相應的約束。
\exists表達式：存在量詞修飾的表達式，表示對於給定範圍內的元素，存在某個元素知足相應的約束。

應用工具鏈狀況

openjml：使用SMT Solver來對檢查程序實現是否知足所設計的規格。目前openjml封裝了四個主流的solver：z3, cvc4, simplify, yices2。
JMLUnitNG/JMLUnit：根據規格自動化生成測試樣例，進行單元化測試。

按照做業梳理本身的架構設計

第九次做業

類圖：

複雜度分析：

第十次做業

類圖：

複雜度分析：

闡述對規格撰寫和理解上的心得體會