BUAA_OO_第三單元

1、JML初探

​ JML(Java Modeling Language)做爲一種形式化語言，能夠約束Java代碼中類和方法的狀態和行爲造成規格，經過將一系列具體代碼實現抽象成明確的行爲接口，能夠造成一種契約式編程模式，JML設計者無需考慮實際的數據結構與算法，能夠聚焦於程序的總體邏輯，JML形式化語言的無二義性能讓實現者準確理解接口功能，根據問題須要選擇合適的實現方式，同時JML能夠幫助實現者開展代碼測試與形式化驗證，固然這時就要分析出模型語言映射到具體代碼的抽象函數了。

JML表達式

​ JML能夠內嵌在.java內，很方便，以// @行註釋或/* @ ... @ */塊註釋，JML表達式支持Java表達式做爲基礎。針對更復雜的邏輯引入了量詞表達式，\forall關鍵字相似數學中的∀，用法爲\forall v; P(v); Q(v)，等價於∀v(P(v) → Q(v))；\exists關鍵字相似數學中的∃，用法爲\exists v; P(v); Q(v)，等價於∃v(P(v) ^ Q(v))；這是在本單元比較經常使用的，固然還有\max, \sum, \min等實用的關鍵字。

​ 還可使用特殊操做符==> <==>表示蘊含與等價關係，使用這種操做符能夠加強JML的可讀性，同時還有\nothing, \everything表示當前做用域下的空集全集

方法規格

​ 本單元咱們聚焦於JML中的方法規格，方法規格針對類中各類方法（構造、修改、查詢、生成）的返回值與行爲進行約束，方法規格的三大關鍵是前置條件、後置條件、反作用範圍。

​ 前置條件經過對參數施加約束，從而區分不一樣的處理操做，大致可分爲normal_behavior，expcetional_behavior，各有各的前置條件，從而經過JML能夠直觀看出什麼時候須要對異常輸入處理，什麼時候是正常輸入，固然兩者的條件不能有交集。若輸入均不知足前置條件，咱們在實現中是沒有理由進行處理的，所以方法的調用者爲了保證結果的可控必須瞭解前置條件。對於前置條件，使用requires P;要求輸入知足命題P

​ 後置條件對方法調用以後的對象狀態與返回值約束，規定方法行爲，使用關鍵字ensures規定後置條件，對於查詢(query)方法，特別是只關心返回值不改變數據的方法，能夠在訪問修飾符後加上/*@pure@*/ 標記，對於返回值(\result)的表示，通常使用ensures P(\result);

​ 固然可能在查詢中可能也會修改對象，好比惰式更新，修改方法(modify)也要修改對象，爲了表示出修改與其範圍，咱們須要調用前的狀態，ensures P針對的是調用後狀態，\old(obj)關鍵字就能夠看做對象/基本類型在方法調用前的快照。好比對於涉及容器的數據管理類，常用增刪Add, Remove方法，\old就派上用場了，可使用P(\old(obj)) ==> Q(obj)描述新的對象狀態，固然這對對象的新狀態是一種弱約束，好比不能保證Add後不會加入不指望的元素，能夠在另外一方向再加一個條件(constains(obj) && !isforadd(obj)) ==> \old(constains(obj))進行最小化，可見利用requires, ensures已經能夠基本描述方法了

​ 還有一個方面就是反作用範圍(side effect)了，咱們能夠列出本方法中可能修改的類中（靜態）屬性，對調用者而言，能夠輕鬆get到是否會修改本身關心的敏感屬性，一般使用assignable(modifiable)來列出可能修改的屬性表assignable v1, v2, ...;，也可使用JML中的全集，空集

​ 上面提到的expcetional_behavior是針對Java的異常特性的，使用signals關鍵字規範了異常的拋出時機與類型，用法爲signals (<Exception Class> e) P;，等價於當P == true時throw異常，本單元對程序魯棒性的考量也在此體現

類型規格

​ 類型規格就是對類中屬性數據的約束，相似Java，JML可在變量名前加修飾符，non_null保證容器內無null，聽從這個規約可有效避免訪問空引用，也有static, instance區分靜態屬性，固然JML想訪問類中private屬性時，相關屬性可加/*@spec_public@*/，但咱們的實現大可沒必要徹底按規格來，規格描述也不應關心具體實現中的數據（這一點是在實驗課中體會到的），本單元JML描述中容器都用數組表示，但咱們只要符合規格的約束條件，能夠選擇更合適的數據結構。本單元代碼中未涉及不變式invariant、狀態變化約束constraint，這兩個是比較強的約束條件，前者規定每次屬性修改後的規約，後者表示屬性修改相對於修改前狀態的規約

​ 總之JML對代碼實現者很實用，本單元寫代碼時官方JML已經給出了總體的結構與邏輯，JML中還有很多很實用的用法，值得往後深刻學習一哈

關鍵字	做用
\not_assigned(x,y,...)	變量是否在方法執行過程當中未被賦值
\not_modified(x,y,...)	變量在方法執行期間的取值是否未發生變化
\type(type)	返回類型type對應的類型
\typeof(expr)	返回expr對應的準確類型
\num_of	返回變量中知足相應條件的元素個數

2、JML之工具鏈

​ IDEA貌似沒有插件式的JML工具，仍是挺惋惜的，JML官網有相關工具的介紹

OpenJML

​ OpenJML可用於JML的語法檢查分析，下載解壓到項目文件夾下運行

java -jar openjml.jar -exec Solvers-windows\z3-4.7.1.exe -esc com\oocourse\spec3\exceptions\*.java com\oocourse\spec3\main\*.java

​ 發現提示int與#INT1不一樣啥的，是JML中三目運算符的解析好像有點問題，把Group接口中三目修改爲

/*@ ensures (\result == 0 && (people.length == 0) || (people.length != 0) && \result ==
      @          ((\sum int i; 0 <= i && i < people.length; people[i].getAge()) / people.length));
      @*/

JMLUnitNG

​ JMLUnitNG可基於JML對代碼實現自動生成測試代碼並開展測試，使用java -jar jmlunitng.jar 接口 源碼生成了測試代碼

​ 與同窗交流貌似須要在JDK 8環境下才能運行，在IDEA中Project Structrue -> Project Settings -> Project language level設置成8，運行一下針對Group接口的測試代碼

​ 可見JMLUnitNG是針對極端數據的，說好也是驗證了程序的基本功能，說壞數據覆蓋面並不廣，對本單元做業的幫助有限。

其餘

• JMLEclipse：針對Eclipse的JML插件
• JMLOK：介紹是說隨機數據對JML實現的測試
• AspectJML tool, JML4c：運行時規格驗證

3、架構與Java性能提高

​ 本次做業要求是對社交關係網絡的模擬，很顯然是一種圖論模型，Person接口做結點，Network做圖，Group做子圖，JML規格將層次描述的很清楚，強制Person管理邊集，層次按圖的層次就好，在hw9, 10我還專門引入了邊類MyFriend，主要考慮到可能迭代會出現Person的子接口。並且針對hw10的isCircle還保留了BFS和Disjoint Sets兩個版本的，主要考慮到最後可能會加入刪邊操做，並查集的刪邊操做至少也得是O(V + E)了，然而都並無,whatever,本單元這一點至關友好，筆者終於不用重構了

​ 選用數據結構方面，考慮到id範圍，類中容器所有選擇以id爲鍵值的Hashmap<>，固然用兩個Hashmap<>創建起結點輸入id到數組下標index的可逆函數 + 靜態數組也很不錯，爲了可維護性選了前者

​ 爲何要說"Java性能"

​ JML設計者只關心類可見的狀態，並不關心具體實現的類內部狀態，這也是同窗們發揮的空間，但那種直接對着規格照葫蘆畫瓢的代碼是很危險的，筆者仍然記得hw10用互測規模數據均可以把Group.getAgeVar樸素遍歷卡到1e9級複雜度(運行分鐘級)，震驚了。反正適合實際問題的方法纔是最好的！其次，Java還有c++這種面嚮對象語言，但凡涉及到字符串String，容器(container)之類的，抽象層次一高，就很難針對問題進行優化，致使執行效率低，反正很慢就是了，並且根據數據本單元T的還很多，因此提升性能很關鍵，這一部分圍繞幾個圖架構下的關鍵矛盾方法開扯

連通塊-isCircle & queryBlockSum

​ 前者查詢是否爲同一連通塊內，後者查詢連通塊數，最優解爲並查集(Union-find Sets)，具體原理老生常談了。isCircle()兩次find操做，同時在圖內維護連通塊數k，增長結點addPerson時k++，增長邊addRelation時進行merge操做，若爲不一樣連通塊合併,k--，在i條指令下複雜度爲O(E + i)

​ 固然hw10中的並查集有很大的隱患，遞歸形式的find操做在退化成單鏈的圖中遞歸層數爲V，筆者經過壓力測試發現四千多層就爆棧了，StackOverFlow由遞歸層數，JVM設置的棧大小以及函數參數，局部變量大小決定，筆者決定穩他一手，將find路徑上的結點暫存一下，找到父節點後統一設置父節點，就不遞歸了

​ 像開頭說的，並查集若是面對刪邊deleteRelation很棘手，因爲查並集路徑壓縮信息丟失，不能單純的改父節點，咱們須要遍歷點集找到涉及的兩個連通塊的點集，再遍歷一遍打上標記，刪邊，對於有標記的點展開BFS從新記錄下父節點,O(V) / O(V + E)，但若是deleteRelation有條數限制，那又是另外一種權衡了

記憶化-Group接口

​ Group用於查詢子圖信息，爲了提升效率維護內部屬性，反正一堆東西在addPerson / delPerson時更新就好，平均值維護年齡和suma，方差維護年齡平方和suma^2，套公式(suma^2 + mean^2 * size - 2 * size * suma) / size特別地，子圖內的增長邊(ar)能夠繞開Group，因此ar的時候得更新一下邊的數據，沒啥可操做的，但必須咱們對變量的維護這個優化要符合JML（好比hw11再維護int suma^2就溢出了，必定得保證正常狀況合法結果），對拍走起

點雙連通份量-queryStrongLinked

​ 通讀一下規格，查詢兩個結點是否在某個階數大於2的環路上，在討論區大手子指點下能夠解讀爲兩個結點是否在某個階數大於2的點雙連通份量上，學習了一下資料，點雙連通份量居然是tarjan？筆者只用過神奇的塔尖求過有向圖的強連通份量啊...而後其實把求有向圖的強連通份量的tarjan的DFS樹的出棧條件改一下就行了：遞歸遍歷子節點後再出棧改爲每一個子節點遞歸後出棧。上張簡單圖（數字是DFS順序，箭頭是DFS大概的方向）

​ 能夠看到咱們2次回溯到1，根據塔尖的遞歸更新，2, 3 / 4，5的low都會標記成1正好對應兩個份量，但在求強連通份量時要等到1無子節點時再出棧；改改代碼，每次回溯到根節點出棧就ok，固然注意不能出棧根節點，它能夠處在多個份量中，而且注意特判階數，O(V + E)

單源帶權最短路-queryMinPath

​ 經典帶權最短路，經典Dijkstra，堆優化後O(Vlog(V))

​ Java中想要搞一個小頂堆，PriorityQueue / TreeSet就夠用，二者分別基於靜態數組與紅黑樹，固然注意不能修改堆比較器中涉及的類屬性，這將破壞堆維護的性質並致使意料以外的Bug，只能冗餘加或先刪除再添加，PriorityQueue就不要先刪再加了，畢竟只能按引用查找遍歷到下標再刪，O(n)，紅黑樹的增刪都是O(log(n))

public boolean remove(Object o);
private int indexOf(Object o);

​ 爲啥筆者仍是TLE一個點，排查後原來是結點聯結邊集Hashmap<>(initalSize)初始化容量太大了，Hashmap迭代器遍歷的核心函數爲

final HashMap.Node<K, V> nextNode() {...
                if ((this.next = (this.current = e).next) == null && (t = HashMap.this.table) != null)
                    while(this.index < t.length && (this.next = t[this.index++]) == null);
...}

​ 可見要一次迭代器遍歷要遍歷哈希表到最後一個鍵值對，複雜度是容器的線性，因此說容量不能設太大，或者說這種無序型容器就不適合進行頻繁的遍歷操做，咱們能夠冗餘存儲一個順序容器。固然對於qmp, qsl這種頻繁訪邊點權的操做，創建起結點輸入id到數組下標index的可逆函數 + 靜態數組進行離散化就很香了，再把那個圖中的邊集直接一給MyNetwork管理，採用鏈式前向星，就純數組，繞太低效的容器和對象，甚至能夠搬本身的c代碼了，起飛

次序，區間查詢

​ queryAgeSum()單點更新，區間查詢，教科書的樹狀數組，queryNameRank在查詢次數遠大於節點數時能夠二分下界查找，本次做業應該不太實用

4、Bug們和修復

JUnit單元測試

​ 這是一個能夠快捷開展針對特定方法測試的框架，很實用，由於本單元咱們要抓住關鍵矛盾，測試複雜方法就行了，用@Before標記能夠在測試前初始化數據，用@Test開展一次測試，通常測一個函數就行了，Junit能夠把不一樣測試的stdout分開，關於測試方式，咱們每每要優化代碼，因此咱們能夠在測試類中模擬這些方法的樸素版，好比Group的，而後隨機構造數據，經過Junit的斷言Assertion機制來驗證一下優化版是否保證了正確性，固然能夠調用c來對拍，Junit內嵌於Java至關靈活，還能夠用於拋出異常的測試和運行時間的分析，是很是有用的Debug工具

自測 & 公測 Bugs

• 首先是以前說的優先隊列內元素不隨意修改，筆者居然沒注意到Java只能傳引用的特性；修復： 冗餘加入的時候clone()一下
• Group.getAgeVar沒注意到size == 0的狀況，divide by zero，hw10強測翻皮水
• 上文說了qmp在設置哈希表容量過大時不要迭代器遍歷，TLE一個點

5、規格設計心得體會

​ JML做爲一種形式化語言，表意很準確，我以爲結合接口API文檔使用也就更直觀了，本單元做業沒有涉及不變式跟繼承關係下的規格啥的。但其實主要讓筆者體會到了規格設計中的契約式編程方法，設計者和實現者分離，咱們在做業中扮演的實現者就是要在JML規格之下考量可維護性，執行效率，可讀性，採用最合適的。這是一種高效的開發模式，對咱們在團隊項目、工做中頗有用處