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