2019年北航OO第三次博客總結

1、JML語言理論基礎及其工具鏈

1. JML語言理論基礎

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

1) 開展規格化設計。這樣交給代碼實現人員的將不是可能帶有內在模糊性的天然語言描述，而是邏輯嚴格的規格。

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

2. JML工具鏈

JML是一種語言，那必然須要一些測試工具來檢驗咱們用JML編寫的規格的正確性。JML的測試可使用開源的JML編譯器來編譯含有JML標記的代碼，所生成的類文件會在運行時自動檢查JML規格，若程序未實現規格中的要求，JML運行期斷言檢查編譯器會拋出一個uncheckedException來講明程序違背了哪一條規格。JMLdoc工具與Javadoc工具相似，可在生成的HTML格式文檔中包含JML規範。還有工具JMLUnitNG能夠根據規格的實現自動生成TestNG測試樣例。SMT在形式化方法、程序語言、軟件工程、以及計算機安全、計算機系統等領域獲得了普遍應用。SMT Solver工具能夠以靜態方式來檢查代碼實現對規格的知足狀況。Openjml使用SMT Solver來對檢查程序實現是否知足所設計的規格(specification)。目前openjml封裝了四個主流的solver。z3由Microsoft開發的，並已在github上開源：https://github.com/Z3Prover/z3 其正式發佈版可經過https://www.microsoft.com/en-us/download/details.aspx?id=52270得到。cvc4由Standford開發，能夠經過http://cvc4.cs.stanford.edu/downloads/下載。 

2、JMLUnitNG測試流程

1. 實現文件樹

test --> test.java

執行 jmlunitng test/Test.java

生成新的文件樹

test
├── Test_InstanceStrategy.java
├── Test.java                                      
├── Test_JML_Data
│   ├── ClassStrategy_int.java
│   ├── ClassStrategy_java_lang_String1DArray.java
│   ├── ClassStrategy_java_lang_String.java
│   ├── compare__int_lhs__int_rhs__0__lhs.java
│   ├── compare__int_lhs__int_rhs__0__rhs.java
│   └── main__String1DArray_args__10__args.java
├── Test_JML_Test.java
├── PackageStrategy_int.java
├── PackageStrategy_java_lang_String1DArray.java
└── PackageStrategy_java_lang_String.java2

2. 編譯

1）javac 編譯 JMLUnitNG的生成文件 java -cp jmlunitng-1_4.jar test.java

2）jmlc 編譯咱們的java代碼，生成class文件 openjml -rac test/Test.java

3. 測試

java -cp jmlunitng-1_4.jar test.Test_JML_Test 便可獲得運行結果

3、三次做業架構設計與迭代

1. 第一次做業PathContainer

PathContainer主要是針對path的增刪改查，指令都很簡單也不涉及到算法，而又有運行時間的要求，所以主要爲了鍛鍊咱們對JML的理解和對java中的各類容器的認識。我在MyPath類中採用的arraylist+hashset的方式，arraylist來計算路徑長度，判相等，hashset用於計算distinctNodes.而MyPathContainer中，我採用了雙hashmap，這樣能保證根據path查pathid和根據pathid查path都有相同的複雜度O(1)。

2. 第二次做業Graph

Graph最重要的是出現了圖這個概念，最重要的方法即是判連通和最短路徑。我用了三個類：Vertex類，Edge類和Graph類三個類來存儲圖，每一個vertex有一個linkedlist的屬性來儲存鄰接表，Graph中有一個hashmap來存儲vertex和其對應的nodeId.算法上判連通我用的BFS，而最短路徑因爲邊權值均爲1所以也能夠用BFS來作。因爲圖結構變化指令不多，所以distinctnodes是在每次加入刪除path時計算，詢問時直接返回便可。

3. 第三次做業RailwayStation

RailwayStation是一個實際應用的場景，包括此次做業實現的方法也是與實際生活息息相關的。這讓咱們體會到了從簡單的底層抽象到複雜的實際問題的分析流程。查連通塊個數能夠用多個BFS或者冰茶几，另外三個最低票價，最短換乘，最少不滿意度其實都是雖短路徑問題的變體。最短路徑算法我採用的是時間複雜度爲O(n^2)的dijkstra算法。對於最短換乘，我把每一個Path看做一個節點，若是兩個Path中有相同的PathId則這兩個Path有一條邊相連，而後用BFS便可。而最低票價和最少不滿意度，都是涉及到一個換乘的問題。我採用的是拆點的解決方案，權值賦值成換乘須要增長的便可。

4、Bug分析與修復

1. WA

第9次做業，也是我認爲OO做業有史以來最簡單的一次做業，然而個人強測卻慘遭爆炸，緣由就是個人偏序比較comparable接口的實現錯誤。我對字典序的理解出現了誤差，致使全部不是相同長度的路徑的比較都會產生相反的結果。分析緣由，一是我C語言功底的薄弱，更重要的是我沒有進行充足的測試，沒有用Junit進行單元測試或者與自動生成測試樣例與人對拍。在以後兩次做業我加強了自個人測試於是以後沒有出現正確性的問題。

2. CTLE

第11次做業個人strong15發生了CPU超時的狀況，緣由是忘了寫cache。在用dijkstra算法求解最短路徑的過程當中，其實不止能夠算出要求的最短路徑，還有包含好多的中間結果(好比起點到好多點的最短路徑)。而後，咱們須要作的，就是充分利用好這些本次暫時用不上的中間結果，使得之後的最短路運算被不斷加速（準確的說，這樣的架構下，求解次數越多，後期速度越快）。對於已經求出來的所有最短路結果(不管本次是否用得上)，都做爲邊加入到構建的圖中(後續通過此段的時候，再也不須要一步步算)，並作好標記(對於訪問已有結果的狀況，能夠直接出解)，使得這張圖不斷滾雪球，運算速度愈來愈快,這樣能夠極大的提升程序性能，下降CPU時間。

5、心得體會

1. 規格撰寫與理解

經過這一單元三次做業還有課上的兩次實驗寫下來，對規格也算是有了更深的理解。規格是對開發人員的規範，爲嚴格的程序設計提供了一套行之有效的方法。咱們第三單元經過三節課的學習，瞭解了類規格，方法規格，數據規格的寫法，最重要的是爲何要寫規格。總結來講，類規格定義了與用戶的契約，也定義了開發人員必須聽從的規約。方法規格則由前置條件，後置條件和反作用組成，這是一個方法對實現者的規約。而數據規格則是類有效性的控制條件，constraint和invariant分別定義了數據狀態須要知足的條件和數據修改須要知足的條件。

規格化設計是一種致力於保證程序正確性的設計方法，它本質上是一種設計方法。咱們能夠利用WARRANTY方法來看待規格化設計。

Step1(Why): 爲何須要這個方法？
Step2(Acceptance criteria): 這個方法所提供結果正確的斷定條件是什麼？
Step3(cleaR Requirement): 這個方法是否須要對調用者作出一些要求，從而確保可以產生正確結果？
Step4(ANticipated changes): 這個方法執行期間是否須要修改輸入數據或者所在對象數據？
Step5(TrustY): 無需代碼便可確認其語義

契約式設計是一種基於信任機制+權利義務均衡機制的設計方法學，JML的誕生正是源自於契約式設計的須要。經過本單元的學習，我感覺到了經過規格設計，能夠更容易得到簡潔和職責單一的設計和實現（複雜方法會致使直接寫不清楚相應的規格）。另外一方面，通過實驗和做業訓練會發現，在不少狀況下設計和撰寫規格要比編寫代碼難。一旦規格肯定了，其實實現代碼就變成了一個相對簡單的事情，除非涉及複雜的算法要求。所以，多理解規格使用規格化設計，對咱們從此的軟件開發大有裨益。

2. 想說的話

隨着第三單元的結果，12周OO生涯已通過去了。本學期的OO課程也接近尾聲，本學期OO課程作了很是大的改革，目前看來都是很是成功的，再次感謝老師助教們的付出。最後一單元是UML相關，但願本身繼續加油，給本學期的OO課程畫上一個圓滿的句號。