BUAA_OO_博客做業3——規格

時間  2020-05-05
標籤 buaa 博客 規格 简体版
原文   原文鏈接

BUAA_OO_博客做業3——規格

 

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

JML是java modeling language的縮寫，是一種描述性質的語言。有必定的語法規則。java

這種語言被用來描述一段代碼的具體行爲，好比前置條件、反作用、後置條件等。node

JML的語法能夠用專門的工具來檢測是否合乎規範。算法

應用工具鏈

OpenJML數組

官網：http://www.openjml.org/downloads/數據結構

JMLUnitNG架構

官網：http://insttech.secretninjaformalmethods.org/software/jmlunitng/dom

jar連接：http://insttech.secretninjaformalmethods.org/software/jmlunitng/assets/jmlunitng.jaride

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

未解決：工具

C:\Users\LiTianYu>java -jar E:\tmp\JMLUnitNG.jar E:\tmp\MyPath1.java
JMLUnitNG exited because of an irrecoverable error:
org.jmlspecs.jmlunitng.JMLUnitNGError: Encountered 5 compilation errors:
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/ArrayList.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/AbstractList.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/AbstractCollection.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Object.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/Collection.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Iterable.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/List.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/AbstractList$ListItr.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/AbstractList$Itr.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/RandomAccess.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Cloneable.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/io/Serializable.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/ArrayList$ArrayListSpliterator.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/ArrayList$SubList.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/ArrayList$ListItr.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/ArrayList$Itr.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/Iterator.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Integer.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Number.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Comparable.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Integer$IntegerCache.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
E:\tmp\MyPath1.java:5: 錯誤: 已在類 MyPath1中定義了變量 nodes
        //@ public instance model non_null int[] nodes;
                                                 ^
E:\tmp\MyPath1.java:5: 錯誤: The field nodes in the specification matches a Java field MyPath1.nodes with different modifiers: public private
        //@ public instance model non_null int[] nodes;
                                                 ^
E:\tmp\MyPath1.java:5: 錯誤: The field nodes in the specification matches a Java field MyPath1.nodes but they have different types: int[] vs. ArrayList<Integer>
        //@ public instance model non_null int[] nodes;
                                              ^
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/ArrayList.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()': 找不到jdk.Profile+Annotation的類文件
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/AbstractList.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/AbstractCollection.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Object.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/Collection.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Iterable.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/List.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/RandomAccess.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Cloneable.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/io/Serializable.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/util/Iterator.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Integer.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Number.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Comparable.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
警告: E:\tmp\jmlruntime.jar(org/jmlspecs/annotation/Instance.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Annotation.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: E:\tmp\jmlruntime.jar(org/jmlspecs/annotation/Model.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: E:\tmp\jmlruntime.jar(org/jmlspecs/annotation/NonNull.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Retention.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/RetentionPolicy.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Annotation.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Target.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/ElementType.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Retention.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/RetentionPolicy.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/Target.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/annotation/ElementType.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/AutoCloseable.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/AutoCloseable.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Byte.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Byte.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Character.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Character.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Short.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/Short.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'
E:\tmp\MyPath1.java:74: 錯誤: An identifier with private visibility may not be used in a ensures clause with public visibility
      @ ensures \result == nodes[index];
                           ^
E:\tmp\MyPath1.java:74: 錯誤: 須要數組, 但找到ArrayList<Integer>
      @ ensures \result == nodes[index];
                                ^
警告: C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/RuntimeException.class): 主版本 52 比 51 新, 此編譯器支持最新的主版本。
  建議升級此編譯器。
C:\Program Files\Java\jdk1.8.0_201\lib\ct.sym(META-INF/sym/rt.jar/java/lang/RuntimeException.class): 警告: 沒法找到類型 'Profile+Annotation' 的註釋方法 'value()'

        at org.jmlspecs.jmlunitng.JMLUnitNG.processAllCompilationUnits(JMLUnitNG.java:527)
        at org.jmlspecs.jmlunitng.JMLUnitNG.run(JMLUnitNG.java:414)
        at org.jmlspecs.jmlunitng.JMLUnitNG.main(JMLUnitNG.java:177)

 規格中//@ public instance model non_null int[] nodes;實際實現爲ArrayList學習

報錯須要數組，不太明白應當怎麼解決

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

這三次做業主要構建了路徑，路徑容器、圖、地鐵圖；

個人設計中都使用了Java原有的一些容器（包括ArrayList和HashMap）；

因爲第一次做業在時間上爆炸了，因此我後兩次的做業使用了冗餘數據和更好的數據結構來方便訪問、查詢等；

整體架構上，Path的變更不大，由於Path在第一次做業寫得時候就已經寫成比較優秀的狀態了，因此後續不太須要變更。

變更主要體如今三次依次加深的部分。因爲三次逐漸增長了功能，致使原有數據結構使用不便，因此後來進行了數據結構方面的重構。

在後兩次次做業中，我使用了頂點集、邊集來模擬無向圖、地鐵圖。其中查詢功能分散到頂點集、邊集或者路徑的數據結構中。

頂點集主要負責查詢點的存在性、數量等；路徑的數據結構負責根據id查路徑或者根據路徑查id；邊集負責其餘複雜的計算（如最短路等）。

須要提到的是，在計算最短路、連通塊數時，邊集須要使用到頂點集，這也是我設計中的一個缺陷。我不得不把頂點集做爲參數傳給邊集。

具體的算法實現主要是採用了BFS、迪傑斯特拉和並查集。

第一次做業類圖：

 

第二次做業類圖：

 

第三次做業類圖：

 三次做業複雜程度逐漸增長；其中能夠看出第二次和第三次的設計存在一些缺陷（如邊集和點集應當封裝到一個圖類裏等）

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

實際上第一次和第二次都沒有邏輯上的bug，第一次在強測時候的時間複雜度上被卡了25分；

第二次就使用HashMap代替了原用的ArrayList而且有多個冗餘的HashMap來方便根據不一樣的Key查詢不一樣的Value；

值得一提的是，我在寫完第二次做業以後得意忘形，忘記修復第一次做業的bug了（劃掉）

第三次做業真真正正出現了所謂的邏輯上的bug。這個bug出現的實際緣由是由於我使用了PriorityQueue，優先隊列。

然而我並無搞懂它自動維護順序的機制，誤覺得一旦修改容器內的對象，容器也會自動維護。

如今想一想這個想法也太搞笑了。實際修復花費的時間主要在思考bug出現的緣由上。發現這個緣由以後，僅僅添加6行就完成了修復。

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

我認爲規格的撰寫是爲了較大型的軟件開發或者團隊開發而誕生的。

在整體上，有一個總的規劃，先確保總的邏輯正確性，再分別實現小的部分，這很OO。

也就是說，每一個對象（或者方法），都假設別人完成了別人的工做，而後本身也確保本身完成本身應有的工做，那麼整個系統就能協調地運行了。

我的理解，規格的給出就相似於架構師，而具體實現則是「碼農」的工做。架構師負責整體架構設計，碼農負責細節處理。各司其職，各背其鍋。

須要注意的是，規格中常常有對於數據結構的一個臨時性描述，而實際上並非必須使用這種數據結構。

這樣設計一個描述性的數據結構只是爲了JML描述方便而已，實際實現應當考慮需求而設計合適的實現方法。（好比考慮響應時間或者內存佔用等）

撰寫一個大項目的JML並非一個容易的事情，是須要鍛鍊的。所以咱們也不能止步於當前的這一點點學習，更應該向長遠將來看去，鍛鍊本身昇華本身。

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