2020北航OO第三單元總結

2020北航OO第三單元總結

本單元要求是根據JML規格完善代碼，初看是一個簡單的代碼照搬實現的東西，但最後才發現因爲CPU時間的限制，還考察了大量優化策略及數據結構中關於圖的知識，是一次很是注重細節構思的一單元，我藉此機會學習並鞏固了好幾個圖的算法，並瞭解了java各種容器的查插刪改的效率。

1、JML理論基礎

JML(Java Modeling Language)是用於對Java程序進行規格化設計的一種表示語言，它至關於一種接口，正確的JML能夠給實現人員清楚的代碼要求，而且針對已有代碼書寫JML也能夠提升代碼的可維護性、可讀性。經我使用看來，它有以下幾種關鍵要素組成：

1. 位於類一開始的//@annotation的屬性定義，它規定了類必含的屬性（固然也能夠由其它形式所展示），在以後的方法規格中會用到這些定義

2. 變式invariant，要求在全部可見狀態（凡是會修改爲員變量（包括靜態成員變量和非靜態成員變量）的方法執行期間，對象的狀態都不是可見狀態）下都必須知足的特性

3. 狀態變化約束constraint，對前序可見狀態和當前可見狀態的關係進行約束

4. pure關鍵詞，表示某些純粹訪問性的方法，即不會對對象的狀態進行任何改變，也不須要提供輸入參數，這樣的方法無需描述前置條件，也不會有任何反作用，且執行必定會正常結束

5. 前置條件(pre-condition)，用requires關鍵詞表示，定義調用者調用方法前必須知足的語句

6. 後置條件(post-condition)，用ensures關鍵詞來表示，定義調用者調用方法後必須知足的語句

7. 反作用約束子句，使用關鍵詞assignable或者modifiable，表示調用方法後能夠改變的變量

8. 異常處理行爲exceptional_behavior，用signals (Exception e) expr表示知足expr條件即拋出Exception異常，用signals only Exception表示知足前置條件即拋出Exception異常

其中，在規格表示時，大多數語句含義與代碼相似，只需注意一下幾個關鍵詞的意含義：

1. \nothing，指空集；everything，指全集，一般用在assinable語句

2. \result，表方法示返回結果

3. \old(expr)表達式，表示一個表達式expr在相應方法執行前的取值

4. 推理操做符：expr1==>expr2，即離散中的→

5. \forall表達式：全稱量詞修飾的表達式

6. \exists表達式：存在量詞修飾的表達式

7. \sum表達式：返回給定範圍內的表達式的和

2、JML應用工具鏈

1. OpenJML：相似於對代碼的檢查，能夠對規格進行語法的檢查

2. JMLUnitNG/JMLUnit： 針對類自動生成測試樣例並進行測試

3. JMLdoc : 相似 Javadoc，能夠快速生成 JML 文檔的相關文件

3、SMT Solver

下載了openjml，想要運行結果出現了一堆警告和error，相似於下面這種問題，\result都會被報錯，但本身寫的Demo裏只有很簡單的一個add方法，徹底摸不着頭腦，並且openjml也不能檢測forall、exsit等語句，只能放棄

public class Demo {
    //@ ensures \result = a + b
    int add(int a, int b) {
        return a + b;
   }
}

4、JMLUnitNG

通過一些奇奇怪怪的操做，我終於配置成功了jmluintng

我先對Person.java進行了測試，主要是先補齊new一個新對象時<>裏的變量類型，並加上包名，其它內容並無改動，能夠看出它產生的測試用例都是比較邊緣的狀況，如0、null、MAX_VALUE等，最後只貼出來出現fail的部分，集中在isLinked函數，緣由是輸入爲null的狀況，這應該是不會在使用中出現的一種狀況

以後我又進一步對Group.java進行了測試，結果以下

最後失敗的還是null的狀況。。。

我感受到，這實際上是一種很好地檢驗方法正確性工具，尤爲體如今它對邊緣狀況進行測試的方面，但可能不是很適合比較複雜的狀況（如咱們的圖算法）

5、架構設計

先放UML圖

看起來有點點複雜，但我在原有架構的基礎上，其實只增長了兩個類Edge和Bcc，一個表明圖中的邊，一個表明一個雙連通塊，經過增長這兩個類，能夠進行更好的雙連通份量與最短路徑的查詢。至於優化的問題，因爲都是在TLE以後才意識到須要進行優化，因此放在下部分講

5、bug及其修復

此次做業的bug主要出如今算法的問題上，因爲一開始都是機械地按照規格重現代碼，因此致使不少點TLE了，最後bug修復完的算法以下：

1. 採用hashmap進行存儲查找，arraylist太慢，並對hashmap進行適當的初始化容量操做（最後的TLE就死在這上面）

2. 對getValueSum和getRelationSum使用緩存機制，提早設置變量，在addRelation和addToGroup時進行即便修改

3. 對blockSum進行緩存，並對每一個person進行block的標號，在addPerson時使blockSum++，在addRelation時合併block，並改變blockSum（這裏在優化過程當中出現了一個bug，是由於沒有區分好block的標號及blockSum，使得後加進來的人也會被打上以前block的標號）

4. 經過每一個id的block號，可直接判斷isCircle

5. 對queryMinPath方法使用堆優化的Dijikstra，對於堆優化，採用了java有序隊列PriorityQueue來存儲，使Edge實現了Comparable的接口，而且每次添加的時候不用進行是否已經訪問過的查詢操做，由於他永遠都是poll出最小值。這裏也出過一個小bug，是因爲我將每一個id初始的路徑值設爲了1001（value[0,1000]），但忽視了value是一個累加的過程。。最後改成Integer.MAX_VALUE，也是因爲本身測試不充分的緣故，這其實只須要將每條邊的value值設大一點就能夠了

6. 因爲會有大量連續測最短路徑的操做，我每查詢一次就將查詢結果以<id, values>的形式儲存起來，若是有addRelation的改動就將相關節點刪去，這樣也能夠減小大量重複的dijisktra查詢操做（我的覺得qmp是此次的優化重點）

7. queryStrongLinked的Tarjan算法，這個就很少說了，由於你們應該都用了

最後MyNetWork的各個方法複雜度分析以下

MyNetwork.addGroup(Group)	2.0	1.0	2.0
MyNetwork.addPerson(Person)	2.0	1.0	2.0
MyNetwork.addRelation(int,int,int)	4.0	6.0	9.0
MyNetwork.addtoGroup(int,int)	4.0	2.0	5.0
MyNetwork.borrowFrom(int,int,int)	3.0	2.0	4.0
MyNetwork.compareAge(int,int)	2.0	2.0	3.0
MyNetwork.compareName(int,int)	2.0	2.0	3.0
MyNetwork.contains(int)	1.0	1.0	1.0
MyNetwork.delFromGroup(int,int)	4.0	1.0	4.0
MyNetwork.getGroup(int)	1.0	1.0	1.0
MyNetwork.getPerson(int)	2.0	1.0	2.0
MyNetwork.isCircle(int,int)	2.0	2.0	3.0
MyNetwork.MyNetwork()	1.0	1.0	1.0
MyNetwork.queryAcquaintanceSum(int)	2.0	1.0	2.0
MyNetwork.queryAgeSum(int,int)	1.0	3.0	4.0
MyNetwork.queryBlockSum()	1.0	1.0	1.0
MyNetwork.queryConflict(int,int)	2.0	2.0	3.0
MyNetwork.queryGroupAgeMean(int)	2.0	1.0	2.0
MyNetwork.queryGroupAgeVar(int)	2.0	1.0	2.0
MyNetwork.queryGroupConflictSum(int)	2.0	1.0	2.0
MyNetwork.queryGroupPeopleSum(int)	2.0	1.0	2.0
MyNetwork.queryGroupRelationSum(int)	2.0	1.0	2.0
MyNetwork.queryGroupSum()	1.0	1.0	1.0
MyNetwork.queryGroupValueSum(int)	2.0	1.0	2.0
MyNetwork.queryMinPath(int,int)	10.0	9.0	14.0
MyNetwork.queryMoney(int)	2.0	1.0	2.0
MyNetwork.queryNameRank(int)	2.0	2.0	4.0
MyNetwork.queryPeopleSum()	1.0	1.0	1.0
MyNetwork.queryStrongLinked(int,int)	5.0	7.0	10.0
MyNetwork.queryValue(int,int)	3.0	2.0	4.0
MyNetwork.renew(int,int)	2.0	7.0	7.0
MyNetwork.tarjan(int,int)	6.0	7.0	8.0

也能夠看出來是qmp和qsl方法複雜度比較高，也是隻有這兩個方法含有圖的反覆查詢操做

6、心得體會

坦白地講，在作第一次做業時，我用了oo有史以來的最短期，並且我的感受沒什麼須要測試的地方，不禁感嘆oo做業變簡單了，在進行互測時，也是第一次認真看完了全部人的代碼，並找出了他們的漏洞，感受第一次做業仍是比較注重規格的。

第二次做業，雖然形式與第一次相同，但忽然講究的多了起來，也開始對時間和算法有要求了，但因爲當週的os做業太難搞，我仍是放鬆了對oo的優化及測試，致使我出了一個很大的bug沒有進互測！！！真的沒有想到中測忽然變得如此簡單。。我是大大的失策了，再加上雙重循環的遍歷，掛掉了全部強測。

第三次做業，我吸取了前兩次的教訓，本身對算法和測試都比較認真地規劃了，並且我也能感覺到第三次做業十分看重算法，難度甚至大過了數據結構，此次的結果還算比較正常，也因爲優化程度不夠致使TLE了一些點，並且互測的大佬們也查出了我沒注意的很小的點，通過最艱難的一次bug修復，我終於完成了這一單元的代碼部分。

真的感觸頗多，從這一次做業，我充分認識到了JML規格的實現不是純」實現」的問題，要進行本身的優化， 使程序效率達到最好，想一想這實際上是合理的，規格的書寫者只負責想好方法的效果，保證規格正確性便可，不可能連咱們怎麼實現都考慮到了。最後，再讚一句助教此次強測的點簡直太妙了，就卡那一點點時間，我是掙扎着才由2.0XX秒到了1.9X秒，真是一次頗爲「愉悅」的經歷。。