【面向對象】第三單元總結——JML

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

JML語言理論基礎

JML（Java Modeling Language）是一種行爲規範接口語言，經過使用不會被編譯的註釋形式，和固定關鍵字的語法，指定Java模塊代碼的行爲。這些行爲包括須要知足的前置條件、後置條件，和可能產生的反作用等。它貫徹了契約方法設計理念，經過JML及其支持工具，不只能夠基於規格自動構造測試用例，並整合了SMT Solver等工具 以靜態方式來檢查代碼實現對規格的知足狀況。

JML的語法、關鍵字及其釋義以下所示：

• JML以javadoc註釋的方式來表示規格，有兩種註釋方式，行註釋和塊註釋。其中行註釋的表示方式 爲 //@annotation ，塊註釋的方式爲 /* @ annotation @*/ 。
• @requires 子句定義該方法的前置條件
• @assignment 子句列出該方法能夠修改的類成員屬性
• @ensure 子句定義了該方法的後置條件
• @pure 子句代表該方法無反作用，即僅具備查詢功能
• @constraint 子句定義了狀態變化約束
• @invariant 子句定義了全過程當中的不變式
• \nothing 關鍵詞代表該方法對類成員屬性不進行修改
• \result 關鍵詞表明該方法的返回值
• \forall表達式：全稱量詞修飾的表達式，表示對於給定範圍內的元素，每一個元素都知足相應的約束。
• \exists表達式： 存在量詞修飾的表達式，表示對於給定範圍內的元素，存在某個元素知足相應的約束。
• \sum表達式：返回給定範圍內的表達式的和。
• \product表達式：返回給定範圍內的表達式的連乘結果。
• \max表達式：返回給定範圍內的表達式的最大值。
• \min表達式：返回給定範圍內的表達式的最小值。
• \num_of表達式：返回指定變量中知足相應條件的取值個數。

JML的應用工具鏈：

• OpenJML：OpenJML能夠對含有JML的代碼進行編譯 ，並提供不一樣類型的選項進行檢查。-esc能夠靜態檢查可能出現的隱藏bug，-rac是運行時檢查，-check則能夠檢查代碼是否符合JML規格要求。
• JMLUnitNG：能夠根據代碼中所寫JML規範自動生成測試框架進行自動化測試。

構架設計分析

第一次做業

第一次做業主要是實現一個路徑類Path和一個容器類PathContainer 。

第二次做業是在第一次做業的基礎上實現數據結構類Graph，新增功能包括圖的連通性和查找路徑。

bug與修復

第一二次做業的bug主要是在添加劇復的路徑時，如分別在第一句和第三句添加 add path 1 2 3 / add path 1 2 3，個人做業會把其當成兩條路徑來記錄，即id分別爲1和2。

心得體會

此次做業給我留下了較爲慘痛的教訓，小bug不予以修改，會在以後的測試中很嚴重地影響到正確性。要防微杜漸。