JML規格編程——BUAA OO第三單元做業總結

時間  2019-12-18
標籤 jml 規格 編程 buaa 第三 單元 總結 简体版
原文   原文鏈接

總體概述

這個單元總體圍繞Java Model Language(JML)展開，經過學習JML規格瞭解契約式編程的過程，課上實驗中進行了JML規格的簡要編寫，課下實驗主要經過閱讀規格並按照規格的要求正確編寫程序實現相應的接口。java

JML入門

JML做爲一種建模語言，主要的功能就是經過邏輯推演的方式對程序的表現進行限制，使用JML建模的程序實現起來只要知足JML的表達式就能夠認爲程序知足的需求。所以，從設計層面看，這既是對天然語言的一種轉換也是從天然語言需求到計算機代碼之間的橋樑，可以幫助使用者更好地對需求進行定義。同時，經過使用SMT solver以及junitNG等工具還能夠很好地驗證程序的正確性，甚至自動生成測試樣例進行機動化測試。node

  1. JML語言基礎linux

    本單元中咱們使用到的JML語言成分主要有：git

    關鍵字 說明
    normal_behavior 正常表現
    requires 前置條件
    ensures 後置條件
    invariant 類不變式
    assignable 約束後置條件中哪些變量可變
    exceptional_behavior 異常表現
    signals 異常描述

    使用以上語言成分就能夠對Java程序中常見的程序表現進行建模，規定某個類、函數的使用條件和不一樣輸入狀況下的表現。此外，在JML中能夠用來表達的邏輯關係有：程序員

    關鍵字 說明
    && 邏輯與
    || 邏輯或
    ! 邏輯非
    == 相等關係
    ==> 邏輯蘊含
    <==> 邏輯等價
    \forall 全稱量詞
    \exists 存在量詞

    使用以上的邏輯關鍵詞就能夠準確且無二義性的表示程序須要完成的需求表現，嚴格規定程序的責任關係。同時，JML還提供了\old表示同一變量修改以前的值，\result表示函數的返回值等進行建模。github

  2. 規格描述

    • 類的數據規格算法

      類的數據規格主要經過不變式invatiant和constraint進行約束，表示一個類在建立時應有怎樣的數據表現，以及進行相應的修改操做時應該知足怎樣的條件。針對層次關係則須要知足：
      • 子類繼承父類的規則，子類能夠重寫父類的方法規格
      • 子類不能違反父類的規則，具體表現爲：前置條件只能減弱，後置條件只能增強。

    • 方法的規格描述編程

      JML的建模主要集中在對類方法的行爲約束上，而JML的約束又主要體如今數據約束上，即：經過指明數據須要知足的邏輯條件來規範程序的表現。建模時須要考慮的過程有：
      • 參數與輸入狀態：即調用函數以前須要知足requires前置條件的約束
      • 輸出與返回的表現：即返回以前應該使得數據知足ensures後置條件以及類不變式的要求
      • 異常行爲：異常行爲經過exceptional_behavior指定
      • 是否修改類的相關數據：方法是pure的查詢方法，仍是包含assignable能夠修改類中的相關數據的？

    經過以上的過程就能實現使用JML的嚴格建模。windows

JML相關工具的使用

SML Solver

SML Solver是一個通用的自動化求解技術，能夠用來證實程序的等價，從而直接從邏輯上驗證程序的正肯定，避免了繁瑣的測試過程。實踐中，我使用了Z3 Theorem Prover與OpenJML結合的方式進行驗證。bash

命令行使用

在下載完兩項工具以後，爲了使OpenJML調用到正確的Z3，須要修改openjml.properties文件：

openjml.defaultProver=z3_4_3
openjml.prover.z3_4_3=D:\\Document\\ProgramHome\\z3-4.3.2-x64-win\\bin\\z3.exe

爲了不每次啓動都要切換目錄並寫jar路徑，能夠創建腳本運行（linux平臺方式不少，這裏只記錄下我在windows下的實踐）:

@REM openjml.cmd
@"C:\Program Files (x86)\Common Files\Oracle\Java\javapath\java.exe" -jar D:\Document\ProgramHome\openjml-0.8.42-20190401\openjml.jar -properties D:\Document\ProgramHome\openjml-0.8.42-20190401\openjml.properties %*

將以上代碼保存爲openjml.cmd並放在任意一個Path中的路徑便可被命令行檢索到並能夠直接使用。經過：

openjml -check -cp JarLib SourceFile.java

能夠實現針對JML語言的語法檢查

openjml -esc -cp JarLib SourceFile.java
openjml -esc -cp JarLib SourceFile.java -nowarn

能夠實現代碼的靜態檢查，給出程序中可能出現的潛在問題，使用-nowarn能夠消除不關心的warning輸出

配合Eclipse使用

OpenJML的命令行使用方式輸出確實不太友好，所以我還嘗試了在Eclipse下安裝相應的插件進行檢查，安裝過程很簡單，經過http://jmlspecs.sourceforge.net/openjml-updatesite便可安裝jml插件，而後在Window->Preferences下對SMT Solver的位置進行一下簡單設置：

jmlspec preferences

就能夠正常使用了，使用時首先選擇一個文件，而後在JML->TypeCheck JML能夠檢查JML的正確性，JML->Static Check (ESC)能夠進行代碼的靜態檢查，JML->*RAC*相關操做能夠生成運行時檢查須要的class文件。我使用這個工具對MyPath.java進行檢查的結果爲：

MyPath_esc

compareTo方法出現INVALID彷佛是由於輸入爲null時出現了錯誤，可是這個在compareTo的前置條件中已經排除了null的狀況，equals方法彷佛也是由於類型問題被斷定爲了INVALID；MyPath構造函數中，JML要求實現的能夠被斷定爲VALID，被斷定爲INVALID的是我額外實現了另外一種構造方式；getUnpleasantValue函數出現了ERROR：

Error occurred while checking method: homework.flymin.MyPath.getUnpleasantValue(int)
錯誤: ESC could not be attempted because of a failure in typechecking or AST transformation: getUnpleasantValue

我經過查閱資料，並無發現這個error的有效解決辦法，同時我也檢查了typechecking過程是沒有問題的，所以問題應該就是出如今AST transformation中，目前我還沒太搞明白。

JMLUnitNG

JMLUnitNG是openjml結合Junit的產物，能夠針對給定的代碼自動生成須要的測試代碼，運行單元測試。但我從網上搜索到的JMLUnitNG相關的資料很是少，所以這部分不少操做尚未太明白，主要操做流程爲：

  1. 首先準備待測代碼

    testng/
├── IntPair.java
├── MyContainer.java
├── MyGraph.java
├── MyPath.java
├── MyPathExtend.java
├── MyRailwaySystem.java
├── Node.java
├── NodeSet.java
└── TicketNode.java

  2. 使用openjml生成動態測試文件(rac)備用：

    cp -r testng testng-o
java -jar ../openjml-0.8.42-20190401/openjml.jar -rac -cp ../specs-homework-3-1.3-raw-jar-with-dependencies.jar testng-o/*.java

  3. 針對待測代碼生成測試代碼的java文件，命令爲：

    java -jar ../JMLUnitNG.jar -cp ../specs-homework-3-1.3-raw-jar-with-dependencies.jar testng/*.java

    執行以後目錄結構爲：

    testng
├── IntPair.java
├── MyContainer.java
├── MyContainer_InstanceStrategy.java
├── MyContainer_JML_Test.java
├── MyGraph.java
├── MyGraph_InstanceStrategy.java
├── MyGraph_JML_Data
│   ├── ClassStrategy_com_oocourse_specs3_models_Path.java
│   ├── ClassStrategy_int.java
│   ├── ClassStrategy_int1DArray.java
│   ├── ClassStrategy_int2DArray.java
│   ├── addPath__Path_path__27__path.java
│   ├── containsEdge__int_fromNodeId__int_toNodeId__0__fromNodeId.java
│   ├── containsEdge__int_fromNodeId__int_toNodeId__0__toNodeId.java
│   ├── containsNode__int_nodeId__0__nodeId.java
│   ├── floidPath__int_size__int2DArray_distance__0__distance.java
│   ├── floidPath__int_size__int2DArray_distance__0__size.java
│   ├── getShortestPathLength__int_fromNodeId__int_toNodeId__0__fromNodeId.java
│   ├── getShortestPathLength__int_fromNodeId__int_toNodeId__0__toNodeId.java
│   ├── isConnected__int_fromNodeId__int_toNodeId__0__fromNodeId.java
│   ├── isConnected__int_fromNodeId__int_toNodeId__0__toNodeId.java
│   ├── removePathById__int_pathId__0__pathId.java
│   └── removePath__Path_path__27__path.java
├── MyGraph_JML_Test.java
├── MyPath.java
├── MyPathExtend.java
├── MyPath_InstanceStrategy.java
├── MyPath_JML_Data
│   ├── ClassStrategy_com_oocourse_specs3_models_Path.java
│   ├── ClassStrategy_int.java
│   ├── ClassStrategy_int1DArray.java
│   ├── ClassStrategy_java_lang_Object.java
│   ├── MyPath__Path_path__27__path.java
│   ├── MyPath__int1DArray_nodeList__0__nodeList.java
│   ├── compareTo__Path_another__27__another.java
│   ├── containsNode__int_nodeId__0__nodeId.java
│   ├── equals__Object_obj__10__obj.java
│   ├── getNode__int_index__0__index.java
│   └── getUnpleasantValue__int_nodeId__0__nodeId.java
├── MyPath_JML_Test.java
├── MyRailwaySystem.java
├── MyRailwaySystem_InstanceStrategy.java
├── MyRailwaySystem_JML_Data
│   ├── ClassStrategy_com_oocourse_specs3_models_Path.java
│   ├── ClassStrategy_int.java
│   ├── ClassStrategy_testng_TicketNode.java
│   ├── addPath__Path_path__27__path.java
│   ├── getLeastTicketPrice__int_fromNodeId__int_toNodeId__0__fromNodeId.java
│   ├── getLeastTicketPrice__int_fromNodeId__int_toNodeId__0__toNodeId.java
│   ├── getLeastTransferCount__int_fromNodeId__int_toNodeId__0__fromNodeId.java
│   ├── getLeastTransferCount__int_fromNodeId__int_toNodeId__0__toNodeId.java
│   ├── getLeastUnpleasantValue__int_fromNodeId__int_toNodeId__0__fromNodeId.java
│   ├── getLeastUnpleasantValue__int_fromNodeId__int_toNodeId__0__toNodeId.java
│   ├── getUnpleasantValue__Path_path__int_fromIndex__int_toIndex__27__fromIndex.java
│   ├── getUnpleasantValue__Path_path__int_fromIndex__int_toIndex__27__path.java
│   ├── getUnpleasantValue__Path_path__int_fromIndex__int_toIndex__27__toIndex.java
│   ├── removeNode__TicketNode_node__7__node.java
│   ├── removePathById__int_pathId__0__pathId.java
│   └── removePath__Path_path__27__path.java
├── MyRailwaySystem_JML_Test.java
├── Node.java
├── NodeSet.java
├── NodeSet_InstanceStrategy.java
├── NodeSet_JML_Data
│   ├── ClassStrategy_int.java
│   ├── ClassStrategy_testng_Node.java
│   ├── getNode__int_nodeId__0__nodeId.java
│   ├── putNode__int_nodeId__0__nodeId.java
│   └── safeRemoveNode__Node_node__7__node.java
├── NodeSet_JML_Test.java
├── Node_InstanceStrategy.java
├── Node_JML_Data
│   ├── ClassStrategy_int.java
│   ├── ClassStrategy_java_lang_Object.java
│   ├── ClassStrategy_testng_Node.java
│   ├── ClassStrategy_testng_Node1DArray.java
│   ├── Node__int_id__0__id.java
│   ├── addNeighbor__Node_node__7__node.java
│   ├── addreachable__Node_node__int_len__7__len.java
│   ├── addreachable__Node_node__int_len__7__node.java
│   ├── equals__Object_obj__10__obj.java
│   ├── getShortestPathLen__Node_another__7__another.java
│   ├── isNeighbor__Node_another__7__another.java
│   ├── reachable__Node_another__7__another.java
│   └── removeNeighbor__Node1DArray_nodes__7__nodes.java
├── Node_JML_Test.java
├── PackageStrategy_com_oocourse_specs3_models_Path.java
├── PackageStrategy_int.java
├── PackageStrategy_int1DArray.java
├── PackageStrategy_int2DArray.java
├── PackageStrategy_java_lang_Object.java
├── PackageStrategy_testng_Node.java
├── PackageStrategy_testng_Node1DArray.java
├── PackageStrategy_testng_TicketNode.java
└── TicketNode.java
    即針對每個方法都生成了相應的測試代碼和數據文件

  4. 而後編譯上述文件，並替換待測代碼對應的class爲openjml rac編譯的class

    javac -cp ../JMLUnitNG.jar:../specs-homework-3-1.3-raw-jar-with-dependencies.jar testng/*.java testng/*/*.java
cp testng-o/*.class testng

  5. 運行測試（這裏運行了較爲簡單的MyPath）

    gaoruiyuan@THINK-X1E:/mnt/d/Document/ProgramHome/Java$ java -cp ./:../JMLUnitNG.jar:../specs-homework-3-1.3-raw-jar-with-dependencies.jar testng.MyPath_JML_Test
[Parser] Running:
Command line suite

Passed: racEnabled()
Passed: constructor MyPath(null)
Passed: constructor MyPath(null)
Passed: constructor MyPath({})
Failed: <<testng.MyPath@2f333739>>.compareTo(null)
Passed: <<testng.MyPath@4cc77c2e>>.containsNode(-2147483648)
Passed: <<testng.MyPath@7a7b0070>>.containsNode(0)
Passed: <<testng.MyPath@71bc1ae4>>.containsNode(2147483647)
Passed: <<testng.MyPath@2437c6dc>>.equals(null)
Passed: <<testng.MyPath@299a06ac>>.equals(java.lang.Object@383534aa)
Passed: <<testng.MyPath@6bc168e5>>.getDistinctNodeCount()
Failed: <<testng.MyPath@7b3300e5>>.getNode(-2147483648)
Failed: <<testng.MyPath@2e5c649>>.getNode(0)
Failed: <<testng.MyPath@136432db>>.getNode(2147483647)
Passed: <<testng.MyPath@3caeaf62>>.getUnpleasantValue(-2147483648)
Passed: <<testng.MyPath@e6ea0c6>>.getUnpleasantValue(0)
Passed: <<testng.MyPath@6a38e57f>>.getUnpleasantValue(2147483647)
Passed: <<testng.MyPath@5577140b>>.isValid()
Passed: <<testng.MyPath@1c6b6478>>.iterator()
Passed: <<testng.MyPath@67f89fa3>>.size()

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

能夠看到出現了幾處Failed，對於compareTo方法，測試中仍舊是在傳入null時出現了錯誤，返回測試代碼進行了相應的修改，getNode方法須要實例知足某個狀態才能正確表現，這裏暫時跳過了這個方法；compareTo方法及其檢測方法中加上了對null的響應操做，以後再次運行測試：

gaoruiyuan@THINK-X1E:/mnt/d/Document/ProgramHome/Java$ java -cp ./:../JMLUnitNG.jar:../specs-homework-3-1.3-raw-jar-with-dependencies.jar testng.MyPath_JML_Test
[Parser] Running:
  Command line suite

Passed: racEnabled()
Passed: constructor MyPath(null)
Passed: constructor MyPath(null)
Passed: constructor MyPath({})
Passed: <<testng.MyPath@2f333739>>.compareTo(null)
Passed: <<testng.MyPath@4cc77c2e>>.containsNode(-2147483648)
Passed: <<testng.MyPath@7a7b0070>>.containsNode(0)
Passed: <<testng.MyPath@71bc1ae4>>.containsNode(2147483647)
Passed: <<testng.MyPath@2437c6dc>>.equals(null)
Passed: <<testng.MyPath@299a06ac>>.equals(java.lang.Object@383534aa)
Passed: <<testng.MyPath@6bc168e5>>.getDistinctNodeCount()
Skipped: <<testng.MyPath@7b3300e5>>.getNode(-2147483648)
Skipped: <<testng.MyPath@2e5c649>>.getNode(0)
Skipped: <<testng.MyPath@136432db>>.getNode(2147483647)
Passed: <<testng.MyPath@3caeaf62>>.getUnpleasantValue(-2147483648)
Passed: <<testng.MyPath@e6ea0c6>>.getUnpleasantValue(0)
Passed: <<testng.MyPath@6a38e57f>>.getUnpleasantValue(2147483647)
Passed: <<testng.MyPath@5577140b>>.isValid()
Passed: <<testng.MyPath@1c6b6478>>.iterator()
Passed: <<testng.MyPath@67f89fa3>>.size()

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

這個結果目前來看是比較和理想中相符的了。

架構設計與重構分析

繼承式增量設計

由於這個單元的代碼做業是給出JML的，咱們須要作的是給出相應的代碼實現，因此能夠理解爲相應的總體架構在JML中已經肯定了，所以三次代碼做業下來我並無作太多重構性的工做。其實官方倉庫給出的規格也是繼承式的，所以我也按照一致的思路，每次繼承上一次的設計再在其基礎上拓展功能實現新的接擴方法。因此，這個單元的做業在我看來一直是一種增量使得設計，只要保證方法的獨立性，即方法、類實現之間沒有相互依賴，就可以保證在需求增長時能夠直接擴展而沒必要要所有從新設計。這一點也可以經過類圖來體現：

第一次

第一次做業不管從JML規格仍是實現方法來說我都沒有作太複雜的操做，固然，想的太簡單的也是要付出代價的。但從類圖裏面能夠看出，Path和PathContainer之間是沒有任何直接聯繫的，因此我保證了只要是按照JML實現的代碼，對於個人實現方式來講都是能夠兼容替換的。

第二次

第二次做業針對PathContainer進行了擴展，創建了圖結構，我就在完善第一次做業的代碼的基礎上，直接繼承了MyPath造成了MyGraph，只是將相關的發放進行了重寫，同時增長了新的方法，並無破壞原代碼的結構。另外，這樣作的好處就是我能夠把和圖運算相關的操做所有保留在MyGraph中，很天然的就能夠和原來的運算分離開，沒必要擔憂這兩部分相互之間出現問題。能夠看出，在此次做業中，MyPath仍舊是獨立的結構，這與其定義的初衷相吻合。實現中，我對於NodeSet使用了單例模式保證其成爲一個全局可訪問的節點集合，這樣的分離設計也使得出錯的可能性大爲下降。

第三次

第三次做業個人思路仍然沒有變，我依舊是擴展了第二次做業的類設計，在繼承原來的類的基礎上加上了新的功能。但此次爲了實現getUnpleasantValue方法同時盡力保持MyPath類本來的獨立性，我在繼承這個類的基礎上進行了擴展，實現了MyPahtExtend類，增長了一些創建局部圖計算最短加權路徑的算法，即便這樣，MyPath類相對的獨立性也沒有受到影響。

算法與數據結構

數據結構上，我三次做業採用的都是鄰接表的結構存儲圖節點，節點自己使用一個HashSet，但由於Set集合並不能隨機讀，所以後來我改爲了HashMap，在保證沒有重複的同時也可以堆積訪問節點Id到節點對象的映射。對於可達節點我仿照鄰居節點處理，也作成了一個Map，表示可達節點以及相應的最短路徑。

值得一提的時，在第三次做業中我須要用到一個無序的Pair結構做爲Map的Key，但Java好像並無提供這樣的機制，所以我本身建立了一份IntPair類做爲索引，由於無須，因此能夠減小一半的冗餘存儲（對於無向圖）。

算法方面，我一直採用了Floyid全局最短路的算法，第三單元中，我將重複節點拆開存儲建圖，而後繼續使用全局最短路。這樣的算法在圖結構較小時效果不錯，當圖結構龐大並且點沒法進行合併時複雜度會急劇上升。我在進行第三單元測試的時候忽視了這一點，知道DDL前一小時才發現，根據需求給出來的數據量，若是節點不進行合併數據規模很容易上千，而這樣的數據量是根本沒法再規定的時間內跑完$O(n^3)$的Floyid算法的，但已經來不及改了，所以第三次做業也出現了大量的超時。

bug與代碼分析

bug分析

這三次做業下來我沒有什麼邏輯上的bug，出現的問題基本都是超時錯誤。第一次做業中我沒有進行任何基本的優化，致使超時；做業二我吸收教訓作了很多優化，所以獲得了滿分；但做業三我覺得做業二的算法依舊適用，所以沒有更換算法，致使出現了更大面積的TLE。

代碼分析

此次的度量分析我只針對第三次做業給出，由於每次都是在前一次的基礎上進行擴展，因此最後一次做業實際上涵蓋了全部三次的代碼實現。

  • 代碼量分析

code

從數據中能夠看出，由於每次只須要作增量設計，因此類的長度仍是比較合理的。但即便是繼承，也免不了須要重寫方法，所以最長的MyRailwaySystem有334行代碼，規模也算不小了。

  • 方法複雜度分析

    這單元做業的方法複雜度分析以下，存在兩個複雜的條件判斷，三個複雜的方法，這三個複雜的方法的循環複雜度均爲9，是計算最短路徑的三個主要方法，其餘方法的複雜度都不高，循環複雜度（CC）平均值爲2.067。方法的平均代碼行數爲8.78，能夠說這個水平對於縮小函數長度來講仍是比較理想的。

Type Name Method Name Code Smell
MyContainer getPathId Complex Conditional
MyGraph removePath Complex Conditional
MyGraph calShortestPathLength Complex Method
MyRailwaySystem calTicket Complex Method
MyRailwaySystem calChange Complex Method

  • 類複雜度分析

    總體來看經過集成實現的設計方法使得類之間的複雜性控制的仍是比較均衡的，最複雜的那幾個類不出所料的集中在MyContainer、MyGraph和MyRailwayStation。部分圖算法爲了提升相同片斷的複用性被放在了TicketNode類中，所以也讓這個類顯得有些複雜，但實際上並無太多本身的運算——這可能就是複雜點的工程設置util的重要性吧。

Type Name NOF(屬性數量) NOM(方法數) NOPM(public方法數) LOC(行數) WMC(加權方法複雜度) LCOM(方法之間缺少聚協力的程度)
IntPair 2 3 2 33 6 0
Main 0 1 1 15 1 -1
MyContainer 3 13 13 50 15 0.462
MyGraph 2 13 10 216 35 0.692
MyPath 2 11 11 90 24 0.364
MyPathExtend 1 3 2 56 10 0.667
MyRailwaySystem 9 17 10 288 61 0.235
Node 3 14 14 107 23 0
NodeSet 2 8 8 64 12 0.25
TestMain 0 1 1 10 1 -1
TicketNode 6 21 19 141 29 0.143

單元感悟

經過這個單元的學習，我體會到了使用JML進行代碼約束的方便，有了JML，實現與需求之間的交互變得明朗起來，並且困擾程序員好久的程序正確性證實也有了好的出口。更關鍵的是，JML的使用不只在工程師交付環節起到關鍵做用，在模式設計、合做任務分配時也會有十分重要的應用，遵照JML進行編程可以使得不一樣來源的程序得到最好的兼容性，並且不須要閱讀代碼就能清楚的知道責任劃分（如前置條件和後置條件），從而在一開始就避免可能出現的bug。我有一個很深的體會就只以前寫代碼時並無一個很強的總體感，基本是一邊想一邊寫，這樣雖然能很快動手，可是代碼量一多就會發現隨着相互的調用關係變得負責，函數之間的責任劃分變得不那麼明確，這時候爲了保證正確性不得不作不少冗餘的check工做，而使用JML正好能夠避免這個問題，輔助咱們在一開始就作好設計並在設計完成後給出合理的驗證。

相關文章
相關標籤/搜索
每日一句
    每一个你不满意的现在，都有一个你没有努力的曾经。
本站公眾號
   歡迎關注本站公眾號,獲取更多信息
聯繫我們 最近搜索 最新文章 沪ICP备13005482号-10 MyBatis教程 SQL 教程 MySQL教程 Java 教程 Thymeleaf 教程 Hibernate教程 Spring教程 Redis教程