BUAA_2022面向物件_第三單元總結

O、寫在前面

正如助教所說，本單元的設計與執行，難度不大，這得益於JML的功勞；但是，對細心的要求尤其的高。如何理解、高效和全面的實現JML，是本單元的關鍵。在該單元中，我們完成了一個簡單聊天系統的實現，與其說實現，不如說是補全。關鍵架構，是將各個訊息收發者和群組的關係用圖的形式表現出來，從而能夠通過各種演算法進行多樣查詢操作。

一、架構設計

除常規實現以外（依據JML規格的完全對應實現），筆者主要針對qci,qbs,qlc,sim的效能進行了演算法優化。由於問題主體是圖論問題，因此我們可以單獨用一個類進行圖的建模與演算法應用，可以大大縮短查詢時間。

除此之外，還有一個細節，就是演算法選擇上，要朝著拓展性的方向，尋找與之前或者可能的之後實現的東西，具有較好契合性的演算法。例如下面的並查集和kruskal演算法就是很好的栗子。

1、qci與qbs——並查集的運用

並查集這個名稱的產生，是來源於並查集中的兩個主要步驟：合併、查詢。它的原理其實很簡單，即令每個結點記錄所在組。單憑這一句話，我們就能理解，為什麼並查集可以幾乎在$O(1)$複雜度內查詢兩個節點是否相連——只需要判斷其記錄的所屬組是否相等。

在具體實現中，需要建立一個一一對應關係的HashMap，來記錄節點與父節點即可。最初，所有節點的根節點均為自身id。每當建立了一條邊（兩節點建立聯絡），則按照儘可能減小樹高度的規則合併兩個節點所在樹。在進行查詢兩個節點是否在一棵樹上，只需要比較二者的根節點id即可。

但是利用並查集實現存在一個問題，那就是刪除問題，當我們想從圖中刪除一個結點，需要綜合考慮該節點聯結的多條關係。所幸，題目要求指令只會將該節點從group中移除，但並不會在整個Network中移除。想想實際情況也能理解這樣做的緣由，想必將一個人完全切斷與所有人的關係是不可能的吧，但是“退群”現象可是時常存在的。

2、qlc——最小生成樹的應用

該指令是求能夠連結某節點所在群組所有人能花費的最小queryValue和。對本問題顯然與最小生成樹問題契合，因此我在此選用較好理解且與並查集相得益彰的演算法，kruskal演算法。

kruskal演算法是一種典型的貪心演算法，我們稍微闡述一下其基本思想。既然我們想要得到最小的路徑權值和，那麼不妨先將所有的邊按照權值排序，然後依次從上往下查詢，如果加入該邊不會構成迴路，則加入到當前有效集合。最終得到的有效集合的邊集，即為最小生成樹的邊集，這對於我們的目的是一個極其直接的演算法。

具體實現時，最主要是能夠構造“邊”物件，並實現一個排序介面，這樣一來就能便捷地排序；除此之外還需要內部new一個並查集，用以查詢是否構成迴路。

3、sim——最短路徑的應用

該指令要求找到最短的傳送路徑，並返回最短路徑權值和。對於本演算法，我們採用dijkstra演算法。

從本質上來講，dijkstra演算法很好的利用了最短路徑的遞推特徵，即該路徑上任何一點到起點的路徑仍然是一條最短路徑。所以該演算法再求出目的節點的最短路徑的過程中，也順帶求出了起點到沿路各點的最短路徑，如果允許，還可以計算出到所有節點的最短路徑。

為了提升演算法效能，這裡採取了堆優化策略，所謂優化不過是優化了其中的排序過程。通過用優先佇列（排序規則套用已實現的“邊”排序介面）儲存新加入的邊，就能利用堆排序提升演算法效能到$nlog(n)$了。

二、自測體會與bug修復

1、有關自測

本單元著實意識到自測的重要性，其緣由與作業的架構有較大的關係。因為本單元的設計，架構尤其明顯，根據前面兩章的體會，架構越是清晰，程式碼量與層次就越複雜，可以理解為抽象性守恆。

因此有許多細小的bug也許藏在了很深很深的角落，不做大量測試是無法找出的。

本單元的自測，其實主要還是要依靠xh同學的評測機，在保證他的實現正確性的條件下（已經進行了大量對拍），我們可以通過大量黑盒測試找到問題，然後自己依據錯誤點，自行構造資料測試（因為測試資料數量實在多，不易debug）。

2、有關bug

本單元的bug其實沒有什麼好講的，如果必須要說的話，我只想說兩點。

首先，能用ArrayList或者HashMap一定不要用陣列。在並查集的實現，我是利用一個數組記錄節點與父節點的對映關係，但是由於陣列設定不夠大，最終造成陣列越界。只能說，非常可惜！

第二點是效能相關，除了利用演算法優化的那幾條指令，其中有一個qgvs指令著實讓人哭笑不得。最初實現，每次查詢都要遍歷所有人之間的queryValue然後相加，但是如果有人構造足夠多的人和足夠多的qgvs，就會造成超時......解決方案是構造“快取”，簡單來說就是拿個數記錄每一次的ValueSum。不得不說能找出這樣bug的人，腦洞還是很大的。

其餘bug基本都是按照JML照抄都能抄錯的地方，不過黑箱測試大概是這類bug的剋星吧。還是要感謝xh的評測機。

三、本單元體會

在經歷第一、二單元的折磨後，第三單元應對起來更加得心應手，可耐仍然存在大意失荊州。細節定成敗的真諦愈發明晰，與此同時，測試的重要性尤其凸顯。除了這些在技術上的警醒外，最大的收穫莫過於JML的學習了。

收穫了require,ensure等JML理解，領悟了契約化程式設計的思想，重要從一個人的程式設計上升到團隊、工程系統級別的程式設計。儘管依據JML寫程式碼是簡單的，但是如果組織一群人從0開始共同完成一個程式碼任務的初衷是可敬的。

四、三個核心方法的JML

總結而言，撰寫JML需要從：normal_behavior,require,assignable,also,exceptional_behavior,signals這些關鍵字，全面考慮所有情況。

/*@ public normal_behavior
      @ requires contains(personId) && getPerson(personId) instanceof Advertiser &&
      @          containsMessage(messageId) && getMessage(messageId) instanceof AdvertisementMessage;
      @ assignable people[*].messages;
      @ ensures (\forall int i; 0 <= i < people.length;
      @          \old(people[i].getMessages().size) + 1 == people[i].getMessages().size() &&
      @          (\forall int j; 0 <= j < \old(people[i].getMessages().size());
      @          \old(people[i].getMessages()).get(i) == people[i].getMessages().get(i+1)) &&
      @          people[i].getMessages().get(0).equals(getMessage(messageId)));
      @ also
      @ public exceptional_behavior
      @ signals (PersonIdNotFoundException e) !contains(personId) ||
      @          (contains(personId) && !(getPerson(personId) instanceof Advertiser));
      @ signals (ProductIdNotFoundException e) contains(personId) && getPerson(personId) instanceof Advertiser &&
      @          (!containsMessage(messageId) ||
      @          (containsMessage(messageId) && !(getMessage(messageId) instanceof AdvertisementMessage)));
      @*/
    public int sendAdvertisementMessage (int personId, int messageId)
            throws PersonIdNotFoundException, MessageIdNotFoundException;

/*@ public normal_behavior
      @ requires containsProductId(ProductId);
      @ ensures \result == getProduct(ProductId).getSalesAmount();
      @ also
      @ public exceptional_behavior
      @ signals (ProductIdNotFoundException e) !containsProduct(ProductId);
      @*/
public int queryProductSales(int ProductId) throws ProductIdNotFoundException;

 /*@ public normal_behavior
     @ requires !(\exists int i; 0 <= i && i < products.length; products[i].equals(product)) && (\exists int i; 0 <= i && i < preProducts.length; preProducts[i].equals(product))
     @ assignable products,producer.getProducts()
     @ ensures products.length == \old(products.length) + 1;
     @ ensures (\forall int i; 0 <= i && i < \old(products.length);
     @          (\exists int j; 0 <= j && j < products.length; products[j].equals(\old(products[i]))));
     @ ensures (\exists int i; 0 <= i && i < products.length; products[i].equals(product));
     @ ensures producer.getProducts().length == \old(producer.getProducts().length) + 1;
     @ ensures (\forall int i; 0 <= i && i < \old(producer.getProducts().length);
     @          (\exists int j; 0 <= j && j < producer.getProducts().length; producer.getProducts()[j].equals(\old(producer.getProducts()          @            [i]))));
     @ ensures (\exists int i; 0 <= i && i < producer.getProducts().length; producer.getProducts()[i].equals(product));
     @ also
     @ public exceptional_behavior
     @ signals (EqualProductException e) (\exists int i; 0 <= i && i < products.length;
     @                                     products[i].equals(product));
     @*/
public void addProduct（Product product,Producer producer）throw EqualProductException