面向物件設計與構造第三單元總結部落格

1 作業概述

第三單元作業的主要內容是根據給出的JML規格和介面定義實現一個社交系統，主要的功能包括社交關係的模擬與查詢、群組功能、不同型別訊息的接收與傳送等。

相較於前兩個單元，本單元的作業由於給出了JML規格，因此在設計上的難度相對較小，但如果只是將JML”翻譯“成程式碼也是無法高質量完成作業的。個人認為本單元需要重點關注的幾個點包括：確保實現的社交系統嚴格遵守給定的JML規格，合理的網路結構設計，使用時間複雜度較低的演算法等。

2 架構設計與圖模型

由於本單元作業需要嚴格遵守JML規格，因此在架構設計上並沒有特別多的發揮餘地，按要求在官方介面的基礎上實現MyNetwork,MyGroup,MyPerson

不難發現本單元作業的核心是構建一個無向圖模型，其中節點為人，邊為人與人之間的關係，群聊則可以看作是子圖，作業中絕大多數的操作都在在這個圖上進行。考慮到本單元作業對效能有一定的要求，因此在實現圖模型時大量使用了HashMap來進行儲存，從而提高查詢的效能，用空間換時間。

每次作業中，部分舊的設計可能難以滿足新的需求，因此在每次迭代開發中圖模型的構建與維護都有所變化。下面對每次作業中的圖模型設計進行解釋。需要注意的是，這一部分只討論基本的圖模型的構建，對於一些用於部分指令的設計將在下一部分中進行詳細的討論。

第一次作業

人：在MyNetwork類中用HashMap<Integer, Person>

關係：在MyPerson類中用HashMap<Person, Integer>來儲存，其中key是與該Person鄰接的其他Person，value是這兩個Person之間邊的權值。為了確保在對一個Person的邊進行查詢時不會漏掉某些邊，對於每一條邊，在其連線的兩個Person中都進行了相應的儲存；

群聊：在MyNetwork類中用HashMap<Integer, Group>來儲存，其中key是Group的id，每個群聊內，用HashSet<Person>存放該群聊內的全部Person。

第二次作業

人、群聊：與第一次作業相同；

關係：之前的設計難以滿足本次作業的需求，因此本次作業中新增了一個Edge類用來表示邊，在MyNetwork類中使用HashMap<Integer, ArrayList<Edge>>來儲存每個Person對應的邊，其中key是該Person的id，value是全部連線該Person的邊組成的ArrayList。對於同一條邊，依然在兩個Person中均進行儲存；

訊息：在MyNetwork類中用HashMap<Integer, Message>來儲存，其中key是Message的id。在MyPerson類中，用ArrayList<Message>來儲存該Person收到的訊息。

第三次作業

人、關係、群聊：與前兩次作業相同；

EmojiMessage：在NetWork類中使用HashMap<Integer, Integer>來儲存，其中key是該Emoji的id，value是其使用次數。

在圖模型的維護上，只需按照JML規定，對相應的容器增刪操作即可。

3 效能優化

本單元的作業對效能有一定要求，因此在部分功能的實現上需要選用合理的演算法與資料結構。由於用到的演算法都是圖論中的經典基礎演算法，個人認為沒必要給出演算法的具體細節，因此這裡重點解釋如何將演算法運用到作業當中。

並查集

對於第一次作業中的 query_circle 和 query_block_sum 兩條指令，如果直接用bfs或dfs暴力遍歷的話時間複雜度會達到 O(|V|+|E|)，效能較差，因此選擇使用並查集進行優化。qci指令用於判斷兩個 Person 是否聯通，qbs 指令求解連通塊的數量，對於這兩種情況我們其實並不需要知道連通塊中邊的細節，只需確定 Person 之間的連通性即可，因此我使用了路徑壓縮來進一步提升效能。

構建與維護

在MyNetwork類中，使用HashMap<Integer, Integer> root來儲存並查集的結果，其中 key 是 Person的 id，value 是該 Person 在並查集中的根節點。

當加入一個新的 Person 時，向 root 中加入其對應的新的元素，其中由於此時沒有連線該 Person 的邊，因此 key 和 value 均為該 Person 的 id。當加入新的關係時，按照並查集演算法進行路徑壓縮與合併。時間複雜度為 O(nα(n))。

query_circle

對於 qci 指令，考慮到同一連通塊內節點在並查集中的根節點一定相同，因此只需判斷兩個 Person 對應的根節點是否相同即可，可以用 O(1) 的複雜度完成查詢。

query_block_sum

對於 qbs 指令，考慮到並查集內的根節點與連通塊一一對應的關係，因此只需計算出並查集中的根節點數目即可。在我的實現中，由於第一次作業並沒有單獨儲存聯通塊，因此需要遍歷一遍所有節點，並記錄根節點是其自身的節點的數目，即為qbs的結果，可以用 O(n) 的複雜度完成查詢。

最小生成樹

在第二次作業中，query_least_connection 這一 JML 較為複雜的指令，實際含義是查詢某個 Person 所在的最小生成樹的邊權之和。在這裡，我選擇了在第一次作業實現的並查集的基礎上，通過 Kruskal 演算法來求解最小生成樹的邊權和。

構建與維護

考慮到對最小生成樹進行動態維護在實現上較為複雜且代價較高，因此我選擇了僅在查詢時計算最小生成樹。優點在於避免了複雜的動態維護，缺點是對同一顆最小生成樹的查詢每次都要重新計算。但考慮到查詢前後整個圖都有可能發生變化，因此個人認為綜合考量下在查詢時計算是更好的解決方案。

為了便於獲取最小生成樹的全部節點，第一次作業的基礎上再MyNetwork中新建了HashMap<Integer, HashSet<Integer>> connection，其中 key 是根節點，value 是該根節點全部子節點的集合，在增加節點和邊等操作時進行相應的維護。

query_least_connection

顯然最小生成樹內各個節點一定是聯通的，因此我們可以通過並查集首先獲得待查詢節點所在最小生成樹的全部節點：首先通過並查集查詢到待查詢節點的根節點，再通過新增的HashMap connection獲得最小生成樹的全部節點。

獲得全部節點後，再通過HashMap<Integer, ArrayList<Edge>>獲取這些節點的所有邊，並對這些邊按權值進行排序，時間複雜度為 O(|E|log|E|)。

接下來，對上述的節點和邊按照 Kruskal 演算法進行計算即可，其中判斷兩節點是否聯通時依然採用並查集來優化效能，該步驟時間複雜度為 O(|E|α(|V|))。總的時間複雜度為 O(|E|log|E|)。

最短路徑

在第三次作業中出現的 send_indirect_message 指令要求我們在兩個 Person 之間以最短路徑傳送訊息，並計算出最短路徑的長度。在具體實現上我選擇了經典的 Dijkstra 演算法。

構建與維護

為了便於 Dijkstra 演算法中起點到節點路徑值的記錄與比較，新建了一個 DijNode類，該類實現了 CompareTo 介面以便進行排序，同時提供路徑值的更新方法。

由於演算法過程中會不斷根據距離對未計算出最短路徑的節點進行排序，因此使用 TreeSet<DijNode> 來存放節點，保證了有序性。

send_indirect_message

與最小生成樹中的處理類似，首先通過並查集獲得起點所在的聯通塊內的所有節點，這些節點為最短路徑可能經過的全部節點，然後在這些節點上進行 Dijkstra演算法的計算即可。注意到我們只需求到固定終點的最短路徑，因此當算出終點的結果時即可退出演算法。

4 異常處理

本單元作業中我們需要實現一些具有計數功能的異常類，這些異常類在實現上非常類似，只是處理的具體異常不盡相同，因此我實現了一個 Counter 類來進行計數，每個異常類均將該類的一個例項作為一個 static 屬性，從而實現計數。

Counter 類中用一個 int 型別的屬性記錄對應異常出現的總次數，用一個 HashMap<Integer, Integer> 記錄某元素引起異常的次數，其中 key 是 id，value 是次數。

5 測試與Bug分析

測試

手動構造

對於連通塊、最小生成樹和最短路徑等作業中的難點問題，由於這些也是圖論中的經典問題，因此我採用的方法是到網上收集一些常見的易錯樣例進行測試。

對於異常類，構造一些異常資料來測試每個異常是否能正確觸發、輸出字串是否正確等。

對於是否符合 JML 規格，主要通過 JUnit 進行單元測試。同時通過閱讀指導書和 JML 來找出了一些細節問題，如群組人數最大為 1111，針對這些問題進行了重點測試。

自動測試

自動測試方面我只進行了大量資料的隨機生成，除了做到全部指令的覆蓋以外並沒有想到很好的構造思路。

Bug分析

三次公測中未出現Bug，第二次和第三次作業的互測中出現了 Bug，互測中沒有 hack 到別人。其中第三次作業的Bug是因為自己手滑，在 if 語句中少輸入了一個 ”！“導致的，沒什麼意義，就不在此記錄了。第二次作業的Bug則是由於效能原因，具體如下：

query_group_value_sum 指令導致的效能問題

這個指令本身其實並不難，但我在考慮效能問題時，只關注了三次作業中的難點（連通塊、最小生成樹、最短路徑），而在其他看起來比較“簡單”的指令的實現上並沒有進行效能的優化。對於 qgvs 這個指令，我直接在查詢時暴力遍歷，導致互測中超時。解決的方法也很簡單，只需要在 MyGroup 中使用一個屬性來記錄邊權和並在增刪 Person 以及增加關係時實時更新，查詢時直接返回其值即可。

6 心得體會

通過本單元，我初步掌握了 JML 規格的基礎知識，並在實驗課和討論課中掌握了一定的 JML 編寫能力。

這是我第一次在嚴格的規格限制下進行程式設計，相較於此前的完全自由發揮，在思維方式、程式設計習慣上等都是有所不同的。規格的存在讓我們可以更好地對自己的程式碼進行設計，幫助我們更加規範地完成任務。

但是，我們依然不能完全依賴於規格。規格只是告訴我們應該做什麼和不能做什麼，但沒有規定應該怎麼做。雖然直接把 JML “翻譯”到程式碼往往能解決大部分問題，但很多情況下這並不是最好的實現方式，我們應該多去思考如何在嚴格遵守 JML 的條件下更好地完成程式碼的編寫。

一個教訓是不能只關注難點而輕視其他內容，我本單元兩個互測中的 Bug 都是由於在實現一些簡單功能時掉以輕心且沒有進行充分測試導致的。

7 NetWork 擴充套件

擴充套件思路

Advertiser 、Producer 和 Customer 實現為 Person 的子類，Advertisement （廣告）和Purchase（購買訊息）實現為 Message 的子類，增加類 Product 表示商品，提供查詢 id 的方法 getId()。每個 Producer 內通過屬性存放其能夠生產的商品，並提供判斷能否生產某種商品的方法 慘Produce()。

JML 規格

完成了生產商品（produceGoods）、釋出廣告（publishAd）和購買商品（purchaseGoods）三個方法的 JML 規格:

public interface Network {
	/*@ 
	  @ public instance model non_null Goods[] goods;
	  @*/
    
    /*@ public normal_behavior
      @ requires contains(producerId) && (getPerson(producerId) instanceof Producer) && 
      @ 		 (getPerson(personId) instanceof Producer).canProduce(GoodsId);
      @ assignable goods;
      @ ensures goods.length == \old(goods.length) + 1;
      @ ensures (\forall int i; 0 <= i && i < \old(goods.length);
      @          (\exists int j; 0 <= j && j < goods.length; goods[j] == (\old(goods[i]))));
      @ ensures (\exists int i; 0 <= i && i < goods.length; goods[i].getId() == GoodsId);       @ also
      @ public exceptional_behavior
      @ signals (PersonIdNotFoundException e) !contains(personId);
      @ signals (NotProductException e) !(getPerson(personId) instanceof Producer);
      @ signals (CantProduceGoodsException e) !((getPerson(personId) instanceof Producer).canProduce(GoodsId));
      @*/
    public void produceGoods(int producerId, int goodsId) throws PersonIdNotFoundException, NotProducerException, CantProduceGoodsException;
    
    
    /*@ public normal_behavior
      @ requires containsMessage(adId) && getMessage(adId) instanceof Advertisement;
      @ assignable messages;
      @ assignable getMessage(adId).getPerson2().messages;
      @ ensures !containsMessage(adId) && messages.length == \old(messages.length) - 1 &&
      @         (\forall int i; 0 <= i && i < \old(messages.length) && \old(messages[i].getId()) != adId;
      @         (\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i]))));
      @ ensures (\forall int i; 0 <= i && i < \old(getMessage(adId).getPerson2().getMessages().size());
      @          \old(getMessage(adId)).getPerson2().getMessages().get(i+1) == \old(getMessage(adId).getPerson2().getMessages().get(i)));
      @ ensures \old(getMessage(adId)).getPerson2().getMessages().get(0).equals(\old(getMessage(adId)));
      @ ensures \old(getMessage(adId)).getPerson2().getMessages().size() == \old(getMessage(adId).getPerson2().getMessages().size()) + 1;
	  @ also
      @ public exceptional_behavior
      @ signals (MessageIdNotFoundException e) !containsMessage(adId);
      @ signals (NotAdException e) !(getMessage(adId) instanceof Advertisement);
      @ signals (PersonIdNotFoundException e) !contains(getMessage(adId).getPerson1().getId());
      @ signals (NotAdvertiserException e) !(getPerson(getMessage(adId).getPerson1().getId()) instanceof Advertiser);
      @*/
    public void publishAd(int adId) throws MessageIdNotFoundException, NotAdException, PersonIdNotFoundException, NotProducerException;
}

    /*@ public normal_behavior
      @ requires containsMessage(purchaseId) && getMessage(purchaseId) instanceof Purchase && contains(getMessage(adId).getPerson1().getId()) && getPerson(getMessage(adId).getPerson1().getId()) instanceof Customer && (\exists int i; 0 <=i && i < goods.length; goods[i].getId() == getMessage(purchaseId).getGoods().getId());
      @ assignable messages;
      @ assignable getMessage(purchaseId).getPerson1().money;
      @ assignable getMessage(purchaseId).getPerson2().messages, getMessage(purchaseId).getPerson2().money;
      @ 
      @ ensures !containsMessage(purchaseId) && messages.length == \old(messages.length) - 1 &&
      @         (\forall int i; 0 <= i && i < \old(messages.length) && \old(messages[i].getId()) != purchaseId;
      @         (\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i]))));
      @ ensures (\forall int i; 0 <= i && i < \old(getMessage(purchaseId).getPerson2().getMessages().size());
      @          \old(getMessage(purchaseId)).getPerson2().getMessages().get(i+1) == \old(getMessage(purchaseId).getPerson2().getMessages().get(i)));
      @ ensures \old(getMessage(purchaseId)).getPerson2().getMessages().get(0).equals(\old(getMessage(purchaseId)));
      @ ensures \old(getMessage(purchaseId)).getPerson2().getMessages().size() == \old(getMessage(purchaseId).getPerson2().getMessages().size()) + 1;
	  @ensures \old(getMessage(purchaseId)).getPerson1().getMoney() ==
      @         \old(getMessage(purchaseId).getPerson1().getMoney()) - ((Purchase)\old(getMessage(purchased))).getMoney();
      @ensures \old(getMessage(purchaseId)).getPerson2().getMoney() ==
      @         \old(getMessage(purchaseId).getPerson2().getMoney()) + ((Ppurchase)\old(getMessage(purchased))).getMoney());   
      @ also
      @ public exceptional_behavior
      @ signals (MessageIdNotFoundException e) !containsMessage(purchasedId);
      @ signals (NotPurchaseException e) !(getMessage(purchaseId) instanceof Purchase);
      @ signals (PersonIdNotFoundException e) !contains(getMessage(adId).getPerson1().getId());
      @ signals (NotCustomerException e) !(getPerson(getMessage(adId).getPerson1().getId()) instanceof Customer);
      @ signals (GoodsIdNotFoundException e) (\exists int i; 0 <=i && i < goods.length; goods[i].getId() == getMessage(purchaseId).getGoods().getId());
      @*/
    public void purchaseGoods(int purchaseId) throws MessageIdNotFoundException, NotPurchaseException, PersonIdNotFoundException, NotCustomerException, GoodsIdNotFoundException;
}