OO第三单元总结：JML
目錄
- 第三單元——jml、junit與圖
第三單元——jml、junit與圖
〇、問題描述
? 本單元主題為JML的學習，問題載體為一個無向圖路徑管理系統。在三次作業種，情景不變，需求遞增。因此需要在層次上做好安排。
一、JML語言
理論基礎(Level 0)
注釋結構
// @annotation 行注釋
/* @annotation*/ 塊注釋
JML表達式
原子表達式
\result 方法執行后的返回值
\old(expr) 表達式expr在方法執行前的值
\not_assigned(expr) 表達式expr是否被賦值
\not_modified(x,y,...) 表達式expr是否變化
\nonnullelements( container ) 表達式：表示 container 對象中存儲的對象不會有 null
\type(type) 表達式：返回類型type對應的類型(Class)
量化表達式
\forall 全稱修飾
(\forall int i,j; 0 <= i && i < j && j < 10; a[i] < a[j])\exists 存在修飾
(\exists int i; 0 <= i && i < 10; a[i] < 0)\sum 給定范圍內的表達式的和
(\sum int i; 0 <= i && i < 5; i)\product 給定范圍內的表達式的連乘結果
\max min 給定范圍內的表達式的最大/小值
\num_of 指定變量中滿足相應條件的取值個數
集合表達式
操作符
<: 子類型關系操作符
<==> <=!=>等價關系操作符
==> <== 推理操作符
\nothing \everything 變量引用操作符
方法規格
requires 前置條件
ensures 后置條件
assignable 可賦值
modifiable 可修改
public normal_behavior 正常功能
signals 拋出異常
類型規格
invariant 不變式
constraint 狀態變化約束
應用工具鏈
? lowa State JML ： 提供了一個斷言檢查編譯器jmlc，將JML注釋轉換為運行時的斷言；
? jmldoc： 文檔生成器，用于生成Javadoc文檔，增加了來自JML注釋的額外信息。
? jmlunit： 單元測試生成器可以從JML注釋中生成JUnit測試代碼。
二、JMLUnitNG/JMLUnit
public class Demo {/*@ public normal_behaviour@ ensures \result == a + b;@*/public static int add(int a, int b) {return a + b;}public static void main(String[] args) {add(12,3);} }[TestNG] Running:
Command line suite
Passed: racEnabled()
Passed: constructor Demo()
Passed: static add(-2147483648, -2147483648)
Passed: static add(0, -2147483648)
Passed: static add(2147483647, -2147483648)
Passed: static add(-2147483648, 0)
Passed: static add(0, 0)
Passed: static add(2147483647, 0)
Passed: static add(-2147483648, 2147483647)
Passed: static add(0, 2147483647)
Passed: static add(2147483647, 2147483647)
Passed: static main(null)
Passed: static main({})
===============================================
Command line suite
Total tests run: 13, Failures: 0, Skips: 0
===============================================
三、程序設計
類的設計——繼承與遞進
簡析三次作業涉及到的指令及實現方式：
第一次：HashMap管理路徑
// 兩個對應的 HashMap 存儲，加快查找 private HashMap<Integer/*id*/,MyPath/*path*/> pathList; private HashMap<MyPath/*path*/,Integer/*id*/> pidList; // 在添加和刪除時管理總點數，分攤復雜度 private HashMap<Integer/*node*/,NumberOfNode/*number of node*/> distinct;// hashcode的設定 /*path*/ @Overridepublic int hashCode() {return nodes.hashCode();} /*integer*/Integer.hashCode();添加刪除類 O(n)
在兩個表中添加/刪除路徑；管理節點數目。包括：
- 添加路徑
- 刪除路徑
- 根據id刪除
查詢類 O(1)
包括：
- 查詢id
- 查詢路徑
- 獲取總路徑數
- 根據id獲取路徑大小
- 根據結點序列判斷容器是否包含路徑
- 根據路徑id判斷容器是否包含路徑
- 容器內不同結點個數
- 路徑中是否包含某個結點
根據id獲取不同節點個數 O(n)
path內排序+遍歷第一次為O(n)，其后為O(1)
根據字典序比較兩個路徑的大小關系 O(n)
第二次：HashMap存儲鄰接表管理無向圖
// 鄰接表：邊權均為1的無向圖 private HashMap<Integer/*起點*/,HashMap<Integer/*終點*/,Integer/*邊數*/>> reachable= new HashMap<>();邊的存在性 O(1)
bfs 搜索 O(v+e)
包括：
兩個結點是否連通
最短路徑存在
兩個結點之間的最短路徑
第三次：UndirectedGraph
含有圖的嵌套關系；圖的連接狀態相同但邊權不同。新增一類專門管理。
abstract class UndirectedGraph {// 無向圖private HashMap<Integer/*point*/,HashMap<Integer/*point*/,Integer/*weight*/>> undirectedGraph;// 緩存區private HashMap<Integer/*point*/,HashMap<Integer/*point*/,Integer/*weight*/>> cache;private bfs(){}private spfa(){}... }以下復雜度討論均不考慮緩存查找。（重復查詢時O(1)）
連通塊數量
涂色
spfa
本質上都是帶權最短路徑的問題。。。以前的沙雕方法都重寫了。
- 最低票價
- 最少換乘次數
- 最少不滿意度
- 最短路徑
- 兩點連通性
三次架構
- 第一次：哈希表+規格方法
- 第二次：添加可達表，原有方法不變
- 第三次：添加圖，重寫查找算法相關方法
算法
第二次：bfs
第三次：每條path內部先構建好小圖，即建立好所有的邊，這樣在每一條邊上加上換乘權值，搜最短路 ( spfa ) 就行。共需三個權值不同的圖。
因為查詢指令較多，應每次搜索都將當前起點的所有終點最短路都放入緩存。每當圖結構更改應該清空緩存。
四、BUG分析
? （本地bug）寫第三次作業時，bfs寫成找到目標終點即停止：
while (size != 0) {if(fr==to) return;//...for (Integer x : keySet()) {//...} }? 導致第二次搜索時進行不下去。應改成一次性搜索完所有終點。
五、心得體會
? 對于jml，語法是相對簡單，理解也相對容易。難點在于自己寫出一份規范的規格。因為寫規格的成本比寫代碼高出太多，我對jml仍僅僅停留在了解階段，還需要更多的學習。畢竟，第三單元的作業架構嚴格來說幾乎沒有自己參與……由此也可見得架構對于程序正確性、效率和可擴展性的重要性。
轉載于:https://www.cnblogs.com/DilemmaR/p/10908548.html
總結
以上是生活随笔為你收集整理的OO第三单元总结：JML的全部內容，希望文章能夠幫你解決所遇到的問題。
- 上一篇： DataTime转Varchar
- 下一篇： Robot Framework-Ride