目錄

• JML語(yǔ)言學(xué)習(xí)筆記
  • 理論基礎(chǔ)
  • 應(yīng)用工具鏈情況
  • JMLUnit/JMLUnitNG
• UNIT3 作業(yè)分析
  • 作業(yè) 3-1 實(shí)現(xiàn)兩個(gè)容器類Path和PathContainer
  • 作業(yè) 3-2 實(shí)現(xiàn)容器類Path和數(shù)據(jù)結(jié)構(gòu)類Graph
  • 作業(yè) 3-3 實(shí)現(xiàn)容器類Path，地鐵系統(tǒng)類RailwaySystem
• 規(guī)格撰寫的心得與體會(huì)
• 最后，衷心感謝為這門課程辛苦付出的老師和助教。???

JML語(yǔ)言學(xué)習(xí)筆記

理論基礎(chǔ)

1. 注釋結(jié)構(gòu)

2. JML表達(dá)式

• 原子表達(dá)式，量化表達(dá)式，集合表達(dá)式，操作符，etc.

3. 方法規(guī)格

• 前置條件(pre-condition)
• 后置條件(post-condition)
• 副作用范圍限定(side-effects)

4. 類型規(guī)格

• 不變式(invariant)
• 狀態(tài)變化約束(constraint)

應(yīng)用工具鏈情況

1. OpenJML & SMT Solver

• 首先由OpenJML將JML規(guī)格轉(zhuǎn)換乘SMT-LIB格式的代碼，然后調(diào)用SMT solver進(jìn)行檢查。用于靜態(tài)檢查。

2. JMLUnitNG

• 根據(jù)規(guī)格自動(dòng)生成測(cè)試文件。用于自動(dòng)測(cè)試。

3. JMLdoc

• 可以快速生成JML文檔的相關(guān)文件

4. Junit

• Junit主要用于單元化測(cè)試與一定的自動(dòng)化測(cè)試，配合JML食用效果極佳。

JMLUnit/JMLUnitNG

1. 前期準(zhǔn)備

• 簡(jiǎn)單代碼示例與jar包配置

2. 命令行操作

java -jar jmlunitng.jar src/Demo.java javac -cp jmlunitng.jar src/*.java

3. 測(cè)試結(jié)果

4. 結(jié)果分析

• 我們可以看出，自動(dòng)生成的測(cè)試樣例對(duì)各種極端情況進(jìn)行了測(cè)試，具有較好的覆蓋性。
• 但是，在試驗(yàn)過(guò)程中，JML測(cè)試的局限性也被暴露出來(lái)了。

UNIT3 作業(yè)分析

作業(yè) 3-1 實(shí)現(xiàn)兩個(gè)容器類Path和PathContainer

1. 架構(gòu)設(shè)計(jì)

1）度量分析

2）結(jié)構(gòu)分析

3）算法分析

• MyPath

  • // path的存儲(chǔ)結(jié)構(gòu)，用來(lái)順序存儲(chǔ)結(jié)點(diǎn) private ArrayList<Integer> arrayNodes; // 用來(lái)存儲(chǔ)一條path中的node的個(gè)數(shù)（無(wú)重復(fù)）。key：結(jié)點(diǎn)名稱；value：該結(jié)點(diǎn)出現(xiàn)的次數(shù) private HashMap<Integer, Integer> hashNodes;
  • ADD： 1）讀入一個(gè)結(jié)點(diǎn)數(shù)組 2）將結(jié)點(diǎn)順序存入arrayNodes 3）遍歷結(jié)點(diǎn)數(shù)組，對(duì)于任一結(jié)點(diǎn)node，若node不在hashNodes中，即存入(node, 1)；若已存在，即存入(node, value + 1)。

• MyPathContainer

  • private int id = 0; // pathID private HashMap<Path, Integer> hashPaths; // Path --> PathID private HashMap<Integer, Path> hashIds; // PathID --> Path private HashMap<Integer, Integer> nodes; // Node --> frequentNumber
  • ADD: 原理與path相同REMOVE： 1）hashIds.remove(pathID)，hashPaths.remove(path) 2）對(duì)于path中的每一個(gè)node，（設(shè)node的出現(xiàn)次數(shù)為frequentNumber），若frequentNumber=1，則將node從nodes中移除；若frequentNumber>1，則 nodes.replace(node, frequentNumber-1)。

2. BUG分析

1）bug情況

• 由于測(cè)試數(shù)據(jù)量的限制，程序在評(píng)測(cè)與互測(cè)環(huán)節(jié)沒(méi)有出現(xiàn)錯(cuò)誤。

2）修復(fù)情況

• 該程序存在一些不優(yōu)美的地方，如MyPath中，利用HashMap來(lái)存儲(chǔ)不同結(jié)點(diǎn)是復(fù)雜的，可以說(shuō)是自己造了個(gè)輪子，改正方法為使用HashSet進(jìn)行存儲(chǔ)，通過(guò)容器的特性來(lái)減少手動(dòng)判斷。

---

作業(yè) 3-2 實(shí)現(xiàn)容器類Path和數(shù)據(jù)結(jié)構(gòu)類Graph

1. 架構(gòu)設(shè)計(jì)

1）度量分析

2）結(jié)構(gòu)分析

3）算法分析

• AlGraph

  • // alGraph: node1 --> (node2 -> node2_frequentNumber) private HashMap<Integer, HashMap<Integer, Integer>> alGraph; // edges: node1 --> (node2 -> shortestPathLength_From_Node1_To_Node2) private HashMap<Integer, HashMap<Integer, Integer>> edges;
  • // 由原始圖（alGraph）生成距離圖（edges）的算法 ———— Floyd算法 for (k = 0; k< MAX; k++) for (i = 0; i < MAX; i++) for (j = 0; j < MAX; j++) if (Graph[i][j] > Graph[i][k] + Graph[k][j]) Graph[i][j] = Graph[i][k] + Graph[k][j];
  • public boolean containsEdge(int node1, int node2) {return alGraph.get(node1).containsKey(node2); } public boolean isConnected(int node1, int node2) {if (node1 == node2) return true;else return edges.get(node1).containsKey(node2); } public int getShortestPathLength(int node1, int node2) {if (node1 == node2) return 0;else return edges.get(node1).get(node2); }

4）迭代中對(duì)架構(gòu)的重構(gòu)

• AlGraph繼承了上一次作業(yè)中的PathContainer，并進(jìn)行了適當(dāng)?shù)臄U(kuò)充（具體擴(kuò)充見(jiàn)如上算法分析）。

2. BUG分析

1）bug情況

• 測(cè)試數(shù)據(jù)量增大時(shí)，程序出現(xiàn) CPU_TIME_LIMIT_EXCEED 的錯(cuò)誤。
• 原因（據(jù)我分析）：在Floyd算法中加入的大量的判斷，當(dāng)數(shù)據(jù)量增大時(shí)，造成CPU的負(fù)擔(dān)過(guò)大，運(yùn)算超時(shí)。

2）修復(fù)情況

• 重構(gòu)后UML圖

• 算法分析

  • private final int biggest = 999999999; // 極大數(shù)（自由定義，小于2^31即可） private int id = 0; // PathID（同上一次作業(yè)） private HashMap<Path, Integer> pathToId; // Path --> PathID（同上一次作業(yè)） private HashMap<Integer, Path> idToPath; // PathID --> Path（同上一次作業(yè)） private HashMap<Integer, Integer> nodeToSum; // Node --> Node_Sum（同上一次作業(yè)） private HashMap<Integer, Integer> nodeToIndex; // Node --> Node_index_in_matrix private HashSet<Integer>[] adjVexSets; // 臨界表：Node--Set{node1, node2, ...} private int[][] disMatrix; // Graph生成的存儲(chǔ)各點(diǎn)之間距離的距離矩陣 private Stack<Integer> indexStack; // 用來(lái)維護(hù)node<->index的映射的棧
  • '映射關(guān)系建立機(jī)制，搭建點(diǎn)與數(shù)組下標(biāo)的關(guān)系 if put_New_Node_Into_Graph then bond_NewNode_to_IndexStack.pop() else if remove_Node_From_Graph then indexStack.push(oldNode.index)

3）前后對(duì)比

• // 原程序，floyd部分代碼 for (int k : tempEdges.keySet()) for (int i : tempEdges.keySet()) for (int j : tempEdges.keySet()) if (tempEdges.get(i).containsKey(k) && tempEdges.get(k).containsKey(j)) { int via = tempEdges.get(i).get(k) + tempEdges.get(k).get(j);if (tempEdges.get(i).containsKey(j)) {if (tempEdges.get(i).get(j) > via) {tempEdges.get(i).replace(j, via);}} else {tempEdges.get(i).put(j, via);}}
• // 重構(gòu)后，floyd部分代碼 for (int k = 0; k < 255; k++) for (int i = 0; i < 255; i++) for (int j = 0; j < 255; j++) if (disMatrix[i][j] > (newDis = disMatrix[i][k] + disMatrix[k][j])) disMatrix[i][j] = newDis;

---

作業(yè) 3-3 實(shí)現(xiàn)容器類Path，地鐵系統(tǒng)類RailwaySystem

1. 架構(gòu)設(shè)計(jì)

1）度量分析

2）結(jié)構(gòu)分析

3）算法分析

• MyRailwaySystem

  • private int cbCount = 0; // 連通塊個(gè)數(shù) private int[][] disMatrix; // 距離矩陣 private int[][] transferMatrix; // 最小換乘矩陣 private int[][] priceMatrix; // 價(jià)格矩陣 private int[][] happyMatrix; // 最低不滿意度矩陣
  • // 下面是算法的偽代碼，以價(jià)格矩陣的更新為例，其它類似 private void updatePriceMatrix() {priceMatrix = initMatrix(2);for (Each path : paths) {maxSize = path.size();priceArray = ((MyPath)path).getPriceArray();nodeMap = ((MyPath)path).getNodeMap();for (Each node1, node2 : nodeMap)if (priceArray[tempId1][tempId2] + 2 < priceMatrix[index1][index2]) priceMatrix[index1][index2] = priceMatrix[index2][index1] = priceArray[tempId2][tempId1] + 2;}floyd(priceMatrix, 125); }

4）迭代中對(duì)架構(gòu)的重構(gòu)

• MyPath

  • 在MyPath添加了兩個(gè)距離矩陣，用來(lái)存儲(chǔ)一個(gè)Path（地鐵線路）內(nèi)部的（加權(quán)）距離信息。

  • 首先，將Path構(gòu)建成兩個(gè)加權(quán)無(wú)向圖（權(quán)值分別為價(jià)格和滿意度）；然后，通過(guò)Floyd算法生成各自的距離矩陣，存儲(chǔ)下來(lái)。

  • private int[][] priceArray; // 加權(quán)（價(jià)錢）距離矩陣 private int[][] happyArray; // 加權(quán)（滿意度）距離矩陣 // 以下是算法的偽代碼 private void updateMatrix() {setNodeMap(); // 重新建立映射關(guān)系priceArray = initMatrix(nodeCount, 2); // 距離矩陣初始化happyArray = initMatrix(nodeCount, 32); // 距離矩陣初始化for (Each node1, node2 ：nodes) { // 建圖賦權(quán)priceArray[node1.index][node2.index] = priceArray[node2.index][node1.index] = 1;happyArray[node1.index][node2.index] = happyArray[node2.index][node1.index] = = CalculatePleasure();}floyd(priceArray); floyd(happyArray); // 計(jì)算各點(diǎn)之間距離 }

2. BUG分析

1）bug情況

• 這種算法在測(cè)試數(shù)據(jù)（最多結(jié)點(diǎn)數(shù)以及最多圖變動(dòng)指令數(shù)）有所約束時(shí)，展現(xiàn)出非常出色的性能。在強(qiáng)測(cè)與互測(cè)中均未出現(xiàn)錯(cuò)誤。
• 但是，我的代碼結(jié)構(gòu)有著較為嚴(yán)重的問(wèn)題：幾乎完全面向過(guò)程的寫法嚴(yán)重違反了OOP的原則；多個(gè)相似結(jié)構(gòu)重復(fù)計(jì)算等。

2）修復(fù)情況

• 尚未進(jìn)行代碼重構(gòu)，僅對(duì)課程組給出的標(biāo)程進(jìn)行了研究，并進(jìn)行了簡(jiǎn)單的算法優(yōu)化嘗試。

規(guī)格撰寫的心得與體會(huì)

• 規(guī)格化設(shè)計(jì)和契約式編程，讓人如沐清風(fēng)，受益匪淺。 其實(shí)這次的代碼工程量很大，但是由于課程組給出的JML的引導(dǎo)以及課程組已經(jīng)將我們需要填寫的代碼抽象成了接口，這使得我們?cè)趯懘a時(shí)會(huì)產(chǎn)生一種錯(cuò)覺(jué)——“這是面向?qū)ο笳n程嗎？”、“這是數(shù)據(jù)結(jié)構(gòu)補(bǔ)習(xí)課吧！”…… 這正是規(guī)格化設(shè)計(jì)和契約式編程 的巨大作用。
• JML語(yǔ)言——好用不好寫。 JML語(yǔ)言書寫的困難度過(guò)高（從課程組編寫JML出現(xiàn)的各種狀況可以看出），給我的感覺(jué)是“可遠(yuǎn)觀而不可褻玩”。而且，由于DDL過(guò)多加上學(xué)習(xí)資料不足（網(wǎng)上、課程資料都幾乎為零），我缺乏自己動(dòng)手寫JML的動(dòng)力。
• 沒(méi)有指引，路程變成了痛苦的過(guò)程。也許，是因?yàn)?strong>JML這一課還在探索階段，課程對(duì)JML編寫、檢測(cè)、使用的工具的講解和介紹頗少，基本全靠討論區(qū)和大佬們的指點(diǎn)，自己摸索著完成任務(wù)。固然，可以說(shuō)這是對(duì)我們自主學(xué)習(xí)能力的養(yǎng)成，但是，有必要嗎？我相信JML單元會(huì)一步步從碎片化走向體系化，更加容易上手。
• 在路上 ……

最后，衷心感謝為這門課程辛苦付出的老師和助教。???

轉(zhuǎn)載于:https://www.cnblogs.com/FUJI-Mount/p/10905195.html

總結(jié)

以上是生活随笔為你收集整理的OO_BLOG3_规格化设计（JML学习）的全部?jī)?nèi)容，希望文章能夠幫你解決所遇到的問(wèn)題。

如果覺(jué)得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。