JML規格單元梳理總結

前言

　　其實直到這個單元結束，對JML的理解也不是很深，對JML最直觀的見解就是對着JML規格寫代碼很舒服，還有JML真的不怎麼好寫。

　　固然，針對這三次做業來談，其實並非很理解JML在此次做業中佔據的主導地位，更像是給了我一份用JML語言寫的代碼功能說明書，而後由我本身來決定使用怎樣的數據結構和算法來提高代碼的性能。

　　因此，到了後來第三次做業，雖然初衷是考察對JML的理解和掌握，但實際上重心已經跑偏到對算法的挖掘和改造了，固然，我這個不知道怎麼想的沒有管算法的笨蛋隨便實現了規格的功能就沒有再管，結果直接致使強測爆0，又一次重現了上單元做業的悲劇（捂臉）——到了最後就瘋狂掉鏈子。實際上，當網站開始強測的時候，我就開始重構代碼了（再次捂臉）。只能說，人是真的菜。

　　好了，接下來按照博客做業的要求對本單元作一次總結。

JML語言的理論基礎及應用工具鏈

JML理論基礎

　　JML（Java Modeling Language，Java建模語言），在Java代碼種增長了一些符號，這些符號用來標誌一個方法是幹什麼的，可是不關心它的具體實現。經過使用JML，在實現代碼前，咱們能夠描述一個方法的預期功能，而儘量地忽略實現，從而把過程性思考一直延遲到方法設計的層面。

　　若是僅僅是描述方法的功能，那麼天然語言同樣能夠作到，可是，使用JML語言的好處是，相比於容易產生歧義的天然語言，之前置條件、反作用、異常行爲、做用域、後置條件等爲標準規格的JML規格語言能減小歧義的產生。

關於JML規格的舉例

    /*@ public normal_behavior（注：通常行爲）
      @ requires class != null;（注：前置條件）
      @ assignable \nothing;（注反作用）
      @ ensures \result = (class == nowclass)(注：後置條件、\result-返回值）
      @ also
      @ public exceptional_behavior（注：異常行爲）
      @ signals (ClassNotValid e) class == null;(注：拋出異常）
   */

 

　　固然，是語言就會有問題，可是，嚴格的JML語言避免了自己的歧義，一旦出現問題，就很容易能找到是JML規格的描述問題仍是代碼的實現問題。對客服而言，能提前發現客戶代碼對類地錯誤使用，還能給客戶提供和代碼徹底一致地JML規格文檔；而對於程序員，可以準確地知道代碼須要實現的功能，高效地尋找和修正程序的bug（對比代碼和規格便知），還能在代碼升級時下降引入bug地可能。

　　注：以上內容部分參考 ：壽智振 ，《應用建模語言 JML 改進 Java 程序》，https://wenku.baidu.com/view/af526b94fc4ffe473368abc0.html。

JML工具鏈

• JML具備標準的格式，所以能夠對其進行語法和格式上的檢查，通常能夠採用Openjml等工具進行JML規格的靜態檢查。
• 而使用JMLUnitNG/IMLunit之類的工具，能夠在設計測試方法，檢查JML規格和相應的代碼實現狀況。

JMLUnitNG實現簡單的測試

測試代碼：

// demo/Demo.java
package demo;

public class Demo {
    /*@ public normal_behaviour
      @ ensures \result == (lhs != rhs);
    */
    public static boolean notequal(int lhs, int rhs) {
        return rhs != lhs;
    }

    public static void main(String[] args) {
        notequal(-1,0);
    }
}

輸出結果：

[TestNG] Running:
Command line suite

Passed: racEnabled()
Passed: constructor Demo()
Passed: static main(null)
Passed: static main({})
Passed: static notequal(-2147483648, -2147483648)
Passed: static notequal(0, -2147483648)
Passed: static notequal(2147483647, -2147483648)
Passed: static notequal(-2147483648, 0)
Passed: static notequal(0, 0)
Passed: static notequal(2147483647, 0)
Passed: static notequal(-2147483648, 2147483647)
Passed: static notequal(0, 2147483647)
Passed: static notequal(2147483647, 2147483647)

===============================================
Command line suite
Total tests run: 13, Failures: 0, Skips: 0
===============================================

分析和假想：

　　首先感謝大佬在討論區的分享，我折騰了三個小時總算搞出來一個勉強看過去的測試樣例，雖然這個樣例是仿照大佬分享的簡單例子。

　　雖然這個徹底實現了簡單的規格，也就是邊界測試沒有Failures，可是我最初寫的測試例子還包括異常拋出，可是因爲沒有時間了，只能草草完成了這麼一個簡單的例子，更深刻的分析也沒有作（沮喪）。　　

梳理幾回做業架構的設計

第一次做業：

類圖：

分析：

　　第一次做業其實沒有什麼好分析，從圖中能夠看出，我在MyPath類中採用了HashMap類，爲了方便統計一個路徑中不一樣節點的個數，其次實現了Compareto和Iterator接口，實現了比較和迭代器，迭代器容許遍歷訪問MyPath類中指定的數據元素而沒有暴露出數據實現自己。而在MyPathContainer中徹底採用了HashMap存儲路徑信息，可是由於沒有重寫hashcode的產生方法，在比較路徑相等時調用了Path的迭代器進行了挨個節點比較，這裏的效率比較低。

第二次做業：

類圖：

 分析：

　　第二次做業至關於在第一次做業規格的基礎上增長了四個查詢方法，基本上是在第一次代碼上作了一些修改完成的。在數據結構上，僅從規格說明的角度看，增長了圖的結構。所以，做爲一個鄰接鏈表的忠實愛好者，我義無反顧地實現了一個Point類，用來存儲點的數據結構，而diffpoint的Hash value也變成了Point類，以此完成了一個鄰接鏈表。Point內部屬性很是簡單，ref表示該點被引用次數，link表示該點與其餘點鏈接的狀況，而在Graph類中除了在添加Path的時候須要修改本來在地磁做業實現的add類方法外，還須要實現一個deleteformgraph的規格外方法來從圖中刪除路徑，同時還有一個getshortest方法內置了bfs（廣度搜索遍歷）來支持規格中的getShortestPathLength方法。

BFS代碼以下：

    private int getshortest(int fromnode,int tonode) {
        if (fromnode == tonode) {
            return 0;
        }
        HashMap<Integer,Integer> sign = new HashMap<>();
        ArrayList<Integer> nodelist = new ArrayList<>();
        int length = 0;
        Iterator iterator = diffpoint.get(fromnode).
                getLink().entrySet().iterator();
        int limit = 0;
        while (iterator.hasNext()) {
            HashMap.Entry entry = (HashMap.Entry) iterator.next();
            int key = Integer.class.cast(entry.getKey());
            nodelist.add(key);
            sign.put(key,key);
        }
        length = 1;
        limit = nodelist.size() - 1;
        if (sign.containsKey(tonode)) {
            return length;
        }
        int pointer = 0;
        for (;pointer < nodelist.size();pointer += 1) {
            iterator = diffpoint.get(nodelist.get(pointer))
                    .getLink().entrySet().iterator();
            while (iterator.hasNext()) {
                HashMap.Entry entry = (HashMap.Entry) iterator.next();
                int key = Integer.class.cast(entry.getKey());
                if (!sign.containsKey(key)) {
                    nodelist.add(key);
                    sign.put(key,key);
                }
            }
            if (sign.containsKey(tonode)) {
                return length + 1;
            }
            if (pointer == limit) {
                limit = nodelist.size() - 1;
                length += 1;
            }
        }
        return -1;
    }

第三次做業：

類圖：

 

分析：

　　第三次做業不管是從算法仍是從架構的設計上均可以說是不折不扣的失敗。

　　由於，地鐵類是在第二次做業的基礎上拓展的規格，所以，在架構的實現上我沿用了以前的實現方式，即繼續採用鄰接表。這裏就不得不提到從第二次做業就開始的算法偏重討論。從第二做業開始，由於查詢圖是件麻煩事，因此大部分同窗都比較支持進行全面的圖的計算，而後查詢時爲O(1）的算法偏重，可是因爲第二次做業使用了鄰接表，那麼florid算法的實現就比較難受，所以我在第三次魔改了深度遍歷搜索，或者說徹底放棄了算法的性能，採用了所有遍歷兩點之間全部的路徑，而後計算不滿意度、最小換乘等問題，這直接致使我強測爆炸。

　　而對架構的傷害，由於思路採用了和第二次同樣的暴力求解，就迫使我對Point類進行大量的增添，其中最重要的一塊就是邊和路徑id的統一，這也迫使我增長了pathid和record兩個類。

　　雖然本來的架構基本沒有重構，但在本來哪一個已經落伍於全新版本的架構上繼續增長的冗餘部分進一步致使了架構的劣化，也就是說，若是在此次做業基礎上繼續增長新的功能的話，個人架構會更加難看。其次，爲了便於使用Point類內的屬性，我直接返回了Point類的私有對象，又是一大敗筆。

重構做業：

類圖：

 

分析：

　　我基本上在重構的時候徹底重寫了第二次和第三次做業（捂臉），重構的思路其實創建在florid算法的基礎上。所以採用了大量的二位靜態數組做爲存儲相關數據的鄰接矩陣。架構上其實沒有什麼值得一談的東西，相比起以前的鄰接表的作法，這種作法更加暴力，增長功能的話增長相應的二維數組對就好了，一個用來存儲當前圖對應的數據，另外一個用來存儲通過florid算法後獲得的內容，因此表示同一功能的二維數組基本上是成對出現的。而在這個基礎把不滿意度、換乘、最小票價問題都利用相應的算法轉化爲通常的florid模式，大大減小了代碼量。除此之外，florid也設計成了一個具體的功能方法，有助於代碼的簡化。

florid方法代碼：

    private boolean floridforlength(int[][] src,int[][] dst
            ,boolean reset,int rin) {
        if (!reset) {
            return false;
        }
        for (int i = 0; i < num; i += 1) {
            for (int j = 0; j < num; j += 1) {
                dst[i][j] = src[i][j];
            }
        }
        for (int k = 0; k < num; k += 1) {
            for (int i = 0; i < num; i += 1) {
                for (int j = 0; j < num; j += 1) {
                    int temp;
                    if (i == j || dst[i][k] == max || dst[k][j] == max) {
                        temp = max;
                    } else {
                        temp = dst[i][k] + dst[k][j] + rin;
                    }
                    if (dst[i][j] > temp) {
                        dst[i][j] = temp;
                    }
                }
            }
        }
        return false;
    }

代碼實現bug及修復狀況

 算法bug:

　　這個嚴格意義上說並不算bug，只是此次形成的後果比較嚴重因此拿出來談一下。

　　根據我此次教訓，我以爲這種bug，徹底能夠在設計前能找到，可是本身不必定能找到，由於當局者迷。而這種Bug出自我對問題的難度和問題的側重點認識不足的狀況。以此次爲例，我在最初設計算法的時候，只考慮了怎麼解決換乘的問題，而沒有解決算法的性能問題，這使得算法最終成形的時候幾乎沒有性能這一律念。所以，我開始寫算法題了（捂臉），讓本身適應去思考怎麼作才能更優化。

其它bug:

　　除了上面的算法問題外，其它幾乎沒有什麼毛病，包括我智障地調用了錯誤的方法啥的都不值得討論。但有一點值得討論一下，那就是Java的對象引用。

　　我對對象的引用就當作了C的指針，實際上用起來差異不是很大，可是在實際使用的時候會犯一些不是很容易發現的小錯誤。

    private void countinit() {
        havetry.clear();
        list.clear();
        record = new Record();
        price = 0;
        trafer = 0;
        unpleasure = 0;
    }

　　上面是我寫的一個初始化方法，該方法每次都會在某些方法使用前調用，能夠看到我這裏寫了一句

record = new Record();

　　而我以前是這麼寫的

record = record.init();

　　而其調用的init方法以下

    public void init() {
        lesttrafer = -1;
        leastprice = -1;
        leatunplt = -1;
        leastlength = -1;
    }

　　以上使用看起來沒問題，實際上問題很大。由於我是對一個record對象調用init()方法，而這個record對象會被我put進某些HashMap對象中，那麼當我再次調用countinit()方法後，已經被put進去的數據會被初始化，而後同化爲下一次計算的結果。

　　我以爲這應該是對引用的濫用致使的，以及我應該給每一個類寫一個clone方法提醒本身淺拷貝和深拷貝的區別。

規格撰寫和理解上的心得體會

 　　首先，我認爲這三次課下做業對規格的撰寫沒有涉及，其次，兩次課上對規格撰寫和修改的練習，也僅僅停留在對JML規格語法的實踐和練習上。

　　我認爲，JML規格，或者說通常意義上的規格，是爲了軟件開發和團隊合做而生的。

　　其在團隊合做的做用應該是減小不一樣人代碼開發的耦合度，同時劃分明確的分工。

　　在軟件開發的層面上，更多地側重於把軟件功能層次化，細分化。

　　規格，側重於功能而非實現，也就是先給出了一個具體地框架，我認爲能夠理解爲給出了一個黑箱，規格一開始要說明這個黑箱能幹什麼；而後，規格會進一步拆解這個黑箱，去說明更多的小黑箱能幹什麼；最終規格會縮小到方法地層面上，說明一個方法黑箱應具備怎麼樣地輸入和輸出。

　　對於規格地實現，個人理解是，只須要理解規格給出的功能性說明，而不須要在乎規格給出的可能的代碼邏輯。舉個最簡單的例子，第一次做業中Path的數據規格給了一個int[]的類型，實際上這只是說明存在這樣的數據結構，而非必定要實現這樣的數組，實際上，真正這麼搞的同窗估計沒有幾個。

　　我以爲規格使用至關有必要，並且在完成規格後再實現代碼會具備更高的效率。目前爲止，我所接觸的代碼都是很小的，幾乎不成功能，可是我以爲若是我想完成一個軟件，那麼我不只會寫設計文檔，還會在完成設計文檔後，寫詳細的規格說明書，最後再開始實現代碼。