第三單元總結

一、自動化測試

​ 本單元推薦使用Junit 單元測試來對自己的程式進行測試，但事實上配置比較麻煩，而且跟著推薦的兩篇部落格配置時，也遇到了一點問題，第一篇部落格要求修改測試用例模板，將模板中生成的package的包名需去掉test，事實上我修改之後就出現錯誤，無法識別測試檔案，搞了好長時間，最後發現不修改反而可以識別測試檔案。

​ 在瞭解了Junit單元測試後，發現Junit單元測試並不能很好滿足我希望的本地測試要求，似乎難以對大量資料的答案的正確性進行檢測，加上相對於Junit自動化測試，我還是更熟悉傳統的對拍測試方法，考慮到效率等因素，我還是選擇了傳統的測試模式。

​ 第一單元的正確性檢查可以使用python庫，第二單元我利用了類似有限狀態機的方法。但是本單元的正確型檢查比較麻煩，我選擇了和小夥伴對拍。

​ 檢視JML規格可發現，對於生成的資料並沒有嚴格的顯示，如果資料不滿足要求的話總會觸發異常，而且觸發異常也是一種“正確性檢查”，所以這裡對測試資料沒有什麼限制。我們可以生成大量的隨機資料。

​ 生成資料方面完全隨機，在大量的資料投入下，雙方都發現了錯誤，主要還是漏看JML規則，或者是錯誤理解JML規則的問題。

​ 本單元強測互測均無bug。

二、架構設計——圖模型構建和維護策略

​ 本單元架構設計方面，主要還是根據JML規格完善方法。

​ 在圖模型構建方面，最主要的還是人之間的關係網路圖。關係的網路圖是帶權的無向圖，每個Person都儲存了自己相鄰的Person節點以及相應的權值。此外並沒有特殊構建圖模型。僅僅是在向社會網路中新增人和關係的時候維護相關量就可以了。

​ 本單元主要是JML的學習和一些圖演算法的瞭解，涉及最小生成樹演算法，最短路徑演算法以及並查集。同時為了不超時，需要儘量壓縮演算法複雜度，消除O(n^2)複雜的演算法，複雜度不超過O(nlog(n))。

​ 本單元作業中，queryBlockSum指令官方推薦並查集演算法。實際上我們只需在加人和加關係的時候，維護一下連通分量集和連通分量的數目就可以了，而且本單元的三次作業均不必再次擴充套件。可以做到O(1)的複雜度。

三、按照作業分析程式碼實現出現的效能問題和修復情況

• queryLeastConnection需要使用最小生成樹演算法，由於可能超時，需要加入堆優化，可以使用java現有的優先佇列。

• queryGroupValueSum可以在改變Group裡的人時，修改相關的ValueSum。

• queryGroupAgeVar可以在加人，刪人或者加關係的時候維護相關變數，在查詢時做到O（1）的複雜度；

​ 對於queryGroupAgeVar，有公式

\(\sum (\mathrm{age}_i - \overline{\mathrm{age}})^2 = \sum \mathrm{age}_i^2 - 2 * \overline{\mathrm{age}} \sum \mathrm{age}_i+ n * \overline{\mathrm{age}}^2\)

因此我們可以在每次加人或者加關係的時候維護\(\sum \mathrm{age}_i^2\), \(\sum \mathrm{age}\), 而且由於計算結果是取整的，因此這樣算在精度上不會出現錯誤。

• sendIndirectMessage指令涉及到最短路徑演算法，同樣為了避免超時，需要進行堆優化。

• 如果需要在集合中間刪減元素的話，可以使用LinkedList替代ArrayList，效率更高。

• 此外，比較容易忽視的一個點就是第三次作業中有關表情包資訊操作，注意的是這裡的一個EmojiId可能對應多個不同的Id(Message)。需要區別EmojiId和Id；

這些優化相當於將一個方法的複雜度平攤到眾多的方法裡面。

如果不進行相關查詢的話，速度可能會慢，但是進行大量的高複雜度的查詢命令的話，速度會大大提升。在課程組10000指令的規模下，相比未優化前，可以減少程式最大執行CPU時間，保證不超時。

（也許不進行一些優化也能過強測，但是很可能在互測遇見一些極其刁鑽的資料，導致超時。）

四、bug分析

主要是和小夥伴對拍的時候發現的錯誤

• 第一次沒有注意到EmojiId可能對應多個不同的Id(Message)。
• queryGroupAgeVar 沒有除人數，主要是漏看了JML，憑這個方法的名字主觀判斷了
• 細節問題，比如有的指令要刪資訊，但是一些相似的指令不需要刪，就導致了主觀性的錯誤。
• 沒有先判斷異常，導致出錯。
• 最多的問題就是在優化裡出錯了，在優化裡要格外注意，往往需要在多個方法裡對一個變數進行維護，比較分散，容易忽略，導致出錯。

五、對Network進行擴充套件，並給出相應的JML規格

設計的類如下：

新增的方法和部分JML規格

//public instance model non_null Product[] product;


/*@ public normal_behavior
  @ requires (\exists int i; 0 <= i && i < people.length;    
  @          people[i].getId() == id && people[i] instanceof Producer); 
  @ assignable product;
  @ assignable getProducer(id).product;
  @ ensures product.length == \old(product.length) + 1;
  @ ensures (\forall int i; 0 <= i && i < \old(product.length);
  @         (\exists int j; 0 <= j && j < product.length; product[j] ==   
  @         (\old(product[i]))));
  @ ensures (\exists int i; 0 <= i && i < product.length; product[i] ==   
  @		     product);
  @ ensures getProducer(id).product.length ==    
  @          \old(getProducer(id).product.length) + 1;
  @ ensures (\forall int i; 0 <= i && i < \old(getProducer(id).product.length);
  @         (\exists int j; 0 <= j && j <getProducer(id).product.length;   
  @       getProducer(id).product[j] == (\old(getProducer(id).product[i])));       
  @ ensures (\exists int i; 0 <= i && i < getProducer(id).product.length;   
  @          getProducer(id).product[i] == product);
  @ also
  @ public normal_behavior
  @ requires !(\exists int i; 0 <= i && i < people.length;    
  @          people[i].getId() == id && people[i] instanceof Producer); 
  @ assignable \nothing;
  @*/
public void createProduct(Product product,int id);

public void advertiseProduct(Product product,int producerId,int advertiserId);

public void watchingAdvertisements(int customerId);

public void buyProduct(int customerId,int productId);

/*
@public normal_behavior
@requires (exists int i;0 <=i && i<product.length ; 
@		   product[i].getid == id );
@ensures  (exists int i;0 <=i && i<product.length ; 
@		   product[i].getid == id && \result ==      	 
@          product[i].getSalesPath );
@also
@requires !(exists int i;0 <=i && i<product.length ; 
@		   product[i].getid == id );
@ensures \result == null;
*/
public String querySalePath(int id);

/*
@public normal_behavior
@requires (exists int i;0 <=i && i<product.length ; 
@		   product[i].getid == id );
@ensures  (exists int i;0 <=i && i<product.length ; 
@		   product[i].getid == id && \result ==      	 
@          product[i].getSalesVolume );
@also
@requires !(exists int i;0 <=i && i<product.length ; 
@		   product[i].getid == id );
@ensures \result == null;
*/
public int querySalesVolume(int id)

六、本單元學習體會

本單元主要學習了一些基礎的JML語法，並且複習了一些基礎的圖演算法。

但是閱讀JML的時候，對於眾多的（），{}，並不好掌握，我使用了VS Code準化為.v檔案進行閱讀，可以把匹配的（）和{}用不同的顏色標出來，便於閱讀，此外，對於每次作業的迭代，可以使用VS Code的檔案對比功能，找到需要進行擴增的點。

JML語言十分準確，保證了課程組傳遞給我們的資訊的準確性，但是一堆的\exists和\forall著實不容易閱讀，對於一個簡單的向一個容器中加一個元素，都要分四五句著實有點麻煩，可能程式的規格本身就不那麼容易地準確表達吧。