OO_JAVA_JML系列做業_單元總結

OO_JAVA_JML系列做業_單元總結

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

簡單梳理

如下三者是jml規格里的核心，對一個方法功能和屬性的限制：

1. requires子句：規定方法的前置條件(precondition)；
2. assignable子句：方法的反作用範圍限定；
3. ensures子句：規定方法的後置條件(post condition)。

簡單運用

採用OpenJML工具check第一次JML官方開源庫代碼獲得以下結果：

對比第一次和第二次JML規格官方源碼：

第一次：

/*@ public normal_behavior
      @ requires path != null && path.isValid() && \old(containsPath(path));
      @ assignable pList, pidList;
      @ ensures containsPath(path) == false;
      @ ensures (pidList.length == pList.length);
      @ ensures (\exists int i; 0 <= i && i < \old(pList.length); \old(pList[i].equals(path)) &&
      @           \result == \old(pidList[i]));
      @ also
      @ public exceptional_behavior
      @ assignable \nothing;
      @ signals (PathNotFoundException e) path == null;
      @ signals (PathNotFoundException e) path.isValid()==false;
      @ signals (PathNotFoundException e) !containsPath(path);
      @*/
    public int removePath(Path path) throws PathNotFoundException;

第二次：

/*@ public normal_behavior
      @ requires path != null && path.isValid() && containsPath(path);
      @ assignable pList, pidList;
      @ ensures containsPath(path) == false;
      @ ensures (\exists int i; 0 <= i && i < \old(pList.length); \old(pList[i].equals(path)) &&
      @           \result == \old(pidList[i]));
      @ ensures (\forall int i; 0 <= i && i < \old(pList.length) && \old(pList[i].equals(path) == false);
      @          containsPath(\old(pList[i])) && containsPathId(\old(pidList[i])));
      @ also
      @ public exceptional_behavior
      @ assignable \nothing;
      @ signals (PathNotFoundException e) path == null;
      @ signals (PathNotFoundException e) path.isValid() == false;
      @ signals (PathNotFoundException e) !containsPath(path);
      @*/
    public int removePath(Path path) throws PathNotFoundException;

發現問題根源在於requires判據自己就發生在該方法執行前，\old條件沒法在此應用，由於，requires執行時就已是old的數據了。

(2)部署SMT Solver，至少選擇3個主要方法來嘗試進行驗證，報告結果，有可能要補充JML規格

(3)部署JMLUnitNG/JMLUnit，針對Graph接口的實現自動生成測試用例， 並結合規格對生成的測試用例和數據進行簡要分析

對本身編寫的graph接口的實現類MyGraph運行JMLUnitNG結果是這樣：

➜  src git:(master) ✗ jmlunitng -cp ~/javalib/specs-homework-2-1.2-raw-jar-with-dependencies.jar container/MyGraph.java 
JMLUnitNG exited because of an irrecoverable error: 
org.jmlspecs.jmlunitng.JMLUnitNGError: Encountered 100 compilation errors: 
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:21: 錯誤: 非法的類型開始
    private HashMap<SymPair<Integer>, Integer> edges = new HashMap<>();
                                                                   ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:24: 錯誤: 非法的類型開始
            shortestRoutes = new HashMap<>();
                                         ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:37: 錯誤: 非法的類型開始
        return edges.containsKey(new SymPair<>(var1, var2));
                                             ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:49: 錯誤: 非法的類型開始
        if (!shortestRoutes.containsKey(new SymPair<>(var1, var2))) {
                                                    ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:52: 錯誤: 非法的類型開始
        return shortestRoutes.containsKey(new SymPair<>(var1, var2));
                                                      ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:61: 錯誤: 非法的類型開始
        return shortestRoutes.get(new SymPair<>(var1, var2));
                                              ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:68: 錯誤: 須要')'
        updateEdges(path, this::edgeAddingConsumer);
                              ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:68: 錯誤: 非法的表達式開始
        updateEdges(path, this::edgeAddingConsumer);
                               ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:68: 錯誤: 須要';'
        updateEdges(path, this::edgeAddingConsumer);
                                                  ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:76: 錯誤: 須要')'
        updateEdges(path, this::edgeRemovingConsumer);
                              ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:76: 錯誤: 非法的表達式開始
        updateEdges(path, this::edgeRemovingConsumer);
                               ^
/home/relia/Projects/Java/OO/graph_management/src/container/MyGraph.java:76: 錯誤: 須要';'
        updateEdges(path, this::edgeRemovingConsumer);

...

可見的是，JMLUnitNG至少不支持兩種特性：

1. 泛型的自動推斷特性，在聲明處已經聲明的泛型，在new實例化時，不須要填充泛型類型，編譯器能夠自動推斷，可是JMLUnitNG不支持；
2. 函數式接口的兩種形式都不支持，不管是方法引用的雙冒號，仍是lambda表達式。

不支持上述特性，不可思議其普遍運用。

(4)按照做業梳理本身的架構設計，並特別分析迭代中對架構的重構

第一次做業

說實話，跟大部分人相同，path container採用三個hash map莽到底，規格很簡單，功能很簡單，正確性容易達成。

第二次做業

這個也沒有什麼特點，就是BFS能用，便採用這個算法計算最短路徑了，想必跟大部分人也是大同小異的設計。

正確性方面仍是較爲容易達成的，強測和互測都沒有發現bug。

第三次做業

聯通集計算

經過一個map來保留聯通集的信息，其原理在於單個path內部的連通性是能夠保障的，就能夠在path ID的基礎上創建聯通集，我也是這麼作的，一個pathID映射該path聯通的pathID的集合，這樣，就能夠在線性時間內完成一次path的添加工做，其線性時間，主要依賴path自己的長度，因爲我看見你們都是提到DFS能解決連通性的問題，就這麼設計了，因此，我在這裏大概說一下個人不同的聯通集的設計思路。

做業架構感想

說實話，沒有算法，架構只是紙上談兵，這是我第三次做業的感想，選擇了最樸素的分離解耦的思惟，可是在算法上，複雜度太高，沒有充分考慮可緩存的，沒有充分考慮遍歷的控制，雖然下降了每一個方法的複雜度，但這樣的程序，是沒有實際價值的，換言之，我大部分是作了無用功；

到如今，我也沒設計出本身的完成第三次做業的思路，雖然學習別人的思路是必要的，我仍是想弄清楚，怎樣的緣由致使了個人遍歷沒法達到想要的效果，而後深入理解怎樣設計遍歷算法，這是我想探究的事物。

我對搜索自己有了更深入的理解，所謂遍歷，究其目的，就是尋找要尋找的目標，或者是在肯定的線性集合裏搜索，或者是在有更加特殊的結構的集合裏搜索，爲了完成這個任務，就要有無數優化加入其中，最樸素的，就是排序，排序能夠極大的加快搜索的過程，放在單純的線性集合裏，排序能夠將集合視爲二分集，進行二叉樹上的搜索，達到最高的靜態集合的搜索效率，而在圖結構裏，搜索單源最短路徑，也能夠利用相似的方法，即dijkstra算法，每次根據基礎集合從待選集合中搜索路徑長度最小的一個，加入基礎集合，變相地實現了排序的要求，排序的目的，就旨在濾除不須要的數據或數據集合，將其提早排除，加速搜索的過程。

總的來講，對集合的遍歷操做十分依賴集合自己的結構，沒有排序這樣的優化，計算就永遠是暴力計算，是不可取的。

(5)按照做業分析代碼實現的bug和修復狀況

這個。。第一次有一個bug可是比較隱蔽，強測和互測均未發現，最後是我在第二次做業編寫中發現的，而且就排除掉了，是兩個path compare的函數的錯誤，第二次做業最後經過了強測和互測，沒有發現bug；

第三次做業，至今爲止，我仍是沒有設計出遍歷算法或者遍歷同時計算的算法，保證計算的徹底性的算法，沒有這個，計算出的結果，就不能肯定是最小值。

目前還在思考修復中，也許若是不採用討論區大佬提的拆點算法了話，可能暫時修復不出來。

(6)闡述對規格撰寫和理解上的心得體會

規格是對方法結果的一種約束，能夠做爲需求的一種清晰表述，利於針對其進行規範詳盡的測試，由於結果都用可證實的形式描述出來，因此針對jml規格，能夠採用更加針對性的測試，測試單個函數的功能正確性，並進一步提升junit的測試手段。

有了完善的規格，必定程度上，有利於咱們寫出更加正確的程序，固然，其做用主要仍是測試方面，根據規格能夠更加形式化地驗證，乃至採用自動化地方法生成測試程序，甚至測試數據，這都是可能的。