BUAA-OO-2022 Unit-3 部落格總結

本單元的目標為熟悉JML規格，任務是構建一個包含人、組、網路、訊息的社交網路。在維護過程中，我們需要通過某些演算法來進行優化以縮減查詢時間。抽象來講，人可以視為社交網路中的一個節點；一個組可以視為社交網路中的連通圖；而整張網路可以視為圖；人與人的關係便可以看做帶權邊，由此，我們將一個具體問題轉換成了一個圖論問題。

架構分析

圖模型構建

第一次作業

涉及的元素為人、組、網路；涉及的操作為新增關係（人與人、人與組），查詢聯通圖數量等。

第二次作業

新增元素訊息；有關訊息的操作包含新增、傳送等；同時考察群組部分屬性的查詢，涉及了最小生成樹。

第三次作業

在訊息元素中引入表情、提醒和紅包三個種類；新增涉及這三種種類訊息的操作以及訊息的間接傳送。

維護策略

在本單元中，涉及效能優化的主要有三點：在維護聯通圖數量時採用並查集演算法；在最小權值搜尋時採用 Dijskra 演算法；在針對屬性查詢的操作中採用以空間換時間的思想，實時維護變數簡化查詢。

路徑壓縮的並查集

前文提到，可以將組視為聯通圖，因此我們對於組數的查詢實際就是對聯通圖數量的查詢。而我們可以將每一個聯通圖視為一個集合，人作為結點就是集合中的元素，所以當我們可以為每個人附加一個集合的標識，在新增人與人的關係時就將這個標識統一成一個，這就是並查集的思想。而筆者在合併時同時採取了按秩合併與路徑壓縮。

堆優化的Dijskra 演算法

在最小生成樹中，筆者採取了堆優化的 Dijskra 演算法，如果未採用堆優化或者使用 DFS 存在較大超時風險。對於該問題，結點是人，而邊的權值便是關係中的Value。

以空間換時間

在對於屬性的查詢中，如果每次查詢再更新，時間複雜大較大。因此我們可以維護對應該屬性的變數，在關係更新的時候實時更新該變數，就可以以O(1)的時間複雜度進行查詢。

資料構造與測試

資料構造

資料構造主要採用隨機構造與針對構造的方式。隨機構造不言而喻，針對構造主要是依據 UML規格 中的細節以及效能進行。

測試

在本地測試時，筆者主要與夥伴採用多人對拍的形式進行。同時，建議在實現過程中獨立思考，以免同時和多個夥伴理解錯 JML規格

BUG 分析

自測

主要是通過大量隨機資料與夥伴對拍，同時共享各自認為 JML規格 中可能出現問題的點並進行測試。

強測

筆者三次強測未出現問題。

互測

筆者在第二次作業自測環節末發現了 qgvs 時間複雜度較高的問題，但出於穩妥起見，為避免引入更多 BUG 而沒有對該點進行優化，這導致了三次作業中唯一的 BUG。

而針對他人的測試主要是隨機資料的壓力測試，以及對組員上限、qgvs和並查集維護、Dijskra實現進行測試。

Network 拓展

需求

假設出現了幾種不同的Person

• Advertiser：持續向外傳送產品廣告

• Producer：產品生產商，通過Advertiser來銷售產品

• Customer：消費者，會關注廣告並選擇和自己偏好匹配的產品來購買 -- 所謂購買，就是直接通過Advertiser給相應Producer發一個購買訊息

• Person：吃瓜群眾，不發廣告，不買東西，不賣東西

/*@ public normal_behavior
@ requires contains(id1) && contains(id2) && getPerson(id1) instanceof Advertiser && getPerson(id2) instanceof Customer
     @ ensures (getPerson(id2).getAdvertisement.addAll((Advertiser) getPerson(id1).getAdvertisement))
     @ also
     @ public exceptional_behavior
     @ signals (PersonIdNotFoundException e) !contains(id1);
     @ signals (PersonIdNotFoundException e) contains(id1) && !contains(id2);
     @ signals (PersonTypeNotCorrectException e) contains(id1) && contains(id2) && !(getPerson(id1) instanceof Advertiser)
     @ signals (PersonTypeNotCorrectException e) contains(id1) && contains(id2) && getPerson(id1) instanceof Advertiser && !(getPerson(id2) instanceof Customer);
     @*/
   public void sendAdvertisement(int id1, int id2) throws PersonIdNotFoundException, PersonTypeNotCorrectException;
​
​
   /*@ public normal_behavior
    @ requires contains(id) && getPerson(id) instanceof Advertiser
    @ ensures \result == (\sum int i; 0 <= i && i < people.length; people[i] instanceof Customer &&
    @ \sum int j; 0 <= j && j < people[i].getPreference && people[i].getPreference[j].equals(id); 1
    @ also
    @ public exceptional_behavior
    @ signals (PersonIdNotFoundException e) !contains(id);
    @ signals (PersonTypeNotCorrectException e) contains(id) && !(getPerson(id) instanceof Advertiser)
    @*/
   public int querySalesValue(int id) throws PersonIdNotFoundException, PersonTypeNotCorrectException;
​
   /*@ public normal_behavior
    @ requires contains(id) && getPerson(id) instanceof Producer
    @ ensures \result == (\num_of int i; 0 <= i && i < people.length; people[i] instanceof Advertiser &&
    @                           (Advertiser) people[i].getProducer.equals((Producer) getPerson(id)));
    @ also
    @ public exceptional_behavior
    @ signals (PersonIdNotFoundException e) !contains(id);
    @ signals (PersonTypeNotCorrectException e) contains(id) && !(getPerson(id) instanceof Producer)
    @*/
   public List<Person> queryMarketChannel(int id) throws PersonIdNotFoundException, PersonTypeNotCorrectException;

心得體會

通過本單元，筆者對 JML 有了較為清晰的認識，但筆者認為本單元不應將同學過多的注意點引導至效能優化。

而關於如果書寫 JML ，筆者認為應當首要明確需求，然後梳理異常與正常的情況，最後給出不同情況下的處理。