面向對象第三單元做業總結

面向對象第三單元做業總結

JML語言和工具鏈

JML的基本語法

契約式設計或者Design by Contract (DbC)是一種設計計算機軟件的方法。這種方法要求軟件設計者爲軟件組件定義正式的，精確的而且可驗證的接口，這樣，爲傳統的抽象數據類型又增長了先驗條件、後驗條件和不變式。這種方法的名字裏用到的「契約」或者說「契約」是一種比喻，由於它和商業契約的狀況有點相似。

在契約式設計的背景下， JML(java model langauge)爲契約式設計提供了支持。
jml的規格放在了註釋裏， // /* */ 來表示一些規則
\requires子句定義了方法的前置條件， 也就是程序運行前須要知足的條件
\ensures 子句定義了方法的後置條件， 也就是程序運行後須要知足的條件
\result 表明了方法執行的結果
\old(expr) 表明了表達式expr在方法執行前的值
\forall 對於給定範圍的元素， 應知足條件
\exist 存在範圍內的元素， 知足條件
\signal 用於拋出異常
\constraint用於限制對象轉檯的變化
\invariant 可見狀態下都必須知足的特性

openjml的使用

經過openjml對程序規格進行動態和靜態的檢查
我採用了命令行的方式

java -jar ./openjml.jar -esc ~/Downloads/computer_science/schoolwork/OO/hw9/src/mycode/MyPath.java

smt solver驗證

下載openjml以及使用

openjml是用來檢查程序是否符合jml定義的規格的工具， 下載openjml.jar以後， 經過命令行運行， 主要有一下三種檢查方式。
-check 僅僅對JML語法進行靜態檢查
-esc 規格靜態檢查， 看在代碼沒有運行的時候， 有沒有不符合JML要求的操做。
-rac runtime check給定輸入文件， 在代碼運行的時候， 判斷是否有不符合JML要求的操做。

進行檢查

靜態檢查
在命令行中打入java -jar ./openjml.jar -esc -cp ~/Downloads/computer_science/schoolwork/OO/hw9/specs-homework-1-1.1-raw-jar-with-dependencies.jar ~/Downloads/computer_science/schoolwork/OO/hw9/src/mycode/MyPath.java

由於沒有修改規格， 致使出現了兩個錯誤和五個warning， 須要修改規格來讓命名方式符合， 不過我以爲這樣檢測方法不是很科學， 每一個人實現的方式不一樣， 在真實的軟件開發中， 你們都很忙， 若是這麼去調bug 的話很浪費時間， 單元測試會比這種方法更合適。

修改規格後出現了更多的報錯
由於是經過容器和hashSet實現的代碼， 和規格的描述不一樣。
目前掌握了SMT的用法， 可是因爲代碼的實現方式不一樣， 沒法合理的用SMT進行測試， 有些爲了知足JML語法而刻意去改的意味。 JML是很好的契約式設計的描述語言， 可是若是直接用SMT去進行測試的話， 還不夠成熟。

jmlUnitNg

jmlUnitNg的用法

jmlUnitng是一款經過jml語言生成testNg測試數據的工具
首先從官網下載jml-uniting， 獲得一個jar包
以後， 對於想要生成數據的java文件， 執行jml uniting
java -jar jmlunitng.jar [OPTIONS] path-list
其中options包括
-d 指定生成測試文件的目錄
-cp , --classpath 給定一系列的class path
--public 只對public方法測試
好比

java -jar jmlunitng.jar -cp hw10/src/opensource/specs-homework-2-1.2-raw-jar-with-dependencies.jar hw10/src/mycode/MyPath.java

生成上圖所示的目錄
以後， 就可使用testNg進行愉快的測試了

運行

運行結果 經過了測試

架構梳理

第一次做業

第一次做業總體難度不高， 須要修改MyPathContainer和MyPATH兩個類。
架構上MyPathContainer實現了PathContainer接口， 做爲路徑的容器。
而Path是PathContainer的組成部分。

第二次做業

第二次做業利用PATHContainer， 實現了graph， 完成第一次做業的增量式設計。

第三次做業

第三次做業在之前的基礎上增長了railwaySystem類， 繼承了Graph， 完成新的操做。

分析代碼

第一次做業

第一次做業主要是增長和刪除路徑， 我用了三個HashMap來實現

private HashMap<Path, Integer> pathToInt;
    private HashMap<Integer, Path> intToPath;
    private HashMap<Integer, Integer> nodeCount;

path到id, id到path， 以及一個node有多少個， 讓每次查詢的複雜度都接近O（1）
path hash值的計算方法以下

for (int i = 0; i < nodeList.length; i++) {
            nodes.add(nodeList[i]);
            nodeSet.add(nodeList[i]);
            hashCode = hashCode * 31 + nodeList[i];
        }

最後再Container裏經過update函數來加減PATH， 完成封裝。

private int updateByAddPath(Path path) {
        int curNextId = getNextId();
        pidList.add(curNextId);
        pathList.add(path);
        pathToInt.put(path, curNextId);
        intToPath.put(curNextId, path);
        for (int e : path) {
            if (nodeCount.containsKey(e)) {
                int oldValue = nodeCount.get(e);
                nodeCount.replace(e, oldValue + 1);
            } else {
                nodeCount.put(e, 1);
            }
        }
        return curNextId;
    }

第二次做業

第二次做業在第一次做業的基礎上增長了graph
我用hash表和數組來存儲圖

private HashMap<Integer, Integer> nodeIdToIndex;
    private HashMap<Integer, Integer> indexToNodeId;
    private int[][] graphMatrix;
    private int maxNodeCount;
    private int curNodeCount;

最後使用floyd算法來求最短路

protected void buildMinDistance() {
        for (int mid = 0; mid < curNodeCount; mid++) {
            for (int i = 0; i < curNodeCount; i++) {
                for (int j = 0; j < curNodeCount; j++) {
                    if (checkNewRoad(i, mid, j)) {
                        updateCost(i, j, getNewCost(i, mid, j));
                    }
                }
            }
        }
    }

第三次做業

此次做業， 我採用的是拆點發， 而後dijstra
把三種最短路， 化爲一個dijstra方法
type == 1, type2, type3 分別對應最低票價， 最少不滿意度， 最少換成次數

private void dijLeast(int from, int type) {
        for (int i = 0; i < distinctNodeCount; i++) {
            if (i == from) {
                dijMinDis[i] = 0;
                dijVisit[i] = true;
            } else {
                dijMinDis[i] = getGraphValue(from, i, type);
                dijVisit[i] = false;
            }
        }
        for (int i = 1; i < distinctNodeCount; i++) {
            int minCost = 10000000;
            int minPos = -1;
            int newCost;
            for (int j = 0; j < distinctNodeCount; j++) {
                if (!dijVisit[j] && dijMinDis[j] != -1) {
                    if (dijMinDis[j] < minCost) {
                        minCost = dijMinDis[j];
                        minPos = j;
                    }
                }
            }
            if (minPos == -1) {
                break;
            }
            dijVisit[minPos] = true;
            for (int j = 0; j < distinctNodeCount; j++) {
                if (!dijVisit[j] && getGraphValue(minPos, j, type) != -1) {
                    newCost = minCost + getGraphValue(minPos, j, type);
                    if (dijMinDis[j] == -1 || (dijMinDis[j] > newCost)) {
                        dijMinDis[j] = newCost;
                    }
                }
            }
        }
    }

心得體會

這三次做業， 讓我體會到了對於一個工程是如何增量設計的。 傳統瀑布式開發雖然好， 可是不夠靈活， 從這三次做業， 我體會到了敏捷開發，一邊設計， 一邊寫代碼， 一邊測試的過程， 加深的我對於開發的理解。 開發一個工程如同滾雪球， 開始只有基本的類和方法， 以後一次一次迭代， 繼承， 封裝， 最後達到要求。