BUAA_OO 第三單元JML規格編程總結

本單元主要以圖算法問題鍛鍊同窗們按照規格編程的能力，主要考察點在於同窗們對於單元測試的使用和對於JML規則的理解。另外實際編程中存在的難點爲對於圖算法時間複雜度的分析。本次做業我寫的是至關的慘烈。第一次第三次都在測試環節被發現bug，並且錯的都十分低級，只有第二次做業寫的較順利沒有被查出bug。下面我將對本單元進行分析。

 

1、JML知識梳理

1.1 JML語言理論基礎

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

通常而言，JML有兩種主要的用法： （1）開展規格化設計。這樣交給代碼實現人員的將不是可能帶有內在模糊性的天然語言描述，而是邏輯嚴格的規格。

（2）針對已有的代碼實現，書寫其對應的規格，從而提升代碼的可維護性。這在遺留代碼的維護方面具備特別重要的意義。

 

JML主要語法以下:

（1）原子表達式 ：

\result表達式：表示一個非 void 類型的方法執行所得到的結果，即方法執行後的返回值

\old( expr )表達式：用來表示一個表達式 expr 在相應方法執行前的取值

\not_assigned(x,y,...)表達式：用來表示括號中的變量是否在方法執行過程當中被賦值。若是沒有被賦值，返回爲 true ，不然返回 false 

\not_modified(x,y,...)表達式：該表達式限制括號中的變量在方法執行期間的取值未發生變化

\nonnullelements( container )表達式：表示 container 對象中存儲的對象不會有 null

\type(type)表達式：返回類型type對應的類型(Class)

\typeof(expr)表達式：該表達式返回expr對應的準確類型

（2）量化表達式

\forall表達式：全稱量詞修飾的表達式，表示對於給定範圍內的元素，每一個元素都知足相應的約束

\exists表達式：存在量詞修飾的表達式，表示對於給定範圍內的元素，存在某個元素知足相應的約束

\sum表達式：返回給定範圍內的表達式的和

\product表達式：返回給定範圍內的表達式的連乘結果

\max表達式：返回給定範圍內的表達式的最大值

\min表達式：返回給定範圍內的表達式的最小值

\num_of表達式：返回指定變量中知足相應條件的取值個數

（3）操做符

JML表達式中能夠正常使用Java語言所定義的操做符，包括算術操做符、邏輯預算操做符等。此外，JML專門又定義 了以下四類操做符。

子類型關係操做符：E1<:E2，若是類型E1是類型E2的子類型(sub type)，則該表達式的結果爲真，不然爲假

等價關係操做符：b_expr1<==>b_expr2 或者 b_expr1<=!=>b_expr2，b_expr1和b_expr2都是布爾表達 式，這兩個表達式的意思是 b_expr1==b_expr2 或者 b_expr1!=b_expr2

推理操做符： b_expr1==>b_expr2 或者 b_expr2<==b_expr1 對於表達式 b_expr1==>b_expr2 而言，當 b_expr1==false ，或者 b_expr1==true 且 b_expr2==true 時，整個表達式的值爲 true 。

 變量引用操做符：。\nothing指示一個空集；\everything指示一個全集，即包括當前做用域下可以訪問到的全部變 量

（4）方法規格

方法規格的核心內容包括三個方面，前置條件、後置條件和反作用約定。

前置條件經過requires子句來表示： requires P;。其中requires是JML關鍵詞，表達的意思是「要求調用者確保P爲 真」。

後置條件經過ensures子句來表示： ensures P;。其中ensures是JML關鍵詞，表達的意思是「方法實現者確保方法執 行返回結果必定知足謂詞P的要求，即確保P爲真」。

反作用約定用關鍵詞 assignable 或者 modifiable表示 ：反作用指方法在執行過程當中會修改對象的屬性數據或者類的靜態成員數據，從而給後續方法的執行帶來影響。

對於設計中不會對對象狀態改變，於是不會產生反作用；無需提供輸入參數，於是無需描述前置條件的方法，稱爲純訪問方法，使用pure關鍵詞標記。

（5）行爲規格

normal_behavior 關鍵字代表這些規範是針對方法不拋出任何異常時的狀況。

public exceptional_behavior 註釋能夠用來描述拋出異常時的行爲。

案例：

/*@ normal_behavior @ requires (\exists Path path; path.isValid() && containsPath(path); path.containsNode(fromNodeId)) && @ (\exists Path path; path.isValid() && containsPath(path); path.containsNode(toNodeId)); @ assignable \nothing; @ ensures (fromNodeId != toNodeId) ==> \result == (\exists int[] npath; npath.length >= 2 && npath[0] == fromNodeId && npath[npath.length - 1] == toNodeId; @ (\forall int i; 0 <= i && (i < npath.length - 1); containsEdge(npath[i], npath[i + 1]))); @ ensures (fromNodeId == toNodeId) ==> \result == true; @ also @ exceptional_behavior @ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(fromNodeId)); @ signals (NodeIdNotFoundException e) (\forall Path path; containsPath(path); !path.containsNode(toNodeId)); @*/

 

（6）類型規格

類型規格指針對Java程序中定義的數據類型所設計的限制規則，經常使用的是不變式限制和約束限制 。不管哪種，類型規格都是針對類型中定義的數據成員所定義的限制規則，一旦違反限制規則，就稱 相應的狀態有錯。

不變式（invariant P )：invariant 爲關鍵詞，P爲謂詞。要求在全部可見狀態下都必須知足的特性。其中，可見狀態是指，修改爲員變量的方法執行以外的狀態。

狀態變化約束（constraint)：對對象的狀態在變化進行約束的不變式。對前序可見狀態和當前可見狀態的關係進行約束。

 

1.2 JML應用工具鏈

OpenJML：能夠對代碼進行JML規格的語法的靜態檢查，還支持使用SMT Solver動態地檢查代碼對JML規格知足的狀況，所以OpenJML通常也自帶有其支持的JML solver。

JML UnitNG：根據JML描述自動生成與之符合的測試樣例，重點會檢測邊界條件。

總的來講，經過這些工具能夠確保咱們規格實現的正確性，由此肯定咱們過程性的模塊的正確性，進而使咱們對象設計擁有穩定安全的基礎。

 

 

2、SMT測試

嘗試着配置了一下可是一直報錯...

 

 

3、JML測試

 

利用討論區大佬的方法使用testMe檢查了MyPath類中compareto方法，檢查比較是否依照字典序進行，並重點檢查了int型極端比較狀況，防止出現溢出致使判斷錯誤的問題。另外檢查了equals方法，看是否能成功實現路徑是否相等的判斷。

使用過程當中我着實感覺到了單元測試的便利性。以往爲了檢查一個嵌套在深層的函數經常須要絞盡腦汁的設計樣例並思索怎樣才能成功調用到該函數。另外爲了看具體結果經常須要加入大量的print語句，人工審閱判斷。而使用單元測試以後無需費力構造，只需針對要檢測的函數進行測試就好，另外現象也極易看出對不對，真的是十分便捷。

 

 

4、做業架構梳理

此次做業架構自己我寫的仍是不錯的，基本上每次做業都不用對以前已經有過的函數進行什麼更新，只須要額外考慮新增長的函數就能夠。助教說這是由於咱們架構能力增長的緣由，但我以爲咱們每次基本都不用大改以前代碼的核心緣由仍是這幾回做業自己層次感比較強，層層推動，每次都爲下一次作鋪墊。

4.1 第一次做業

 第一次做業較爲簡單，循序漸進寫好了，架構和算法方面沒有任何值得強調的部分。

 

4.2 第二次做業

 第二次比起第一次做業增長了部分難度，開始涉及圖算法問題，但圖算法只在兩個函數中涉及，所以函數自己不須要像第三次做業那樣封裝（第三次做業同一個算法出現了4次），只要在須要時直接使用就好。

 

 

 

4.3 第三次做業

 第三次做業不管是算法複雜度仍是架構複雜度都增長了許多。第一次做業我只有三個類，第二次做業四個類，第三次做業是6個類，同時總代碼量也增長了許多。此次做業最難的三個方法——求最低票價，求最少換乘，求最低不滿意度實際上均可以用迪傑斯特拉算法實現。所以我這三個函數都是用bfs+優先隊列實現迪傑斯特拉算法。

下面是我此次的架構設計：

 

 

 

5、代碼實現bug與修復

慘烈，太慘烈了。這個單元明明感受寫的都挺順的，結果由於許多小錯（好吧，代碼只要錯了就是大錯，不存在大小錯一說，不過從觀感上來講確實感受是小bug）致使分數慘不忍睹，好在終歸從這個慘痛的教訓中學到了一些。下面我將具體說明我每次做業具體犯的錯及修改方法。

5.1 第一次做業

本次做業compare方法中我不是直接比較大小而是對兩個數做差比較，這種比較方式在int邊緣時會發生溢出，致使結果錯誤，而後直接錯8個點60了，最後修改了兩行就改完了。那麼本次做業我或者不少人爲何會作出如此愚蠢的抉擇呢？不用更直觀的大小比較而是選擇作差比較？我認爲咱們都是受到了string類源碼中compare的誤導所致。

字典序比較在string源碼中有包含，源碼compareto實現以下：

public int compareTo(String anotherString) { int len1 = value.length; int len2 = anotherString.value.length; int lim = Math.min(len1, len2); char v1[] = value; char v2[] = anotherString.value; int k = 0; while (k < lim) { char c1 = v1[k]; char c2 = v2[k]; if (c1 != c2) { return c1 - c2; } k++; } return len1 - len2; }

以上摘自源碼。我看源碼後感受這種設計更規範就直接採用了這種設計，卻忽略了String類與Int類不同，string以char爲單位，每一個char換算成int範圍在0-128之間，不存在越界狀況。Int類型卻可能出現越界的狀況。這也提示了我不能迷信源碼，在參考源碼或別人代碼的時候必定要具體狀況具體分析，不少時候兩個狀況儘管十分相近但仍不能直接化用而須要修正。

 

5.2 第二次做業

本次做業程序沒有被查出任何bug，從總體反饋來看此次做業雖然設計存在難度，但設計出來後你們基本都沒什麼錯，所以不進行過多討論。

 

5.3 第三次做業

本次做業設計和算法都沒毛病，可是由於一個筆誤，最後做業連錯6個點，直接70分。即我在迪傑斯特拉算法運行時添加了一個visit數組判斷該點是否出現過以免重複通過一樣的點，以增長效率。該visit數組設計爲HashSet<Node>類型，應該判斷我本身設計的Node類，但我運行時卻使用了另外一個Integer類型變量，致使判斷條件任何狀況都爲錯，判斷失效，程序會不斷通過已經訪問過的點。最後改了把判斷條件給改了一行就修復完畢了。

具體錯誤狀況以下：

畫藍線上面那裏我原本想寫的是Node類型的x，結果筆誤寫成Integer類型begin了。

表面上看這只是個小錯，但卻反映出個人不少很差的編程習慣。這個問題十分低級，其實只要我在寫完後再通讀一遍代碼就能解決，但遺憾的是我並無這樣作，而是在debug階段盯着判斷出錯的代碼塊改，以後也沒再複查。

其實原本這種類型不符合是會有提示的（上面代碼塊begin部分缺失被標黃了），但我設計的時候有問題，最少換乘，最少票價，最低不滿意度三個函數徹底能夠經過調用同一個函數並向裏面傳遞不一樣的參數來處理，但我卻直接將函數在代碼塊裏面實現，大量部分被黃線標記，致使我忽略了begin上面的判斷。這是設計上的大失誤，這也提示我之後必定要儘可能在設計過程當中進行縝密思考，儘可能讓本身寫的代碼知足高內聚，低耦合的設計原則。

 

6、JML規格心得體會

JML的出現仍是十分有必要的。還記得大一上C語言程序設計課時有時咱們會由於題意不清而進行激烈的討論，最後每每是各自嘗試直至一我的過了才能判斷出題意到底想表達的是什麼。而在使用JML後咱們只需仔細閱讀JML描述，即可順利理解題意，不會再出現題意不清的狀況。能夠說，JML這種契約式的編程將架構設計與具體實現分離，有助於實現更優秀的架構，同時底層實現也不受約束。

遺憾的是，JML雖然帶來了不少幫助，可是JML自己使用並不容易。課上實驗時咱們須要本身寫JML，那時咱們所描述的不過是最簡單的函數（好比說add等），但仍然感受比寫代碼自己要困難。另外本單元做業由老師和助教共同商議寫出的JML也常出如今發佈後經同窗反饋進行從新修改的狀況，可見JML是真的很差寫。另外在嘗試使用JML應用工做鏈的過程我也發現JML的配套工具並非很是容易使用，即便有討論區前人栽樹，咱們仍然不容易乘涼。

雖然JML自己應用體驗並非很是好，不過本單元對於JML的介紹確實給我了很大啓發。寫JML意味着撰寫者本人須要對於本身的需求有着充分的理解，在這個過程當中撰寫者進一步改進理解思考本身程序的寫法，避免出現設計性問題。同時JML嚴苛的語法也意味着設計者須要通過縝密的思考才能完成，在這個過程當中撰寫者本人的邏輯也會獲得鍛鍊變得更嚴密。我認爲這種契約式編程思惟自己是十分值得稱道的，這幫助咱們極大程度避免了需求溝通的成本和難度。所以之後也許咱們能夠考慮按照講座課老師介紹的那樣嘗試使用更多的工具來完成設計描述從而幫助他人理解。