面向物件 第三單元總結

基於規格的測試策略

本單元的測試內容可以大致分成兩個部分：

• 首先是程式碼的正確性測試。由於本單元的主題是契約式程式設計，所以我們不需要擔心在程式碼架構上的問題；但是很可能出現對於jml理解上的錯誤，進而導致程式碼中的bug。這一部分的測試我起初採取了課程組推薦的 JUnit 來單獨測試每一個函式，但是發現實在是過於複雜，需要對每一個函式手動構造資料。因此，在後面的作業中我都採取了自動生成資料與同學對拍來發現問題。這一步一般只需要幾個資料點就能解決掉絕大部分的bug。
• 其次是程式碼的複雜度測試。本單元強測中有很多對於實現方法的複雜度的測試資料點，這一部分的測試通過演算法手動構造資料點即可，比如說對並查集和最短路的壓力測試。

架構設計

雖然說本單元已經給出了每個類的結構以及方法規格，但是留給我們自行設計的架構部分也有很多且十分關鍵，比如說容器的選擇與圖模型的構建與維護。

容器選擇

在容器選擇方面，我們可以用 ArrayList，HashMap，HashSet，LinkedList 等等多種容器。具體該怎麼選擇，應當對於問題與容器特點進行分別分析後再進行選擇。比如本單元中我大量使用的容器是 HashMap 而不是 ArrayList。這是因為我們常常需要通過id來索引某一個元素，若使用 ArrayList 則每次查詢都需要遍歷得到，時間複雜度為 O(n)。但是如果使用 HashMap 就可以在 O(1) 的複雜度內查詢到目標元素。而在圖相關的演算法中，我們常常會用到佇列，這時候就不能再使用 HashMap

圖模型的構建與維護

• 首先是第九次作業中的 qci 指令，查詢圖中兩點是否連通，我使用了路徑壓縮的並查集來降低複雜度。具體來說，在普通並查集的基礎上加入了路徑壓縮，將同一集合中所有結點的父節點都直接設定成根節點，這樣就避免了圖退化成一條鏈，進而導致超時的情況。

public int find(int curId) {
        int rootId = curId;
        while (roots.get(rootId) != rootId) {
            rootId = roots.get(rootId);
        }
        int fatherId;
        int tmpId = curId;
        while (tmpId != rootId) {
            fatherId = roots.get(tmpId);
            roots.replace(tmpId, rootId);
            tmpId = fatherId;
        }
        return rootId;
    }
 

• 然後是第十次作業中的 qlc 指令，實際上是查詢包含某結點的最小生成樹。通常最小生成樹有prim和kruskal兩種演算法，但是兩種方法的原版複雜度都會導致超時的情況。因此，基於上一次作業實現的並查集，並考慮到本題目中稀疏圖出現的概率是遠大於稠密圖的，我最終選擇了並查集和快排優化的kruskal演算法。

	/* 構建並查集 */
	for (int i: dsu.getRoots().keySet()) {
            if (dsu.find(dsu.getRoots().get(i)) == father) {
                dsuNew.getRoots().put(i, i);
                HashMap<Integer, Person> acq = ((MyPerson) getPerson(i)).getAcquaintance();
                for (int j: acq.keySet()) {
                    if (i > acq.get(j).getId()) {
                        continue;
                    }
                    left[cnt] = i;
                    right[cnt] = j;
                    length[cnt] = (Integer) ((MyPerson) getPerson(i)).getValue().get(j);
                    cnt++;
                }
            }
        }
       /* 快排 */
        Util.qSort(left, right, length, 0, cnt - 1);
        /* kruskal */
        for (int i = 0; i < cnt; i++) {
            int l = left[i];
            int r = right[i];
            int len = length[i];
            int leftFather = dsuNew.find(dsuNew.getRoots().get(l));
            int rightFather = dsuNew.find(dsuNew.getRoots().get(r));
            if (leftFather != rightFather) {
                res += len;
                dsuNew.getRoots().replace(leftFather, rightFather);
            }
        }

• 最後是第十一次作業中的 smi 指令，實際上是查詢兩個點之間的最短路徑。我選擇了堆優化的Dijkstra演算法，並且直接利用了java內建的 PriorityQueue 來儲存結點。由於最短路演算法本身比較簡單就不放在部落格上了。

程式碼效能及修復

由於有關容器和圖的時間複雜度問題為已在上一部分進行分析，故本部分我只列出三次作業中強測及互測中出現的問題。

• 第九次作業因為偷懶所以直接使用了bfs，雖然過了強測，卻在互測被hack爛了，所以不得再bug修復時進行大重構整體換成了並查集。事實證明偷懶不會有好果汁吃。
• 第十次作業本以為用了並查集優化的kruskal演算法就不會出什麼問題，卻沒想到在 qgvs 這個指令上掛掉了。我使用了樸素的兩重迴圈導致時間複雜度是 O(n^2)，同樣在互測時被hack慘了。這個對應的修復也比較複雜，需要動態維護一個 HashMap<Integer, Integer> groupValue ，需要在 addRelation，delRelation 等多個方法中進行對應的修改。

Network擴充套件

對於Network的擴充套件，我選擇 sendAdvertise，addProduct， querySale 三個方法來詳細展開：

/*@ public normal_behavior
  @ requires containsMessage(id);
  @ assignable messages;
  @ 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 int i; 0 <= i && i < people.length; person[i].likeType(\old(((Advertisement)getMessage(id))).getType) ==> 
  @         ((\forall int j; 0 <= j && j < \old(person[i].getMessages().size());
  @          person[i].getMessages().get(j+1) == \old(person[i].getMessages().get(j))) &&
  @         (person[i].getMessages().get(0).equals(\old(getMessage(id)))) &&
  @         (person[i].getMessages().size() == \old(person[i].getMessages().size()) + 1)));
  @ also
  @ public exceptional_behavior
  @ signals (MessageIdNotFoundException e) !containsMessage(id);
  @*/
public /*@ pure @*/ void sendAdvertise(int id) throws MessageIdNotFoundException;

/*
			@ public normal_behavior
      @ requires !(\exists int i; 0 <= i && i < products.length; products[i].equals(product));
      @ assignable products;
      @ ensures products.length == \old(products.length) + 1;
      @ ensures (\forall int i; 0 <= i && i < \old(products.length);
      @          (\exists int j; 0 <= j && j < products.length; products[j].equals(\old(products[i]))));
      @ ensures (\exists int i; 0 <= i && i < products.length; products[i].equals(product));
      @ also
      @ public exceptional_behavior
      @ signals (EqualProductIdException e) (\exists int i; 0 <= i && i < products.length;
      @                                     products[i].equals(product));
*/
public /*@ pure @*/ void addProduct(ProductInfo product) throws EqualProductIdException

/*@ public normal_behavior
  @ requires containsProduct(id);
  @ ensures \result == getProduct(id).getNum();
  @ also
  @ public exceptional_behavior
  @ signals (ProductIdNotFoundException e) !containsProduct(id);
  @*/
public /*@ pure @*/ int querySale(int id) throws ProductIdNotFoundException;

學習體會

本單元是我第一次正式接觸契約式程式設計的思想，在學習之後不得不感嘆JML語言的確可以嚴謹的給出函式和類的功能和執行要求。同時讓我想到了這學期的os實驗其實也與JML描述十分相似，我們可以通過函式上方的描述清楚地瞭解每個函式的作用是什麼以及在實現時應當注意什麼。但是我認為JML也有其弊端，其中最顯著的一個就是為了追求嚴謹的表達有時會過於抽象和冗雜。在完成作業時看到有些方法上面是數十行的JML時實在是令人頭痛不知該從何下筆。最後，雖然JML給出了我們程式碼的整體框架，卻沒有規定程式碼內部的實現邏輯。因此，我們必須認真考慮程式碼的時間複雜度甚至空間複雜度等屬性，以免在執行時出現不可預料的錯誤。