2022-OO-Unit3

mashiroly

1. 概述

又到輕鬆愉快的部落格周了（赫赫，hw13似乎不是很容易呢），回顧一下過去一個月做了什麼吧。
本單元的目標是學習基於規格的層次化設計，需求是在JML規格的指導下，實現一個模擬社交關係系統。作業重點是閱讀和理解JML規格，掌握異常處理和測試方法，體會設計和實現的分離。

2. 架構設計

2.1 圖結構

引入圖的劃分Partition，可將社交網路如下圖建模，基本囊括了所有關聯關係。

具體而言，自上而下的構建可分為以下幾步：

1. Network中維護三個集合。為方便查詢，使用HashMap<id, Class>。

2. 引入新類Relation

   （也就是Edge類），維護關聯的Person和value。

   在Network中維護id（自增），同樣將HashMap<id,Edge> EdgeSet作為屬性。

3. 引入新類Partition，表示以Person通過Relation關聯的連通子圖（劃分）。其儲存劃分內部的所有Vectex(Person)和Edge(Relation)，方便查詢。

   在Network中維護id（並查集更新根結點id），同樣將HashMap<id,Partition>PartitionSet作為屬性。

4. 根據JML規格撰寫三個類，對於集合能用HashMap<id, Class>盡用。注意Person

   的MessageSet需要維護佇列。

設計與實現分離初步體現於此，我們不需要如JML描述逐個遍歷，只要保證符合規格，可以選擇合適的資料結構。

2.2 維護策略

不涉及Partition的結構維護：

• 基本策略:由於大量使用HashMap，幾乎只需要使用put()進行新增操作 。有遍歷時刪除操作的Map可以使用執行緒安全的ConcurrentHashMap。Arraylist的刪除使用removeIf()。
• 不降複雜度的維護:部分指令複雜度無法優化到O(1)，且隨圖結構更新改變，如qrm, sim 。維護一個有效位。

三次作業經歷的最大“重構”應該是：為提高並查集+kruskal的效率，從hw9到hw10引入Partition

• 並查集:路徑壓縮。ar指令執行時合併劃分，更新劃分屬性，將劃分內所有Person新定義的ParentId屬性設為劃分內的某個id，這個id更新為Network中該劃分在Map中的key。
• 平均年齡、方差等Group屬性: Group自身維護ageSum, ageSquareSum，在atg, dfg時更新，時間複雜度能做到O(1)。

​ 公式$$D(X)=E^(X2)-E^2(X)$$計算方差，與JML描述精度不同。

​ 參考討論區帖子，有以下公式不丟失精度：$$D(X) = \frac{\Sigma X^2 -2\overline{X}}{n}+(\overline{X})^2$$

3. 效能問題和bug修復

3.1 hw9（悲

​ 週六下午，才測出未堆優化的Prim被鏈式資料+qci打穿了，臨時改寫不帶並查集的kruskal，結果完全寫錯。強測也寄的很慘。

​ 此次作業未引入並查集和劃分，qbs在ar時更新，複雜度O(1)。

3.2 hw10

​ 強測未發現bug。

​ 引入了並查集+kruskal，將qci複雜度優化到O(nlogE) 。

​ 但是qgav複雜度O(n^2)，被hack TLE了。之後將qgvs和qgav均優化到O(1)

3.3 hw11

​ 強測未發現bug。

​ sim使用堆優化的dijkstra，複雜度為O(nlogE)。

​ 互測也沒有被卡效能，但是dce規格理解有誤，以為是刪去所有EmojiMessage，被hack了。感謝僅10條指令讓我一眼看出bug的好哥哥！

4. 測試設計

1. Junit實踐

使用Junit編寫測試方法，個人的操作是通過完全遵守JML規格重新撰寫方法，用assertEquals()判斷方法實現是否符合不變式。龐大的測試類也需要維護一系列屬性（全域性變數），也需要面向物件，也需要封裝好各種修改圖結構的方法。

但實際編寫中，不可能完全照搬JML，例如sim,qlc等方法，規格上就有“尋找一個集合（子圖，鏈）”。隨著方法更加複雜，測試方法寫得越來越像實現的方法。hw10和hw11中，也因此被勸退，沒有繼續進行Junit編寫。

2. 隨機資料生成與對拍

最後還是採用python寫隨機資料生成器，並進行覆蓋性測試。為保證資料質量，生成器也要維護好Person、Group、Message集合（使用id），並從集合中取出id生成指令。為保障異常覆蓋率，我人為地設定隨機數按一定比例生成錯誤指令。同時手動構造邊界資料，如鏈式圖、完全圖、1111等。

這是10w條+5k人的資料，可以看到覆蓋率還是有保證的。未覆蓋的方法幾乎都是規格有定義、但實現上沒有使用的方法。

正確結果唯一就是好啊，不用寫正確性判斷，和小夥伴對拍就好了。（

5. Network拓展

假設出現了幾種不同的Person

• Advertiser：持續向外傳送產品廣告
• Producer：產品生產商，通過Advertiser來銷售產品
• Customer：消費者，會關注廣告並選擇和自己偏好匹配的產品來購買 -- 所謂購買，就是直接通過Advertiser給相應Producer發一個購買訊息
• Person：吃瓜群眾，不發廣告，不買東西，不賣東西

如此Network可以支援市場營銷，並能查詢某種商品的銷售額和銷售路徑等 請討論如何對Network擴充套件，給出相關介面方法，並選擇3個核心業務功能的介面方法撰寫JML規格（借鑑所總結的JML規格模式）

1. 新增Advertiser, Producer, Customer類繼承Person類；
2. 新增Product類；
3. 新增PurchaseMeassage，Advertisement類繼承Message類；

Network中應該新增方法：新增產品，傳送廣告，購買商品，查詢商品銷售額，查詢商品銷售路徑等。

public interface Network {
	/*@ public instance model non_null Produce[] produces;
	  @ ...
	  @*/
}

1. 新增產品addProducer

/*@ public normal_behavior 
  @ requires (\exists int i;0 <= i && i < people.length;people[i].getId() == id && people[i] instance of Procuder);
  @ requires !(\exists int i;0 <= i && i < produces.length;     	produces[i].equals(produce));
  @ assignable people;
  @ ensures produce.length == \old(produce.length) + 1;
  @ ensures (\forall int i; 0 <= i && i < \old(produces.length);
  @          (\exists int j; 0 <= j && j < produces.length; produces[j] == (\old(produces[i]))));
  @ ensures (\exists int i; 0 <= i && i < people.length; people[i] == person);
  @ also
  @ public exceptional_behavior
  @ signals (PersonIdNotFoundException e) (\forall int i; 0 <= i && i < people.length);
  @			people[i].getId() != id 
  @			|| (people[i].getId() == id && !(people[i] instance of Producer));
  @ public exceptional_behavior
  @ signals (EqualProduceIdException e) (\exists int i; 0 <= i 
  @ 		&& i < produces.length;produces[i].equals(person));
  @*/
public void addProduce(/*@ non_null @*/int id, Produce produce) 
    throws PersonIdNotFoundException, EqualProduceIdException;

2. 傳送廣告sendAdvertisement

/*@ public normal_behavior
  @ requires getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) &&
getMessage(id).getPerson1() != getMessage(id).getPerson2();
  @ requires containsMessage(id) && getMessage(id) instanceof Advertisement getMessage(id).getType() == 0 &&; 
  @ assignable messages;
  @ assignalbe getMessage(id).getPerson2().messages;
  @ ensures !containsMessage(id) && messages.length == \old(messages.length) - 1 &&(\forall int i; 0 <= i && i < \old(messages.length) && \old(messages[i].getId()) != id; (\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i]))));
  @ ensures (\forall int i; 0 <= i && i < \old(getMessage(id).getPerson2().getMessages().size());\old(getMessage(id)).getPerson2().getMessages().get(i+1) == \old(getMessage(id).getPerson2().getMessages().get(i)));
  @ also
  @ public exceptional_behavior
  @ requires containsMessage(id) && getMessage(id).getType() == 1 && getMessage(id) instanceof Advertisement
  @ requires getMessage(id).getGroup().hasPerson(getMessage(id).getPerson1());
  @ assignable people[*].messages
  @ ensures !containsMessage(id) && messages.length == \old(messages.length) - 1 && (\forall int i; 0 <= i && i < \old(messages.length) && \old(messages[i].getId()) != id;(\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i]))));
  @ ensures (\forall Person p; \old(getMessage(id)).getGroup().hasPerson(p);(\forall int i; 0 <= i && i < \old(p.getMessages().size());\old(p.getMessages().get(i+1) == \old(p.getMessages().get(i))));
  @ signals (MessageIdNotFoundException e) !containsMessage(id);
  @ signals (MessageIdNotFoundException e) containsMessage(id) && !(getMessage(id) instanceof Advertisement); 
  @ signals (RelationNotFoundException e) containsMessage(id) && getMessage(id) instanceof Advertisement && getMessage(id).getType() == 0 &&!(getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()));
  @ signals (PersonIdNotFoundException e) containsMessage(id) && getMessage(id) instanceof Advertisement && getMessage(id).getType() == 1 && !(getMessage(id).getGroup().hasPerson(getMessage(id).getPerson1()));
  @ */


public void sendAdvertisement(int id) throws MessageIdNotFoundException,PersonIdNotFoundException,RelationNotFoundException;

3. 查詢產品銷售額queryPrice

/*@ public normal_behavior 
  @ requires (\exists int i; 0 <= i && i < produces.length);produces[i].getId() == id);
  @ assignalbe none;
  @ ensures (\exists int i; 0 <= i && i < produces.length);produces[i].getId() == id && \result == produces[i].getPrice()); 
  @ public exceptional_behavior
  @ signals (ProduceIdNotFoundException e) !(\exists int i; 0 <= i && i < produces.length);produces[i].getId() == id);
  @ */

public void queryPrice(/*@ non_null @*/int id) throws ProduceIdNotFoundException