第三單元部落格作業

一、自測過程

在自測之間，我一般會反覆閱讀自己的程式碼，靜態地看一下可能的問題。

• 在第一次作業的時候，嘗試使用了JUnit 來構造資料，但是發現構造的時候非常的麻煩，基本上是手動構造。
• 之後就開始使用對拍的方法來測試了……效果似乎還不錯。

二、本單元的架構設計

在本單元中，所謂架構主要是指如何儲存資訊，JML只是指出了一種抽象的概念框架，但是在實際上可以有不同的選擇，在不同的實際實現之間選擇最適合本單元測試的，這是一種權衡。

例如在一個NetWork中，需要去用id去索引 MyPerson，MyNetwork等元素。在JML提供的抽象概念中，使用了一個數組來表示這樣的概念，由於Id

描述這樣的鍵值對關係，一個更好的辦法是使用HashMap來進行處理，由於雜湊表的性質，查詢變得非常的快，並且可以提供比陣列更好的功能。

綜上所述，在本單元中，對於所有的需要索引來查詢的物件，都使用HashMap來儲存。

具體而言：

• MyNetwork中：

  • people 儲存該網路中的所有id => Person 鍵值對
  • groups 儲存該網路中的所有id => group 鍵值對
  • messages
    儲存該網路中的所有 id => Message 鍵值對
  • emojiHeat 儲存該網路中的 emojiId => emojiHeat 鍵值對

• MyPerson中：

  • edges 儲存該人與其他人的所有邊關係，仍然以鍵值對的方式儲存Integer => edges

在以上的大多數使用HashMap來儲存圖的架構中，還有一個例外：對於每個人收到的Message，由於我們在輸出的時候需要按照下標來輸出，因此必須真的順序儲存，所以使用了一個ArrayList<Message>來進行儲存。

在儲存之後，就是維護策略：

對於大多數“新增”的行為，可以使用HashMap

但有少數比較Trick的地方，比如在關於Group的getValueSum的時候，需要進行一些特殊的儲存，這些將在下一節中提到。

三、效能問題和修復情況

在本單元中，大多數查詢對效能的要求都不高，但是有一些是例外的。

3.1 group::getValueSum

這裡的問題是，如果像JML的描述一樣使用二重迴圈來掃描的話，理論的時間複雜度就會達到O(N^2)，即使強測沒有資料卡這個點，互測肯定會。

我的方法是，語氣讓少數指令的時間複雜度達到平方，不如讓所有指令的時間複雜度均攤為線性O(N).

實際上，對於每個Person而言，維護了一個雜湊表

private final HashMap<Integer, Integer> groupSum;

這個雜湊表的意義在於，建立一個從groupId，到“該Group中，所有與本人相連的邊的權重的總和”，在新增邊的時候，時間複雜度從O(1)變成了O(# Groups)，但是在執行求組內邊權重和的時候，只需要將組內所有的Person，在該Group下的groupSum.get(groupId)求和即可。

3.2 並查集

在本次作業中，需要判斷某些Person（以下等同於點）之間是否有邊相連，如果點在同一個聯通塊中就算做一個Block，並且還需要計算所有Block的數量。

這是一個圖上分組的問題，用並查集（再加上路徑優化）就很合適。

3.3 最小生成樹

在第二次作業中，queryLeastConnection需要求“在某個點所在的Block中的最小生成樹”，這裡執行一個Kruskal演算法就可以了。

3.4 Dijkstra演算法的堆優化

似乎在時間複雜度上，並不需要堆優化……

總之，在Dijkstra演算法中，每次需要尋找一個與當錢“求出了最短距離”的點集合中，距離最近的那一個點，這裡本身是用掃描進行的，但是可以通過使用一個堆來更快地確定這個最小值。

四、Network的擴充套件

我的想法是，Advertiser自己可以擁有一個廣告，然後還擁有一些目標人群，每次呼叫傳送方法，廣告者就把自己的廣告發送給目標人群。

Class Advertiser extends Person {
    
    // public instance model non_null AdMessage ad;
    // public instance model non_null Customer[] customers;

    /** 將某個人加入到廣告發送組中 */
    public void addPeson(Person p);
    
    /** 將自己的廣告發送給廣告發送組中的每個人*/
    public void sendAds();
}
/*
JML of function sendAds():
@ assignable customers[*].getmessages()
@ ensures customers.length == \old(customer.length)
@ ensures(\forall int i; 0 <= i && i < customers.length;customers[i].getmessages().size() == \old(customers[i].getmessages().size()) + 1))
@ ensures(\forall int i; 0 <= i && i < customers.length; 
	(\forall int j; 0 <= j && j < \old(customers[i].getmessages().size());
	\old(customers[i].getmessages().get(j)) == customers[i].getmessages().get(j+1)))
@ ensures(\forall int i; 0 <= i && i < customers.length; 
	customers[i].getmessages.get(0) == ad)
*/

對於生產商，它應該能夠動態地新增商品，還可以查詢商品的銷售額，對於銷售路徑，可以用一個Map來表示：即每個廣告商提供了多少銷售量。

Class Producer extends Person {
    
    private ArrayList<int> productId;
    private ArrayList<int> productSale;
    
    /** 生產商可以增加自己能生產的商品*/
    public void addProduct(int id);
    
    /** 生產商可以查詢某種商品的銷售額*/
    public void querySale(int id) throws noProductException;
    
    /** 生產商可以查詢某種商品的銷售路徑*/
    public Map<Advertiser, int> querySalePath(int);
    
    /** 生產商將自己接收到的最早一筆訂單進行處理，更新元資料*/
    public void processOrder();
}
/*
JML of function querySale

@ public normal_behavior
@ requires (\exists int i; 0 <= i && i < productId.size(); id == productId[i])
@ ensures (\exist int i; 0 <= i && i < productId.size(); id == productId[i] && \result == productSale[i])

@ also
@ public exceptional_behavior
@ requires (\forall int i; 0 <= i && i < productId.size(); id != productId[i])
@ signals noProductException;
*/

對於消費者，它應該能夠擁有自己的偏好，還可以選擇收到的廣告進行購買。

Class Customer extends Person {
    
    private ArrayList<int> perference;
    private OrderMessage order;
    
    /** 消費者的偏好是否和廣告匹配*/
    public void boolean(AdMessage);
    
    /** 消費者可以新增自己的偏好*/
    public void addPreference();
    
    /** 消費者選擇自己收到的廣告中，最新的一條符合自己偏好的廣告並進行購買*/
    public void buy() throws noAdvertisementException;
}

/*
JML of function buy()
@ public normal_behavior
@ assgiable messages
@ requires (\exists int i; 0 <= i && i < getmessages().size(); getmessages().get(i) instanceof AdMessage && preference.match(get.messages().get(i)))

@ ensures getmessages.size() == \old(getmessages.size()) - 1
@ ensures (\exist int i; 0 <= i && i < \old(getmessages.size());
	\old(getmessages.get(i) instanceof AdMessage) 
	&&
	preference.match(get.messages().get(i)))
	&&
	(\forall int j; 0 <= j && j < \old(getmessages.size()); (\old(getmessages.get(j)) instanceof AdMessage && preference.match(get.messages().get(j)))) ==> (i <= j))
	&&
	(\forall int j; 0 <= j && j < \old(getmessage.size()); (j != i) ==> (\exists int k; 0 <= k && k < getmessage.size(); getmessages.get(k) == \old(getmessages.get(j)))
	&& 
	(\forall int j; 0 <= j && j < getmessage.size(); getmessages.get(j) != getmessages.get(i))
	&&
	getmessages.get(i).producer.getmessages().size() == \old(getmessages.get(i).producer.getmessages().size() + 1
	&&
	(\forall int j; 0 <= j && j < \old(getmessages.get(i).producer.getmessages().size());
	\old(getmessages.get(i).producer.getmessages().get(i)) == getmessages.get(i).producer.getmessages().get(i+1))
	&&
	getmessages.get(i).producer.getmessages().get(0) == order
)


@ also
@ public exceptional_behavior
@ requires (\forall int i; 0 <= i && i < getmessages().size(); !(getmessages().get(i) instanceof AdMessage)))
@ signals noAdvertisementException;

*/

五、學習體會

一開始，我以為JML和普通的Docs是很像的，在學習之後發現，Docs是要簡潔很多，而JML可以形式化地給出函式和類的執行要求。

很多時候，在類似的情景，比如OS中看不清楚出題人的意圖的時候，真的很想在函式上看到類似於JML的文件，這也說明了（我的理解中）JML的好處：它提供了一個非常清晰的前件、後件的描述。

但是這也是一種權衡，在簡潔性和清晰度之間的選擇。例如，在最小生成樹的那個函式中，JML佔了數十行，僅僅是閱讀理解JML的意思就需要很久，但是普通的Docs卻可以直接描述出來。

我自己在課外瞭解中發現，JML的使用並不像想象中的廣泛，或許在實際的工業產品中，程式碼的各個變數、元件之間遠遠比現在的還要複雜，如果要想把所有的函式的效果全部用JML描寫的話，會帶來巨大的複雜性，這似乎就有點得不償失了。

總結起來：在本單元中，我們瞭解了這樣一種新的，可以執行規模化設計的語言，可以提高程式碼的邏輯嚴密性和可維護性。但在寫自己的程式的時候、或是工作中，什麼時候需要使用JML，還是值得三思。