第三單元博客總結
這一單元，主要是進行的JML的使用，以及考察了對於容器，對於算法選擇時候的時間復雜度的控制。
JML的理論基礎和相關工具
JML的核心就是規格和規范，當我們作為設計者想要向開發表達出讓他們做什么的時候，我們往往需要用注釋的方式來進行表述，比如某個類應該有什么變量，干什么，再比如某個方法應該做什么，什么可以變，什么不可以變化，以及對於數據有着特殊的要求等等一系列的要求。我最開始的時候認為如果用自然語言模仿規格進行表述的話，可以有着更好的效果。同樣，最開始作為一個開發者，我或許更加希望能有類似於規格的自然語言描述。
那么問題來了，我們為什么要用一種規范的類似於偽代碼的方式去寫注釋呢？因為只要有了規范，就代表可以自動化驗證，自動化驗證可以避免人思維的死角，能夠從一個更加完整的系統的方法進行規格的驗證，檢測正確性，除此之外，為了進行大規模，批量復雜的驗證，光靠人力去一點一點看注釋解答注釋，或者說，讓測試人員去先讀明白注釋，再去讀明白代碼，檢測是否正確，需要大量的人力和時間。如果機器可以代替我們的工作，當然是最好的。但是機器是死的，只能按照模板按照規矩來解讀，所以我們不得不創造一個約定，讓機器可以識別，但是對於書寫者來說便於書寫，對於開發者來說便於看，最終就誕生了我們的JML。除此之外，自然語言會有各種各樣的歧義，也會導致很大的問題。
JML的核心是用表達式，對於方法規格，類型規格進行控制的一種語言。
這里面就涉及到了三個要素，什么是JML表達式，什么式方法規格，什么是類型規格
注釋的形式為兩種
行注釋和塊注釋。其中行注釋的表示方式為 //@annotation ，塊注釋的方式為 /* @ annotation @*/
（1）表達式
有關於表達式的內容，說白了就是JML的語法的核心內容，這部分在JML手冊里面規定的很詳細了，我這里不再過多贅述，
包括原子表達式，量化表達式，集合表達式，操作符等一系列表達式。這些就是JML語言的基本語法，用這些語句表達出具體的意思。
補充一下，表達式內容特別接近離散數學一里面的謂詞邏輯系列的內容，在有大一離散數學的基礎之上，我們可以不太困難的理解JML的表達式語言
關於表達式的各個內容，比如 \result , \forall , \exist , \max , \min , 等等的東西都是很好理解的
\result表示非void的返回值，
\forall表示全稱量詞，給定范圍，全部滿足約束
\exist表示存在量詞，給定范圍，存在一個滿足約束
\max表示給定范圍最大值
\min表示給定范圍最小值
\not_assigned(x,y,...)括號內沒賦值就是true，反之false
\nothing 表示空集
\everything 表示全集
以上是比較常用的表達式，還有一些不常見的
\product連乘，\num_of求個數等等
唯一一個需要特別注意的是 \old
\old(p.length) 和 \old(p).length 看起來一樣，實際上第一個表示的是變化前的長度，后面表達的是變化后的長度
原因就是，p是一個引用，指向的地址是不變的，也就是 \old(p)=p
但是p.length是一個int類型的數據，所以\old（p.length）代表先前的數字，
我個人認為，究其本質原因，就在於對象在棧里面就是存了一個地址而已
所以對象p內部數據變了之后，\old(p)還是p，然后再查詢或者調用變化之后的p的相關數據與方法
（2）方法規格
方法規格的核心就是，滿足什么條件達成什么樣的結果。特別強調的是，方法規格只規定了滿足什么條件，和產生什么結果。不關心產生結果的過程
在這句核心的基礎之上，生發出來各種各樣的約束，
前置條件（@require）：就是需要滿足什么要的條件才能進行方法，
后置條件（@ensure）：你這個方法做完了要滿足什么結果。
在這里特別提出一下，后置條件只規定了方法結束應該滿足什么，不規定方法怎么執行。
副作用（@assignable）：允許你的方法對什么進行成員修改，不允許你修改的不可以動
在這里補充一下，有一些單獨的訪問方法，即不會對對象的狀態進行任何改變，也不需要提供輸入參數，
這樣的方法無需描述前置條件，也不會有任何副作用，且執行一定會正常結束。對於這類方法，可以使用
異常（@exceptional_behavior，@signal）：滿足什么條件，需要你去拋出什么樣的異常（使用signal 標注出異常類型）
由此可見，方法規格，或者叫JML的核心，就是調用方法如果滿足A條件，必須得到B結果，怎么得到結果？我不關心，那是開發者的事情。
（3）類型規格
類型規格的核心是變於不變，
不變式（invariant）就是告訴你，在方法執行前，完成等可見狀態下某種數據變量的要求。
與之相對的約束就是狀態變化約束（constraint），如果要變化，怎么變，描述變前變后的關系。
有關JML的工具有很多
如， 使用OpenJml檢查JML規范性
如， 使用SMT Solver檢查等價性
如， 使用JMLUnitNG自動化生成數據測試
JML相關工具的使用
說到JML相關工具使用，可以說一把心酸，工具的不成熟，JDK版本的不對勁，還有各種各樣的神奇bug的出現，導致了一些工具可以使用，而有一些的工具在我的電腦之上完全無法運行。
在查閱了各種各樣的資料之后，無論是同學的幫助，還是網上教程，還是學長往屆博客，我的工具問題還是沒有解決，我就只能簡單的說一說我使用過的工具。
注意：一定要用jdk8，不然瘋狂報錯！！！！！！！！！！！！！！！！！！
（1） openjml與solver
執行語句：java -jar .\openjml.jar -exec C:\Users\73939\t\Solvers\z3-4.7.1.exe -esc C:\Users\73939\t\*.java
JML域和Java域不能重名，所以完全沒法弄，修改的話也設計很多亂七八糟的東西
比如JML里面的Person [ ] people在不同方法里面映射到不同的容器，如hashset，hashmap，arraylist等
還有什么繼承的原因，以及各種各樣的bug，找不到文件之類的。
就會導致一系列問題，所以我放棄了直接測試，選擇分段測試，只測試幾個能成功運行的函數
import java.math.BigInteger;
public class Person {
public int id;
public String name;
public BigInteger character;
public int age;
public Person[] acquaintance;
public int[] value;
//@ ensures \result == id;
public /*@ pure @*/int getId() {
return id;
}
//@ ensures \result.equals(name);
public/*@ pure @*/ String getName() {
return name;
}
//@ ensures \result.equals(character);
public /*@ pure @*/BigInteger getCharacter() {
return character;
}
//@ ensures \result == age;
public/*@ pure @*/ int getAge() {
return age;
}
/*@also
@ public normal_behavior
@ requires obj != null && obj instanceof Person;
@ assignable \nothing;
@ ensures \result == (((Person) obj).getId() == id);
@ also
@ public normal_behavior
@ requires obj == null || !(obj instanceof Person);
@ assignable \nothing;
@ ensures \result == false;
@*/
public/*@ pure @*/ boolean equals(Object obj) {
if (obj != null && obj instanceof Person) {
return (((Person) obj).getId() == id);
} else {
return false;
}
}
/*@ public normal_behavior
@ ensures \result == name.compareTo(p2.getName());
@*/
public /*@ pure @*/int compareTo(Person p2) {
return name.compareTo(p2.getName());
}
}
這是非常簡單的魔改版demo，簡單測試了一下
一些警告問題不大，沒有錯誤，不需要過多擔心。
但是這只是個demo，我的主要函數想驗證特別困難，幾乎無法實現，報錯信息也沒什么價值，就不貼出來了。
除此之外，我最想驗證的幾個方法，如同最短路徑，強連通，連通之類的方法，由於openJML似乎不支持對於 （forall int [] path）之類對於數組的判斷，加上我本身使用的各種hashmap，hashset，以及為了滿足算法規定增加的若干變量，都沒法進行有效的進行openJML的判斷 。
到這一步我覺得，如果我為了穿鞋，把腳砍去一半的話，完全體現不出這個博客的意義，所以我在這一步選擇了放棄
至少我覺得，如果讓程序員拋棄程序效率，拋棄程序簡潔度，甚至說是拋棄程序能否滿足課程組要求（算法時間之類的），去滿足一個比較低下的工具，我真的覺得本末倒置。
（2）JMLUNITNG相關測試
在用這個工具之前，我是滿心期待的，這也太爽了吧，我不用對拍了，不用自己寫測試代碼了
但是我看到一片夾雜的FAILED和PASSED之后，我整個人是完全無語的，
由於實際實現和規格差別過大，瘋狂報錯，我就為了成功測試Group類，只能先魔改了一下，然后順便寫了一個demo作為測試
魔改版的代碼把arraylist換成了數組，可以符合規定
測試結果如下：
（補充一下，del函數也過了測試）
（魔改版刪除了一些我自創的函數，只保留了有規格的函數）
group里面的函數沒有什么傳參數的，這個包就是靠着傳奇怪參數進行測試，所以有一些函數通過了，比如直接返回的函數
hasPerson由於不會出現null，和預計也是一樣的，所以falied了
但是怎么解釋其他的Falied呢？我仔細分析，發現我的動態維護方法不適合這個包進行測試。
我測試的時候沒有加main函數，也沒有加network，導致加人的時候，一些方法沒有被調用。
因為我的這個類利用的是緩存機制，沒有外界同步的進行更新，只有單純的針對一個方法來回測試，就會導致那些getRelationsum，getValuesum等函數失效
原因就是：單獨測試一個函數不一定能保證正確，因為缺少之前添加的很多步驟，尤其是需要network調用這里面的函數更新緩存
換句話說，我因為用的是緩存機制，必須進行完整的指令驗證，而不是給定一些數據，計算出結果
我需要從network里面加入之后，在network層次調用函數，更新新的valueSum和relationSum
顯然，據我的觀測，這個包就是給出一些數據然后判斷結果
但是我的動態維護做法必須要求，這些數據每一次出現都是指令產生的，而不是隨意給出來的，
用最簡單的話來說就是，你想測試這個組里面有三個人時候的平均值，那么必須要一步一步用指令加入三個人，再運算
而不是直接給出三個人，調用函數計算出結果。
這和方法實現有關，同時也是這個測試包本身的限制
一言以蔽之，這個包不適合檢查一些動態維護方法，原因就是動態維護需要完整的數據生成過程，每一次進行更新
但是這個包就是給你一些數據，利用函數進行計算而已，它要你的函數返回計算結果，要求無論何時都是計算出來的。
但是顯然，課程組要求記憶化，要求動態維護減少復雜度，這個包特別不適合進行驗證
這可能是我的猜測，為了驗證我的猜測，我深入研究了評測機制
為了深入研究這個包的評測機制，我又寫了個demo跑了一下，然后發現這個評測包局限性很大
package test; import java.math.BigInteger; public class Person { public int id; public String name; public BigInteger character; public int age; public Person[] acquaintance; public int[] value; //@ ensures \result == value[i]; public int getValue(int i) { return value[i]; } //@ ensures \result == id; public int getId() { return id; } //@ ensures \result.equals(name); public String getName() { return name; } //@ ensures \result.equals(character); public BigInteger getCharacter() { return character; } //@ ensures \result == age; public int getAge() { return age; } /*@ also @ public normal_behavior @ requires obj != null && obj instanceof Person; @ assignable \nothing; @ ensures \result == (((Person) obj).getId() == id); @ also @ public normal_behavior @ requires obj == null || !(obj instanceof Person); @ assignable \nothing; @ ensures \result == false; @*/ public boolean equals(Object obj) { if (obj != null && obj instanceof Person) { return (((Person) obj).getId() == id); } else { return false; } } /*@ also @ public normal_behavior @ ensures \result == name.compareTo(p2.getName()); @*/ public int compareTo(Person p2) { return name.compareTo(p2.getName()); } public static void main(String[] args) { System.out.println("hello") ; } }
然后輸入命令
java -jar jmlunitng.jar test/Person.java
javac -cp jmlunitng.jar test/*.java
java -jar openjml.jar -rac test/Person.java
java -cp jmlunitng.jar test.Person_JML_Test
貼圖如下
完全不是隨機測試
它就是給你的方法輸入一些“隨機”參數，輸入，告訴你Passed還是Failed
之后我又測試了幾個demo，發現了神奇的事情，數據長得一模一樣
如果參數是int，就給你輸入0，int最大值，int最小值
如果參數是對象，就給你一個null進去
之后進行排列組合，進行測試
Passed和Failed的標准似乎是你的程序會不會出現類似於讓程序中斷的異常
但是新的問題來了，為什么我前面的一些get系列函數會Failed了呢？
如果只是根據異常判斷對錯的話，理論上get系列函數不會出問題啊？
我前幾個fail是因為結果錯了還是異常錯了？
換句話說，這個東西到底能不能利用JML語言判斷返回值是多少，我陷入了懷疑
我覺得作為一個工具，不能，至少不應該只靠異常判斷正誤，所以我又寫了一個demo
//@ ensures \result == 0; public int getZero(int x) { System.out.println(people.length); return 1; } //@ ensures \result == 1; public int getOne(int x) { return 1; }
結果如下
發現這個測試代碼是可以根據我的JML判斷代碼的對錯的
也就是說，他不是單純的極端測試數據測試異常，是可以根據JML判斷返回值正確性的！！！
至此，我覺得已經清晰明了了，
仔細觀察輸出發現三個問題：
（1）測試一個函數不會調用其他函數
（2）測試數據隨機生成，而非按照我們要求調用add函數生成
（3）測試參數過於單一
對於有參數的數據：帶入極端參數，根據類加生成數據，進行JML結果驗證
對於無參數的數據：根據類生成一定數據，進行一定檢驗，進行JML結果驗證
到了這一步，已經驗證了我前面為什么failed了的猜想
和我的猜想一模一樣，就在於里面的People數組是隨機生成的，不是調用add函數加入的，沒有同步更新緩存
總而言之，Failed原因：測試包根據類的數據隨機生成people，沒有從network級調用更新動態維護的數據，也沒有走addPerson渠道更新動態維護數據，導致用來緩存的數據 ，不能被及時更新。在函數返回值和根據JML計算值比較的時候，由於返回值並沒有在這一次測試的時候更新過，所以出現了錯誤，導致了Failed。
到此為止可以說是完美破案了
說實話，課程組以及規定了各種異常處理方式，各種數據的限制
很多測試做的無用功，求年齡在-2147483648到0之間的人。。。
總而言之，這個方法只能判斷極端條件下的異常，和少數情況下JML的正確性
說實話，限制挺大的，不適合我們這次這種強制在線類型的作業。
（3）JUNIT系列
這個系列是典型的測試，有着完備的工具，規范簡單的使用方法，也是我進行測試的主力，但是這個和JML怎么搭配呢？
由於上述工具基本對我都是沒有幫助的收益，我只能利用JUnit和自己寫其他函數的方式，來模仿一個我希望的“JMLUNIT”“openjml”的功能
我希望有一個測試方法，完全按照規格，只判斷滿足條件之后的結果
所以我就相當於在測試代碼翻譯了JML語言后置條件，進行比對操作等等。
總而言之，JML本意是節省人力和時間，但是使用出來之后，卻造成了沒太大意義的結果
說實話，這不是JML的問題，這是不成熟工具鏈的問題，我們要給JML工具鏈發展的時間
我只能說，在現在這個時間段，JML的這幾個工具沒法高效率投入工作生產甚至課后作業里面發揮很大的良性作用，
這一系列的工具，目前頂多是跑一跑demo，給一點小的提示防止遺漏判斷，完全不能滿足JML希望的“用規格保證正確”的這種目的。
三次作業架構設計
第一次作業
第一次作業架構很簡單
總體來說，沒什么好的架構，在當時的時間內，我還處於認為JML規格就是方法執行步驟的階段
（1）架構設計
JML用的數組，我就用arraylist
（2）算法分析
JML用循環遍歷，我也循環遍歷
第一次作業唯一一個難度，就是判斷兩個點是不是直接可達的，這里用到了一個dfs函數，沒有更多復雜的東西了
dfs就是簡單的遍歷每個人相鄰的人，還要給訪問的人標記訪問
標記訪問的方法我采用了hashmap，person為索引，（0/1）代表訪問與否作為值
第一次作業由於測試很弱，我這種無腦循環的方式可以沒有任何bug的通過中測，強測，拿到滿分
當時我還以為照着規格翻譯就好了，然后第二次作業釀成了大禍
（3）復雜度分析
Myperson復雜度
Mynetwork復雜度
總的來說，不復雜，就是有幾個循環而已
第二次作業
第二次作業和第三次類圖是一樣的
總體結構很簡單，因為架構是課程組規定好的，不需要我大幅度更改
（1）架構變化
我做的最大的改變就是：使用hashmap和arraylist結合的方法，
因為hashmap方便取，方便判斷存在，但是不方便遍歷，而arraylist剛好可以補充遍歷困難的弱點，所以我通過兩種方法一起使用，相互補充，最大限度減少時間開銷，也讓代碼更加簡潔。
當我判斷存在的時候，我就調用hashmap，id為索引，person為值
當我遍歷的時候，我就取arraylist，更加簡單直接
（2）算法改變
我前面說過了，第二次實驗，我最開始是無腦的按照規格進行的雙循環遍歷，
在10w條指令的轟炸之下，出現了巨大的問題，所以我使用了緩存機制
緩存機制也很簡單，觀察所有算法里面，只有兩個函數是O（n*n）的，那就是group里面的getRelationSum()和getValueSum()兩個函數
使用雙循環直接超時
但是仔細觀察這個函數，發現有竅門，可以在每一次加入group的時候更新一次，在每一次加關系時，可能更新一次
所以我進行了更改，先是加人的時候和組里面所有人比對，如果有link的人，就更新relationsum和valuesum
除此之外，還要加上relationsum的自圈數。
但是，有個巨大的問題，那就是當兩個人先加入group再加關系的時候，難以直接通過已經有的函數進行更新
那怎么辦呢？我選擇了犧牲封閉性的方法，額外加了個方法，允許外界更新relationsum，valuesum，那就是加關系的時候判斷兩個人都在組里面的話，就更新這個組的有關數據
總的來說，這次在JML不代表方法運行方式上面這一點吃了大虧，因為超時出了問題。
（3）復雜度分析
這一次，MyPerson沒有變化
MyGroup復雜度
MyNetwork復雜度
所有復雜度在於添加關系上面。和預想的一樣，但是這樣子會減少超時的錯誤，所以是合理的復雜。
第三次作業
第三次作業是這一單元靈魂所在，雖然我的方法最終還是超時了，但是我個人認為，我的一些方法有着很好的借鑒意義。
（1）架構變化
這次為了管理人和錢的關系，使用了hashmap，id為索引，money為值
為了計算最短距離，增加了二維數組，記錄兩個點之間最短距離，增加關系時動態維護
同時，為了找到每個人對應數組的位置，增加了hashmap，id為索引，在數組位置為值
（2）算法分析
這次的增加了從組里面刪除一個人，就是增加一個的鏡像操作，把加改成減，利用緩存更新就可以了，問題不大
至於增加的年齡范圍的人數，借錢，判斷一個人錢多少這種操作，就不提了，因為是很簡單的一次遍歷或者不用遍歷的操作。
這次主要三個大難點
第一，最短路徑
最短路徑我使用了一個矩陣記錄任意兩個點之間最短距離，再添加一次關系的時候，更新所有點的最短距離
當調用函數計算最短距離的時候，就是一次二維矩陣的讀取操作，是O（1）
但是問題來了，更新最短距離的時候，是一次O（n*n）的操作，特別浪費時間，也是我超時+被hack的直接原因
這一部分內容會在bug里面詳細展開
思路就是，最開始所有人之間距離無限大，每次添加關系，如果兩個人之間最短距離大於加入的關系，就更新最短距離
如果更新了最短距離，就會進行二重循環遍歷，遍歷任意兩個點的最短距離會不會因為這條邊距離的變化而變化，
由於終點和起點都需要包括所有點，所以復雜度數O（n*n）
第二，強連通
強連通我使用了課程組給的方法，如果兩個人不是直接連接，就采取每次刪除一個人，遍歷刪除所有人的每一個，之后判斷起點終點是否可達的方法
如果兩個人因為刪除一個人無法連通，就不是強連通。
但是有一個問題，那就是兩個人直接link的時候，這種做法是無效的
所以這種情況需要特殊判斷，就是遍歷起點所有的相鄰結點，如果起點的相鄰結點（除去終點）有一條不經過起點可以到達終點的路徑，那就是強連通的
所以做法分兩個分支，直接相連和不直接相連，復雜度都接近O（n*n）
第三，連通塊數
使用雙循環一定暴斃，所以我用了緩存技術，每次加入一個人，就blocksum加一，每次加入一個關系，如果加關系的兩個人之前不是可達的，
那就blocksum-1，代表兩個塊變成了一個塊
這個方法是我覺得的最簡單也是最省時間的方法
由於我的最短距離矩陣存在，所以我的isCircle是O（1），所以這個方法也不復雜
（3）復雜度分析
總的來說，這一次我把所有復雜度丟給了addrelation上面，導致了方法臃腫，時間緩慢。
這是network的復雜度，所有復雜度堆在了stronglink和addrelation上面，和預料一致
現在反思，應該降低單個方法復雜度，使用堆優化方法的迪傑斯特拉算法，計算最短路徑。
MyGroup的復雜度也沒大的變化
這一次作業嘔心瀝血，擔心自己會強測0分，但是結果比想的好了不少，雖然錯了幾個點，也被hack一次，但是可以接受了
畢竟當時只能想到O（n*n）的方法了，是自己能力不足導致的。
bug實現和修復
第一次，沒有bug，
課下進行了大量測試檢查正確性
同時我還使用了大量偽JUnit代碼進行了測試
都沒有發現特別大的問題，也順利拿下了第一次滿分
互測階段，大家寫得基本是一個模子刻出來的，所以沒什么測試必要性，
拍了一些沒發現大的問題，就沒繼續管
但是在課下階段，我最大的問題是isLink函數的實現，想當然認為自己和自己之間不是link的，沒有管規格語句，還好及時在課下階段發現
好幾個人，因為這個函數的問題，強測0分
同樣的，還有dfs，bfs不標記循環到死的，也在強測拿了0分
這些我在課下都遇到了，也解決了，出現這個問題就是課下不到位，沒看規格
第二次，超時bug
這次就是方法完全按照規格后置條件造成的錯誤
沒記憶化，沒緩存，無腦循環，不去考慮時間問題
是我這次最大的失誤
解決方案就是前文描述的那樣，增加緩存機制
組里加人的時候更新，加關系的時候如果在同一組就給這個組更新
很成功的兩次解決兩個bug。
hack別人也是hack這兩個函數，失敗了
第三次，超時bug
如同前文所言，所有復雜度堆在了addrelation上面，被人使用addrelation多次給hack了
強測也因為這個問題掛掉了四個測試點
解決bug的方法要完全重構代碼，從isCircle，minpath，stronglink到之前若干函數
都要進行大大小小改動調整，截止到寫博客這一天，bug還沒修理
預計使用堆優化迪傑斯特拉方法修理bug
心得體會
（1）對於JML的用途感悟
經過這一單元，我對於規范化有了更加深刻的認知，雖然因為openjml工具出了問題，導致我的一些驗證失敗了，但是這個小插曲並不能阻擋我對JML的贊賞。
同樣是注釋，如果別的課也可以用這種注釋給大家進行方法規格的注釋，開發者的任務量就會少很多，而且更容易傳達相應的信息，防止各種各樣的歧義，防止自然語言的一些死角。
自然語言往往為了消除歧義追加內容
然后為了消除追加內容的歧義追加新的內容
再之后每次修訂很可能是在改正上一次歧義導致的錯誤，而不是本身的問題
但是JML語言消除這種歧義，讓注釋簡單易懂，直接了當。
（2）對於JML本身的理解
對於理解JML語言而言，我也有了很高的進步
第一次作業我是忽視JML，按照自己的性子寫，覺得差不多就沒管
第二次作業我是誤以為后置條件是方法執行過程，導致出現了tle
第三次作業是我個人算法設計問題導致了超時，但是完美對接了JML規格，有着很大的進步
多次作業下來，我對規格有了更加深刻的認識，雖然自身代碼功底有一些不足，一些算法沒實現成功，但是我深刻感受到了讀懂規格，遵守規格是一種什么感受，感覺有了規格的幫助，寫起代碼心里就有了保底，有了底氣，只要我滿足規格，我就是對的。
規格核心就是，允許你改什么數據，怎么改數據，滿足條件達成什么結果
但是規格不關心你取得結果的方法，只關心更改之后的結果是什么樣子，以及更改之后的結果和之前應該有什么關系
這種看似鎖定但是很自由的規格，真的讓我收獲很多。
（3）對於java語言的掌握
對於容器選擇，對於算法把握，對時間復雜度的分析，
不同容器的不同好處相互結合降低時間，
都是我這個單元很重要的收獲
最后，再次強調，雖然openjml沒法實現生活中大部分工作和作業要求，但是這不代表JML是有問題的，這種想法，一定會隨着工具鏈逐漸成熟，一步一步深入到軟件設計和開發之中。