BUAA_OO_2020_UNIT3

来源:https://www.cnblogs.com/iff0/archive/2020/05/22/12938544.html

一、JML初探 ​ 作為一種形式化語言,可以約束 代碼中類和方法的狀態和行為形成規格,通過將一系列具體代碼實現抽象成明確的行為介面,可以形成一種契約式編程模式, 設計者無需考慮實際的數據結構與演算法,可以聚焦於程式的整體邏輯, 形式化語言的無二義性能讓實現者準確理解介面功能,根據問題需要選擇合適的實現 ...


一、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_behaviorexpcetional_behavior,各有各的前置條件,從而通過JML可以直觀看出何時需要對異常輸入處理,何時是正常輸入,當然二者的條件不能有交集。若輸入均不滿足前置條件,我們在實現中是沒有理由進行處理的,因此方法的調用者為了保證結果的可控必須瞭解前置條件。對於前置條件,使用requires P;要求輸入滿足命題P

​ 後置條件對方法調用之後的對象狀態與返回值約束,規定方法行為,使用關鍵字ensures規定後置條件,對於查詢(query)方法,特別是只關心返回值不改變數據的方法,可以在訪問修飾符後加上/*@[email protected]*/ 標記,對於返回值(\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 == truethrow異常,本單元對程式魯棒性的考量也在此體現

類型規格

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

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

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

二、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 介面 源碼生成了測試代碼

img

​ 與同學交流貌似需要在JDK 8環境下才能運行,在IDEAProject Structrue -> Project Settings -> Project language level設置成8,運行一下針對Group介面的測試代碼

imgimg

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

其他

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

三、架構與Java性能提升

​ 本次作業要求是對社交關係網路的模擬,很顯然是一種圖論模型,Person介面作結點,Network作圖,Group作子圖,JML規格將層次描述的很清楚,強制Person管理邊集,層次按圖的層次就好,在hw9, 10我還專門引入了邊類MyFriend,主要考慮到可能迭代會出現Person的子介面。而且針對hw10isCircle還保留了BFSDisjoint 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,增加結點addPersonk++,增加邊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?筆者只用過神奇的塔尖求過有向圖的強連通分量啊...然後其實把求有向圖的強連通分量的tarjanDFS樹的出棧條件改一下就好了:遞歸遍歷子節點後再出棧改成每個子節點遞歸後出棧。上張簡單圖(數字是DFS順序,箭頭是DFS大概的方向)

img

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

img

單源帶權最短路-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在查詢次數遠大於節點數時可以二分下界查找,本次作業應該不太實用

四、Bug們和修複

JUnit單元測試

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

自測 & 公測 Bugs

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

五、規格設計心得體會

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


您的分享是我們最大的動力!

更多相關文章
  • 摘要 axios是一個基於promise的HTTP庫,可以用於瀏覽器中進行AJAX請求處理。在項目中,為了實現通用性,封裝了一個axios請求。 axios封裝 1、配置環境變數 // 根據不同環境變數選擇不同的介面伺服器功能變數名稱 export const BASE_URL = process.env. ...
  • 摘要 在開發項目中時常有點擊跳轉滾動到錨點的需求,最簡單的錨點定位就是給一個a標簽,a標簽的href = ‘#錨點’,然後給需要跳轉的錨點一個id = ‘錨點’。參考最簡單的錨點跳轉實現方式,在React中使用useRef來實現跳轉錨點的功能。 功能具體步驟 1、創建空的Ref import Rea ...
  • 目前市場上HTML、CSS 類別書籍,都是大同小異,在噹噹網、卓越網搜索一下很多推薦。今天總結:Javascript 的書籍推薦看老外寫的,國內很多 Javascript 書籍的作者對 Javascript 語言瞭解的都不是很透徹。 想成為一個高薪WEB前端程式員,這些書籍你要看 初級讀物 《Jav ...
  • 為了方便大家寫代碼,vue.js給大家提供了很多方便的修飾符,比如我們經常用到的取消冒泡,阻止預設事件等等~。 目錄 表單修飾符 事件修飾符 滑鼠按鍵修飾符 鍵值修飾符 v-bind修飾符(實在不知道叫啥名字) 表單修飾符 填寫表單,最常用的是什麼?input!v-model~而我們的修飾符正是為了 ...
  • 1、初始化:選中元素進行初始化;$('input').iCheck({ checkboxClass: 'icheckbox_flat-blue', //選擇框的風格。 radioClass: 'icheckbox_flat-blue', });具體顏色:Black — minimal.css //黑 ...
  • 說句心裡話,小編在從事碼農之前。就是乾金融的!而且還是三年“萬金油” 多金多油 金融行業工資高? 我們當初在金融行業做業務,常常會說這樣一句安慰話:三月不出單,一單頂半年。 可想而知,這個薪水是真的讓人眼紅,高薪程式員瞬間就黯淡了。 但我為什麼又轉行做程式員? 一:金融行業就是從去年315開始下滑了 ...
  • 前提: SpringBoot + Vue + ElementUI 實現後臺管理系統模板 -- 前端篇(一):搭建基本環境:https://www.cnblogs.com/l-y-h/p/12930895.html 一、定義公共組件頁面 簡單的頁面效果如下所示:(做的比較粗糙,大致理解頁面即可) 1、 ...
  • 轉載請註明出處:葡萄城官網,葡萄城為開發者提供專業的開發工具、解決方案和服務,賦能開發者。 原文出處:https://blog.bitsrc.io/what-is-deno-and-will-it-replace-nodejs-a13aa1734a74 Deno是什麼? Deno v1.0.0已於5 ...
一周排行
  • 上一篇(https://www.cnblogs.com/meowv/p/12974439.html)完成了全網各大平臺的熱點新聞數據的抓取,本篇繼續圍繞抓取完成後的操作做一個提醒。當每次抓取完數據後,自動發送郵件進行提醒。 在開始正題之前還是先玩一玩之前的說到卻沒有用到的一個庫PuppeteerSh ...
  • 搞學習 猿學:http://yuanxue365.com/簡書:https://www.jianshu.com/doyoudo:http://www.doyoudo.com/好知網:http://www.howzhi.com/學小易(大學生搜題)https://www.51xuexiaoyi.com ...
  • LINQ 的優勢並不是提供了什麼新功能,而是讓我們能夠用更新、更簡單、更優雅的方法來實現原有的功能。不過通常來講,這類功能所帶來的就是對性能上的影響——LINQ 也不例外。本篇文章的主要目的就是讓你瞭解 LINQ 查詢對性能的影響。我們將介紹最基本的 LINQ 性能分析方法,並提供一些數據。還會給出 ...
  • Elasticsearch 入門(三)使用Elasticsearch.Net & NEST作為elasticsearch客戶端 GitHub倉庫 https://github.com/elastic/elasticsearch-net 選擇 Elasticsearch.Net 作為客戶端 連接方式 ...
  • 1.我們要知道為啥用框架? 代碼可讀性提高,加快開發速度,提高代碼穩定性,重覆代碼的封裝。 2.用框架有啥好處 結構清晰,調用方便,能低代碼開發。 3.怎麼用框架 根據邏輯邏輯與功能現實,把不同分類的東西,按照一定的規則,區分好模塊,一個令你滿意的框架就出來了 註意點: 技術薄弱的學員,不要著急學框 ...
  • 今天在學習winform項目時,看到同時是這樣解決text文本框變換值的: winform界面是這樣的 於是我在想,為什麼不直接進行賦值來進行變換,而通過替換局部字元串來變換呢?兩者之間有什麼區別?到底哪一種的性能會好點?於是帶著種種疑問,設計瞭如下實驗: using System; using S ...
  • HttpClient 中 FormUrlEncodeContent 的 bug ...
  • static void FileStreamSDemo() { DateTime dtNow = DateTime.Now; DateTime dtEnd = dtNow.AddSeconds(60); using(FileStream fs=new FileStream("FileStream.t ...
  • 用戶許可權驗證源碼剖析,和用戶登錄驗證有點相似,但是為了增加記憶,有必要再一次添加, 註意:一定要跟著博主的解說再看代碼的中文註釋及其下麵的一行代碼!!! 1、準備一個路由和視圖類,全局路由配置暫時忽略,當流程執行到下麵的url:groupsSelectAll——> GroupsView的視圖類下的a ...
  • 作者:勿念先生 https://blog.csdn.net/moHedong/java/article/details/79687878 GC的歷史比Java還有久遠,我們在思考GC時候需要思考三個問題: 哪些記憶體需要回收? 什麼時候回收? 如何回收? 在Java中程式計數器、虛擬機棧、本地方法棧這 ...