OO第三單元總結--根據JML寫代碼

一. JML語言

1. 理論基礎

　　首先，JML不是JAVA的一部分，它是一羣研究者爲JAVA設計的擴展部分，但尚未獲得官方的支持。所以，JAVA編譯器並不支持JML，因此要想JML起做用，只能採用相似openJML這樣的第三方來編譯，將JML 規格編譯爲運行時檢查的語句，即RAC code(runtime assertion checking)。若是代碼實現與其JML規格不一致，將引起運行時JML exception。

　　JML聽從契約式設計範式(DBC)，Design by contract是軟件開發的一種方法，核心是類與其客戶之間達成契約。JML是一種形式化的、 面向 JAVA的行爲接口規格語言。

　　推薦一篇step by step以一個比較複雜的例子來說解JML語法和設計的教程：https://www.ibm.com/developerworks/library/j-jml/

2. 應用工具鏈

• jmlrac: test for violations of assertions during execution
• ESC/Java2: static verification; compile-time proving that contracts are never violated
• jmldoc: javadoc-style documentation
• jmlc: assertion-checking compiler
• jml4c: a new JML compiler built upon the Eclipse JDT open-source platform

　　上述工具不少都已經再也不維護（跟不上java的升級，大多支持到java 1.5）, 看你們抱怨openJML坑，就想找找有沒有更好用的JML工具，結果發現openJML居然是最好用的。

• openJML：目前對JML支持最好，維護最積極的JML編譯器了 
• jmlunit/jmlunitNG: unit testing tool

二. 部署SMT Solver

　　maven+openJML+Eclipse試了一下午仍是報錯，命令行沒試過，不知道怎麼樣，這一部分只好放棄了。

二. JMLUnitNG

　　下述過程可復現，代碼和運行結果是一致的，若是有興趣，能夠參照個人步驟在本地試一試。

　　配置過程參見討論區https://course.buaaoo.top/assignment/71/discussion/199  ，爲了保證配置成功，我也是在Linux下配置。

 　　Graph接口方法的規格幾乎所有含有 \exists 或 \old，根本搞不了，因而只能退而求其次，去驗證Path類。Path類裏面的\sum等語法也不支持，因而我就模仿MyPath，寫了個比減法稍複雜的demo。

 1 // yifan/MyPath.java
 2 package yifan;  3 
 4 public class MyPath {  5     private/*@ spec_public @*/ int[] nodes;  6 
 7     public MyPath(int[] nodeList) {  8         nodes = new int[nodeList.length];  9         for (int i = 0; i < nodeList.length; i++) { 10             nodes[i]=nodeList[i]; 11  } 12  } 13 
14     //@ ensures \result == nodes.length;
15     public /*@pure@*/ int size() { 16         return nodes.length; 17  } 18 
19     /*@ requires index >= 0 && index < size(); 20  @ assignable \nothing; 21  @ ensures \result == nodes[index]; 22  @*/
23     public /*@pure@*/ int getNode(int index) { 24         return nodes[index]; 25  } 26 
27     //@ ensures \result == (nodes.length >= 2);
28     public /*@pure@*/ boolean isValid() { 29         return nodes.length >= 2; 30  } 31 
32     public static void main(String args[]) { 33         return; 34  } 35 }

    運行過程 step-by-step：

./jmlunitng yifan/MyPath.java javac -cp jmlunitng.jar yifan/**/*.java ./openjml -rac yifan/MyPath.java javac -cp jmlunitng.jar yifan/MyPath_InstanceStrategy.java java -cp jmlunitng.jar yifan.MyPath_JML_Test

運行前目錄

 

運行後目錄

 運行結果

結果討論

• MyPath(null)，MyPath.java中會調用length，錯誤，意料之中；
• 明明已經requires index>=0了，爲何生成的測試例子裏還會有負數？就算剛開始nodes=new int[10]，避免nodes爲null的狀況仍是這種結果；
• 彷佛JmlUnitNG只會生成int的邊界值和0，無論requires? 這只是個人猜測。

有個問題須要討論一下：

• 爲何不寫成

//@ public instance model non_null int[] nodes;
    private ArrayList<Integer> nodes;

        openJML會把規格和實現裏的nodes當成一個nodes，會報錯。

        那這麼寫不就好了嗎？

//@ public instance model non_null int[] nodes;
    private ArrayList<Integer> myNodes;

        非也，會報下述錯誤

yifan/MyPath.java:6: 警告: JML model field is not implemented: nodes
    //@ public model int[] nodes;
                           ^

        nodes沒實現？對的。要想解決這個問題，就得寫抽象函數，能夠看看這篇論文https://digitalcommons.utep.edu/cgi/viewcontent.cgi?referer=https://www.google.com.hk/&httpsredir=1&article=2073&context=cs_techrep ，我大概寫了個抽象函數，沒bug，但也沒起做用，仍是報nodes沒實現的錯誤，因此這裏就不貼個人抽象函數了。

從上圖能夠看到若是不實現nodes，大多數方法都被skip掉了。

 

三. 架構設計

1. 第一次做業

 直接繼承接口，簡單地實現了兩個類。

2. 第二次做業

 

 爲了更改方便，直接ctrl+v把MyPathContiner的代碼複製到MyGraph。

3. 第三次做業

 

因爲第二次做業比較複雜，再去動極可能出bug，因而在寫第三次做業的時候對於第二次做業已有的代碼我一行都沒動，只是在MyGraph類里加了求連通塊個數的Public的函數。這樣一來bug少了，但新加的架構和已有的架構看起來很不協調。

看了std碼以後，驚呼：我以前竟將全部代碼都直接放在src文件夾下。好的分層設計應該像標程同樣，起碼得有多個文件夾吧，好比base,core,util,grpha等。

四. bug和修復狀況

三次做業均無bug。

五. 心得體會

撰寫：規格的撰寫用到了不少離散數學的知識，掌握常見的幾種模式後，就可以比較容易地寫出一些簡單函數的規格。以我目前的水平看，寫代碼仍是要比寫規格來得容易。

理解：實操中，我其實是先看的指導書，對於含混的地方，（好比起點和終點相同的狀況下，算不算換乘，最小費用算多少？同一路徑中若是有環該怎麼算？）我會去詳細閱讀規格，由於規格嚴謹的描述了某一個方法該幹什麼。（但此次直覺上的理解實際上更靠譜，好比同一路徑中有環的狀況，直覺上的理解是不用非得繞着環走一圈多餘的路，但死扣規格，確實得繞，過後證實是老師或助教的規格寫錯了）。

JML和JmlunitNG：JML設計指望過高，其目的是寫出規格後，就能夠自動生成測試用例，還可直接檢查代碼是否準確實現了規格；但相關工具鏈及其難用，功能及其有限，目前我只能寫個簡單的demo探索一下它的性質，體驗一下整個流程。