碼上快樂

相關內容    簡體    繁體

OO第三單元博客作業

本文轉載自   查看原文   2019-05-20 11:00   459 

——“基於正確規格的程序就可以被認為是正確的程序 ”

本單元的三次作為均為根據jml規格完成代碼。三次作業依次為實現Path路徑類和PathContainer路徑容器類；將PathContainer類擴展成Graph類以實現圖相關問題的處理；將Graph類擴展成RailwaySystem類以支持多種最短路查詢(完成數據結構圖論專題練習)。

本文將從JML語言梳理、部署SMT Solver進行驗證、部署JML UnitNG並針對Graph接口的實現進行測試、梳理架構設計以及分析代碼實現的bug和修復情況方面對第三單元的三次作業進行總結，並在最后闡述對規格撰寫和理解上的心得體會。

  • JML語言梳理

    • 理論基礎

      面向對象編程思想中有一個重要原則就是盡量推遲過程性的思考。所以我們在設計面向對象程序時首先要考慮的要干什么而不是怎么干什么。而Java本身並沒有提供一種描述程序要干什么的方法，於是我們引入Java建模語言JML(Java Modeling Language)來實現這一目的。

      JML是一種行為接口的規范語言，可以用來指定Java模塊的行為，其最基本的用途是作為Java的合同設計(DBC)語言。

      JML在實際設計中主要有兩種用途：

      • 在實現前對設計的規格進行精確傳達

        JML語言通過對規格進行精確表述，使架構人員和代碼實現人員達成一致，可以認為是程序猿之間進行交流的猿語。

      • 對已實現的代碼進行總結梳理

        這方面的作用主要體現在提高代碼的可維護性。

        實際上，如果我是維護人員，可能我只會在第一次通讀規格，然后用自然語言進行注釋（畢竟還是要說人話的）。這種感覺有點像把精妙但晦澀文言文翻譯成粗糙易懂白話文，白話文有什么地方解釋得模糊了，再去查原文。

    • 應用工具鏈

      首先通過開源的JML編譯器，比如OpenJml，編譯含有JML標記的代碼。

      對於Openjml來說 -check 選項可以對生成的類文件進行JML規范檢查。

      Openjml中還包含z3等SMT Solver，可以對代碼等價性進行驗證。通過Openjml -esc 選項對代碼的靜態驗證是不依賴JML的，SMT Solver會自動整理JML(當然存在整理不出來的情況，這時就只能手動添加一波，強烈建議統一源碼和jar包)。

      JML UnitNG可以生成一個Java類文件測試的框架，基於JML並結合Openjml的-rac運行時檢查選項，實現對代碼的自動化測試。據觀察，這種測試主要是邊界測試。

      JMLdoc工具與Javadoc工具類似，可在生成的HTML格式文檔中包含JML規范。

  • 部署SMT Solver進行驗證

    SMT(Staisfiability modulo theories) Solver即定理證明器。

    通過OpenJML下載OpenJML，然后根據討論區霸霸的OpenJML基本使用部署OpenJML的同時就能擁有SMT Solver啦~

    其工作機理是：

    OpenJML將JML規范轉換為SMT-LIB格式，並將Java+JML程序所隱含的證明問題傳遞給后端SMT求解器。

    OpenJML支持主要的SMT解決方案，如Z3、CVC4和YIES。

    證明的成功將取決於SMT解算器的能力（例如，它支持哪些邏輯）、代碼+規范的特定邏輯編碼以及代碼和規范編寫的復雜性和樣式。

    使用命令

    java -jar <path>/openjml.jar -esc <soursefile>	# 未按上述鏈接部署
openjml -esc <sourcefile> 						# 按上述鏈接添加了openjml腳本

    即可對代碼進行靜態檢查。

    下文是使用SMT Solver對第一次作業中各方法進行驗證的結果。

    • public MyPath(int... nodeList)

      // 1.下標可能為負
homework/MyPath.java:16: warning: The prover cannot establish an assertion (PossiblyNegativeIndex) in method MyPath
            this.nodeList.add(nodeList[i]);
                                      ^
/*
	// 修改前代碼
    public MyPath(int... nodeList) {
        this.nodeList = new ArrayList<>();
        for (int i = 0; i < nodeList.length; i++) {
            this.nodeList.add(nodeList[i]);
        }
    }
*/
	// 修改后代碼
    public MyPath(int... nodeList) {
        this.nodeList = new ArrayList<>();
        for (int i = 0; i < nodeList.length; i++) {
        	if (i >= 0) {
            	this.nodeList.add(nodeList[i]);
            }
        }
    }

    • public int compareTo(Path o)

      /usr/share/java/openjml-0.8.42/openjml.jar(specs/java/util/Collection.jml):71: warning: The prover cannot establish an assertion (Invariant) in method compareTo
    //-RAC@ public invariant content.theSize >= 0;
                   ^
/usr/share/java/openjml-0.8.42/openjml.jar(specs/java/util/Collection.jml):70: warning: The prover cannot establish an assertion (Invariant) in method compareTo
    //-RAC@ public invariant content.owner == this;
                   ^

    • public boolean equals(Obj o)

      homework/MyPath.java:45: warning: The prover cannot establish an assertion (ExceptionalPostcondition: /usr/share/java/openjml-0.8.42/openjml.jar(specs/java/lang/Object.jml):76: ) in method equals
        if (!(this.size() == ((Path) varl).size())) {
                       ^
/usr/share/java/openjml-0.8.42/openjml.jar(specs/java/lang/Object.jml):76: warning: Associated declaration: homework/MyPath.java:45: 
      @   public normal_behavior
                 ^
/usr/share/java/openjml-0.8.42/openjml.jar(specs/java/util/Collection.jml):70: warning: The prover cannot establish an assertion (Invariant) in method equals
    //-RAC@ public invariant content.owner == this;
                   ^
homework/MyPath.java:50: warning: The prover cannot establish an assertion (Postcondition: /usr/share/java/openjml-0.8.42/openjml.jar(specs/java/lang/Object.jml):78: ) in method equals
                return false;
                ^
/usr/share/java/openjml-0.8.42/openjml.jar(specs/java/lang/Object.jml):78: warning: Associated declaration: homework/MyPath.java:50: 
      @     ensures \result;
            ^
/usr/share/java/openjml-0.8.42/openjml.jar(specs/java/util/Collection.jml):71: warning: The prover cannot establish an assertion (Invariant) in method equals
    //-RAC@ public invariant content.theSize >= 0;
                  ^
    
/*
	// 修改前代碼
    public boolean equals(Object varl) {
        if (varl == null || !(varl instanceof Path)) {
            return false;
        }
        if (!(this.size() == ((Path) varl).size())) {
            return false;
        }
        for (int i = 0; i < this.size(); i++) {
            if (!(this.getNode(i) == ((Path) varl).getNode(i))) {
                return false;
            }
        }
        return true;
    }
*/

// 修改后代碼
    public boolean equals(Object varl) {
        if (varl == null || !(varl instanceof Path)) {
            return false;
        }
        int thisSize;
        int varlSize;
        
        try { thisSize = this.size(); } 
        catch (Exception e) { return false; }
        
        try { varlSize = ((Path) varl).size(); } 
        catch (Exception e) { return false; }
        
        if (thisSize != varlSize) {
            return false;
        }
        
        int i;
        for (i = 0; i < thisSize; i++) {
            try {
                if (!(this.getNode(i) == ((Path) varl).getNode(i))) {
                    break;
                }
            } catch (Exception e) { return false; }
        }
        if (i < thisSize) {
            return true;
        } else {
        	return false;
		}
    }

    • public int hashCode()

      homework/MyPath.java:87: warning: The prover cannot establish an assertion (Postcondition: /usr/share/java/openjml-0.8.42/openjml.jar(specs/java/lang/Object.jml):63: ) in method hashCode
        return nodeList.hashCode();
        ^
/usr/share/java/openjml-0.8.42/openjml.jar(specs/java/lang/Object.jml):63: warning: Associated declaration: homework/MyPath.java:87: 
    //-RAC@ ensures \result == theHashCode;  
            ^

    可見，靜態驗證可能更適合於更大型的項目。在我們的作業中應用使我們的代碼中需要額外考慮一些可能並不會出現的exception，導致代碼不夠簡明。

  • 部署JMLUnitNG並針對Graph接口的實現進行測試

    JMLUnitNG是JMLUnit的一個基於TestNG的繼承者，而TestNG(Test Next Gerneration)是一個開源自動化測試框架。

    JMLUnitNG的部署方法還是仰仗同一個霸霸使用 JMLUnitNG 生成 TestNG 測試樣例。

    以下是測試結果：

    [TestNG] Running:
  Command line suite

Passed: racEnabled()
Passed: constructor MyGraph()
Passed: <<homework.MyGraph@18ef96>>.addPath(null)
Passed: <<homework.MyGraph@ba4d54>>.containsEdge(-2147483648, -2147483648)
Passed: <<homework.MyGraph@de0a01f>>.containsEdge(0, -2147483648)
Passed: <<homework.MyGraph@4c75cab9>>.containsEdge(2147483647, -2147483648)
Passed: <<homework.MyGraph@1ef7fe8e>>.containsEdge(-2147483648, 0)
Passed: <<homework.MyGraph@6f79caec>>.containsEdge(0, 0)
Passed: <<homework.MyGraph@67117f44>>.containsEdge(2147483647, 0)
Passed: <<homework.MyGraph@5d3411d>>.containsEdge(-2147483648, 2147483647)
Passed: <<homework.MyGraph@2471cca7>>.containsEdge(0, 2147483647)
Passed: <<homework.MyGraph@5fe5c6f>>.containsEdge(2147483647, 2147483647)
Passed: <<homework.MyGraph@6979e8cb>>.containsNode(-2147483648)
Passed: <<homework.MyGraph@763d9750>>.containsNode(0)
Passed: <<homework.MyGraph@2be94b0f>>.containsNode(2147483647)
Passed: <<homework.MyGraph@d70c109>>.containsPathId(-2147483648)
Passed: <<homework.MyGraph@17ed40e0>>.containsPathId(0)
Passed: <<homework.MyGraph@50675690>>.containsPathId(2147483647)
Skipped: <<homework.MyGraph@31b7dea0>>.containsPath(null)
Passed: <<homework.MyGraph@3ac42916>>.getDist()
Passed: <<homework.MyGraph@47d384ee>>.getDistinctNodeCount()
Passed: <<homework.MyGraph@2d6a9952>>.getGraph()
Failed: <<homework.MyGraph@22a71081>>.getPathById(-2147483648)
Failed: <<homework.MyGraph@3930015a>>.getPathById(0)
Failed: <<homework.MyGraph@629f0666>>.getPathById(2147483647)
Failed: <<homework.MyGraph@1bc6a36e>>.getPathId(null)
Failed: <<homework.MyGraph@1ff8b8f>>.getShortestPathLength(-2147483648, -2147483648)
Failed: <<homework.MyGraph@387c703b>>.getShortestPathLength(0, -2147483648)
Failed: <<homework.MyGraph@224aed64>>.getShortestPathLength(2147483647, -2147483648)
Failed: <<homework.MyGraph@c39f790>>.getShortestPathLength(-2147483648, 0)
Failed: <<homework.MyGraph@71e7a66b>>.getShortestPathLength(0, 0)
Failed: <<homework.MyGraph@2ac1fdc4>>.getShortestPathLength(2147483647, 0)
Failed: <<homework.MyGraph@5f150435>>.getShortestPathLength(-2147483648, 2147483647)
Failed: <<homework.MyGraph@1c53fd30>>.getShortestPathLength(0, 2147483647)
Failed: <<homework.MyGraph@50cbc42f>>.getShortestPathLength(2147483647, 2147483647)
Passed: <<homework.MyGraph@75412c2f>>.getUpdateDist()
Failed: <<homework.MyGraph@282ba1e>>.isConnected(-2147483648, -2147483648)
Failed: <<homework.MyGraph@13b6d03>>.isConnected(0, -2147483648)
Failed: <<homework.MyGraph@f5f2bb7>>.isConnected(2147483647, -2147483648)
Failed: <<homework.MyGraph@73035e27>>.isConnected(-2147483648, 0)
Failed: <<homework.MyGraph@64c64813>>.isConnected(0, 0)
Failed: <<homework.MyGraph@3ecf72fd>>.isConnected(2147483647, 0)
Failed: <<homework.MyGraph@483bf400>>.isConnected(-2147483648, 2147483647)
Failed: <<homework.MyGraph@21a06946>>.isConnected(0, 2147483647)
Failed: <<homework.MyGraph@77f03bb1>>.isConnected(2147483647, 2147483647)
Failed: <<homework.MyGraph@326de728>>.removePathById(-2147483648)
Failed: <<homework.MyGraph@25618e91>>.removePathById(0)
Failed: <<homework.MyGraph@7a92922>>.removePathById(2147483647)
Failed: <<homework.MyGraph@71f2a7d5>>.removePath(null)
Passed: <<homework.MyGraph@2cfb4a64>>.size()

===============================================
Command line suite
Total tests run: 50, Failures: 26, Skips: 1
===============================================

    這些測試數據中，如果方法聲明中變量是int類型的話，會對int范圍內的極大極小值和0進行測試；如果是Integer類型還會額外增加對空指針null的測試。

    對於通過JMLUnitNG生成測試樣例我還有許多不解，希望有dalao能夠救救孩子。

    • 首先，可以看到結果中有許多failed，看起來非常不詳。

      我的第一個疑惑是failed的含義是什么？是指我的程序運行結果與預期不符，還是指我的程序沒有正常執行完，比如拋出了異常？

    • 其次，通過這種方式生成的測試是否與jml相關？

      我試圖通過實驗驗證，於是對較為簡單的Path類進行了以上測試，結果如下：

      [TestNG] Running:
  Command line suite

Passed: racEnabled()
Failed: constructor MyPath(null)
Passed: constructor MyPath({})
Failed: <<homework.MyPath@1>>.compareTo(null)
Passed: <<homework.MyPath@1>>.containsNode(-2147483648)
Passed: <<homework.MyPath@1>>.containsNode(0)
Passed: <<homework.MyPath@1>>.containsNode(2147483647)
Passed: <<homework.MyPath@1>>.equals(null)
Passed: <<homework.MyPath@1>>.equals(java.lang.Object@1c2c22f3)
Passed: <<homework.MyPath@1>>.getDistinctNodeCount()
Failed: <<homework.MyPath@1>>.getNode(-2147483648)
Failed: <<homework.MyPath@1>>.getNode(0)
Failed: <<homework.MyPath@1>>.getNode(2147483647)
Passed: <<homework.MyPath@1>>.hashCode()
Passed: <<homework.MyPath@1>>.isValid()
Passed: <<homework.MyPath@1>>.iterator()
Passed: <<homework.MyPath@1>>.size()

===============================================
Command line suite

# Total tests run: 17, Failures: 5, Skips: 0
===============================================

      可以看到以上failed樣例對應的方法都是有前置條件@requires的方法，如果該測試是依賴jml的，即生成的測試樣例一定是符合jml的，且產生的結果是否正確也是以jml為依據的，那就應該在我添加了相關@requires限制之后就不存在failed樣例了，然而我進行了以上操作之后結果並沒有改變。

      如果這意味着這種測試方法是jml無關的話，那是否passed顯得也並不那么重要了，畢竟在不滿足規格中的@requires條件的情況下結果是不可預測的，這就使TestNG的價值降低了不少，因為這樣對於每一個failed樣例都需要人工判斷是否真的錯誤？

      最后牆裂建議統一源碼和jar包！！！

  • 梳理架構設計

    第一次作業就是粗暴的接口長啥樣我長啥樣。

    第一次作業類圖

    第二次作業也基本上和接口長一樣，不過可能第二次作業意識到規格只是對結果的限制，對實現並沒有限制，於是寫得隨意了許多。另外，第二次作業中的Graph類實際上可以繼承PathContainer類，但我腦子一熱就順手CtrlCV了，到第三次作業就發現，幸好當時腦子熱了。

    第二次作業類圖

    第三次作業的架構是陽春白雪和下里巴人的結合。之前的部分不想重構了，擴展的部分又繼承了之前的部分，就非常，，，混搭。

    第三次作業花式最短路，我選擇了拆點算法，而且是菊花點。然后架構大概長這樣：

    其中NodeWithPathId繼承了Pair類，是儲存在圖中的節點結構，包含了NodeId和它所屬的PathId；GraphStructure是抽象的圖類，包含已實現的加路徑、刪路徑和計算實際最短路結果的方法，以及未實現的加邊、刪邊和求最短路方法；

    TicketPriceGraph(TPG)類和抽象類MultiPointsWeightGraph(MPWG)類均繼承了GraphStruceture類，其中TPG中最短路的實現方法為BFS，MPWG是帶權圖抽象類，最短路的實現方法為堆優化Dijstra，其中還聲明了未實現的求權重方法；

    最后TransferGraph和Unpleasant類均繼承MPWG類，各自實現不同的求權重方法。

    實際上如果將第二次作業的架構也整合進去的話，可以直接將TicketPriceGraph類作為無權圖類，然后TicketPriceGraph和ShortestPathLength各自作為該類實例化出的對象即可。

    同時，如果使用泛型還可以將有權圖和無權圖的方法進一步復用，然而知識水平暫時不資瓷，就先這樣了。

    第三次作業類圖

  • 分析代碼實現的bug和修復情況

    這一部分的題目看起開非常有趣，”分析代碼實現的bug“，我的代碼確實實現了一堆bug QAQ

    • 第一次作業

      第一次作業因為還不了解jml只是對結果的約束，以為只能有兩個線性存儲結構，導致DISTINCT_NODE_COUNT方法時間復雜度過高，出現了TLE的問題。

      通過增加一個HashMap存儲當前某個節點出現了多少次，查詢時輸出size()解決了該問題。

    • 第三次作業

      墨菲定律車禍現場，以為自己穩了，結局確實穩C了。

      • 首先，come some music，如果我不會寫dij你會愛我嗎~

        原來的寫法存在部分節點realDist更新后沒有重新進入優先隊列的問題（強測這分已經是撞大運了

            @Override
    public void
        shortestPath(Integer st, HashMap<Integer, Integer> dist,
                 HashSet<Integer> pathIdContainsSt) {
        HashMap<NodeWithPathId, Integer> realDist = new HashMap<>();

        PriorityQueue<NodeWithPathId> queue
                = new PriorityQueue<>(new Comparator<NodeWithPathId>() {
                    @Override
                    public int compare(NodeWithPathId o1, NodeWithPathId o2) {
                        return realDist.get(o1).compareTo(
                                realDist.get(o2));
                    }
                });

        NodeWithPathId uu = new NodeWithPathId(st, terminalPathId);
        realDist.put(uu, new Integer(0));
        queue.offer(uu);
      
        while (!queue.isEmpty()) {
            uu = queue.poll();
            for (Pair<NodeWithPathId, Integer> vvWithValue
                    : this.get(uu).keySet()) {
                NodeWithPathId vv = vvWithValue.getKey();
                Integer ww = vvWithValue.getValue();
                Integer newDist = new Integer(realDist.get(uu) + ww);
                /*
                它原來長這樣
                if (!realDist.containsKey(vv)) {
                	realDist.put(vv, newDist);
                	queue.offer(vv);
                } else if(newDist < realDist.get(vv)) { // 更新后沒有入隊
                    realDist.put(vv, newDist);
                }
                */
                if (!realDist.containsKey(vv) || (realDist.containsKey(vv)
                        && newDist.compareTo(realDist.get(vv)) < 0)) {
                    realDist.put(vv, newDist);
                    if (!queue.contains(vv)) {
                        queue.offer(vv);
                    }
                }
            }
        }
        calculateDist(dist, realDist);
    }

      • 其次，由於第三次作業繼承了第二次作業，但是對於圖修改指令又有所擴充，腦子一抽就沒檢查擴充后的方法是否符合規格，導致addPath方法中，如果該邊存在，還是會重新加一遍相同的邊。

            @Override
    public int addPath(Path varl) throws Exception {
        int lastId = getId();
        int addPathId =  super.addPath(varl);
        // 原來它長這樣
        // if (addPathId != 0) { 
        if (addPathId > lastId) { 
            ticketPriceGraph.addPath(addPathId, varl, termials);
            transferGraph.addPath(addPathId, varl, termials);
            unpleasentGraph.addPath(addPathId, varl, termials);
            addForTerminals(addPathId, varl);
        }
        return addPathId;
    }

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

    對於規格撰寫，有以下幾點體會：

    • 清楚規格只限定結果不規定實現的特性；
    • 要熟悉語法，同時規格定義中只能調用pure方法；
    • 可以先從數學的角度進行分析，對充分必要條件拆分成充分條件和必要條件進行分別表述。

    對於規格的理解大概就是像讀os代碼一樣，尋尋覓覓(凄凄慘慘戚戚)追根溯源地通讀一遍，有個大概輪廓，然后在寫代碼的過程中哪里模糊了再去查詢細究之類。


免責聲明！

本站轉載的文章為個人學習借鑒使用，本站對版權不負任何法律責任。如果侵犯了您的隱私權益，請聯系本站郵箱yoyou2525@163.com刪除。



猜您在找 OO第三次博客作業 OO第二單元總結博客 2020 OO 第三單元總結 JML語言 BUAA_OO_2020_第三單元總結 oo 第一次博客作業 第三單元博客總結 OO第一單元總結 OO第5~7次作業總結 2020 OO 第二單元總結 第四單元及OO課程總結
 
粵ICP備18138465號   © 2018-2025 CODEPRJ.COM