一、利用JML規格構造測試資料

兼顧正常行為和異常行為

• 例如對於ar指令，exceptional_behavior是!contains(id1) || !contains(id2) || getPerson(id1).isLinked(getPerson(id2))
• 生成指令時把people_id的隨機數在總人數的基礎上增加50，"ar {} {} {}\n".format(id1, id2, randint(1, (people_num + 50)))，從而保證正常行為和異常行為都可以覆蓋到

根據Jml限制，設定邊界資料

• 比如group的人數上限1111，getReceivedMessage()的條數為4條
• qgav當people=0的時候需要丟擲異常，容易遺忘出現除0錯誤

高複雜度的指令測試是否超時

• queryGroupValueSum不限制條數，需要考慮動態維護的方式避免tle
• queryBlockSum和iscircle指令，如果沒有使用並查集使用dfs會超時

一條指令觸發多種異常時的行為

• 隨機資料不能保證把各種異常型別的組合完全覆蓋，需要手動構造特定異常的測試資料保證完備性。

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

hw9

PersonClass

• 維護一個集合groups：person所在的所有group

GroupClass

• 維護三個欄位

    private int ageSum;
    private int squareAgeSum;
    private int valueSum;
 

• atg()方法中維護上述四個欄位:

public void addPerson(Person person) {
    people.putIfAbsent(person.getId(), person);
    int tmp = person.getAge();

    ((PersonClass) person).addGroups(this);
    ageSum += tmp;
    squareAge += (tmp * tmp);

    people.forEach((k,v) -> valueSum += v.queryValue(person));
    //所有和新進組的person有關係的人和新進組人之間的value加進groupValueSum
}
 

• 並且對於valueSum欄位：在NetWork類的addRelation()方法也要維護：如果person1和person2在一個group，給此group加上兩倍的value。

        HashMap<Integer,GroupClass> g1 = sp1.getGroups();
        HashMap<Integer,GroupClass> g2 = sp2.getGroups();
        g1.forEach((k,v) -> { if (g2.containsKey(k)) { v.addValue(value); } });

• dfg()方法同理
• 需要注意在使用公式計算AgeVar時，關於整除的誤差.

    public int getAgeVar() {
        if (people.isEmpty()) {
            return 0;
        }
        long mean = age / (people.size());
        long tmp = squareAge - 2 * mean * age + (people.size()) * mean * mean;
        int ans = (int)(tmp / (people.size()));
        return (ans);
        //(squareAge / (people.size()) - 2 * mean * mean)為錯誤公式，會由於整除而產生誤差。
    }

NetworkClass

• 需要維護連通分支。採用並查集，維護連通分支的頂層父節點和最大連通分支數量，分別用於isCircle()和getBlockSum()。
• addPerson()時，需要在union中新建Person節點，自己為一個連通分支，最大連通分支數量++。
• addRelation()時，需要union.merge(person1,person2)，找到兩個人的頂層父節點。如果不同，合併兩個連通分支，更新節點的父節點，最大連通分支數量--。
• isCircle()時，找到兩個人的頂層父節點判斷是否相同即可

hw10

queryLeastConnection()指令，需要找節點所在連通分支的最小生成樹

• 處理策略是建一個SuperUnion類繼承並查集Union類,使用基於並查集的Kruskal最小生成樹演算法
• 演算法需要兩個新維護的欄位：每個頂層父節點的Id為key，維護好本連通分支的邊集blockEdgeMap和節點的數量blockPoints。

    private HashMap<Integer,ArrayList<MemEdge>> blockEdgeMap;
    private HashMap<Integer,Integer> blockPoints;

• addRelation()呼叫union.merge()時：
  • 找到對應父節點id的邊集，加入關係這條邊，邊的MemEdge類儲存兩個節點和邊權。
  • 如果發生兩個連通分支合併，需要把新的頂層父節點的邊集和點集都進行更新合併。
• 基於並查集的Kruskal最小生成樹演算法虛擬碼：

從NetWork維護的並查集裡取出people_id的所在的連通分量block；
為了判斷最小生成樹不成環，為這個block  new一個基礎並查集union；
取出block的 邊集&點的數量；
sort(邊集)

int nowEdges=0；//最小生成樹已加入的邊數 

for(邊集的每條邊）{
	
	if（id1節點沒有被加進過unionTmp）{
		unionTmp.addPoint(id1)
	}
	if（id2節點沒有被加進過unionTmp）{
		unionTmp.addPoint(id2)
	}
	id1的父親 = unionTmp.find(邊的id1)
	id2的父親 = unionTmp.find(邊的id2)

	if（id1的父親 == id2的父親）{
		//成環
		continue;
	} else {
		unionTmp.merge(id1,id2);
		ans += 這條邊的weight;
		nowEdges++;
	}

	if (nowEdges ==（ block點的總數-1) {
		break;
	}
}

return ans;

hw11

PersonClass

• 設定noticeDirty，如果未加入notice訊息，則clearNotices()時不需要遍歷，直接返回即可。

    public void clearNotices() {
        if (noticeDirty) {
            messages.removeIf(message -> message instanceof NoticeMessage);
            noticeDirty = false;
        }
    }

sendIndirectionMessage():堆優化的Dijkstra最短路

        HashMap<Integer, Integer> distance = new HashMap<>();
        //起點到各節點間的最短路
        HashSet<Integer> points = new HashSet<>();
        //找過的節點
        PriorityQueue<NodeMessage> pq = new PriorityQueue<>(Comparator.comparing(NodeMessage::getDis));
        //優先佇列實現堆優化
        pq.add(new NodeMessage(id1, 0));
        distance.put(id1, 0);
        //加入起點

        while (!pq.isEmpty()) {
            NodeMessage node = pq.poll();
            int nextId = node.getId();
            int thisDis = node.getDis();

            if (nextId == id2) {
                return node.getDis();
            }
            //最短路徑更新到終點後，退出即可，不需要遍歷全圖

            if (points.contains(nextId)) { continue; }
            //節點已經被計算出最短路徑，跳過
            points.add(nextId);
            //把未經過的節點標記為經過

            Set<Integer> set = ((PersonClass)(people.get(nextId))).getAcquaintance().keySet();
            //遍歷這個點的所有通路
            for (Integer next: set) {
                
                if (points.contains(next)) { continue; }
                //節點已經被計算出最短路徑，跳過

                int dis = thisDis;
                try {
                    dis += queryValue(next, nextId);
                } catch (Exception e) {
                    e.printStackTrace();
                }
                //沒有計算過這個點的最短路或這個點的最短路需要更新
                if ((!distance.containsKey(next)) || (distance.get(next) > dis)) {
                    distance.put(next,dis);
                    pq.offer(new NodeMessage(next,dis));
                }
            }
        }

三、效能問題和修復情況

3.1 效能

• queryBlockSum和iscircle指令，如果沒有使用並查集使用dfs會超時.
• queryGroupValueSum不限制條數，需要考慮動態維護的方式避免tle，在addToGroup()和addRelation()時動態維護。

3.2 規範

• jml閱讀的細節：group的人數上限1111，getReceivedMessage()的條數為4條
• 異常的處理順序：
  ```互測時被hack到一個點：由於EmojiIdNotFoundException, EqualPersonIdException兩個異常的條件並不是互斥的，所以EqualPersonIdException的判斷條件不應該使用else if，應該使用if。

    public void addMessage(Message message) throws EqualMessageIdException,EmojiIdNotFoundException, EqualPersonIdException {
        if (messages.containsKey(message.getId())) {
            throw new MyEqualMessageIdException(pid);
        }
        else if (message instanceof EmojiMessage) {
            if (!emojiHeat.containsKey(emojiId)) {
                throw new MyEmojiIdNotFoundException(emojiId);
            }
        }
        else if ((message.getType() == 0) && (message.getPerson1().equals(message.getPerson2()))) {
            throw new MyEqualPersonIdException(message.getPerson1().getId());
        }
        //....
    }

• 不能在遍歷時remove。可以使用ArrayList.removeIf()方法。或者使用hashmap的迭代器

    public int deleteColdEmoji(int limit) {
        Iterator<Map.Entry<Integer,Integer>> iter = emojiHeat.entrySet().iterator();
        while (iter.hasNext()) {
            Map.Entry<Integer,Integer> entry = iter.next();
            if ((entry.getValue()) < limit) {
                int emojiKey = (entry.getKey());
                iter.remove();
                for (Integer id:emojiMessages.get(emojiKey)) {
                    messages.remove(id);
                }
                emojiMessages.remove(emojiKey);
            }
        }
        return emojiHeat.size();
    }

四、Network的擴充套件與JML規格

Producer：產品生產商增加產品

    /*@ 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] == (\old(products[i]))));
      @ ensures (\exists int i; 0 <= i && i < products.length; products[i] == Product);
      @ also
      @ public exceptional_behavior
      @ signals (EqualProductIdException e) (\exists int i; 0 <= i && i < products.length;
      @                                     products[i].equals(Product));
      @*/
    public void addProduct(/*@ non_null @*/Product Product) throws EqualProductIdException;

NetWork: 特定Advertiser向所有存在聯絡的消費者傳送特定產品的廣告

    /*@ public normal_behavior
      @ requires containsProduct(productId) &&  contains(advertiserId)
      @ assignable people[*].advs;
      @ ensures ((\forall int i; 0 <= i && i < people.length && people[i] instanceof Customer && people[i].isLinked(getPerson(advertiserId))
      @          (people[i].advs.length == \old(people[i].advs.length) + 1) &&
      @          (\forall int j; 0 <= j && j < \old(people[i].advs.length);
      @           (\exists int k; 0 <= k && k < people[i].advs.length; people[i].advs[k].equals(\old(people[i].advs[j])))) &&
      @          (\exists int j; 0 <= j && j < people[i].advs.length; people[i].advs[j].product.equals(getProduct(productId)) &&
      @           people[i].advs[j].advtiser.equals(getPerson(advertiserId)));
      @ ensures (\forall int i; 0 <= i && i < people.length && (!(people[i] instanceof Customer) || !(people[i].isLinked(getPerson(advertiserId))));
      @          (\forall int j; 0 <= j && j < people[i].advs.length; people[i].advs[j].equals(\old(people[i].advs[j]))));
      @ also
      @ public exceptional_behavior
      @ signals (ProductIdNotFoundException e) !containsProduct(productId);
      @ signals (PersonIdNotFoundException e) containsProduct(productId) && 
      @          !(contains(advertiserId));
      @*/
    public void sendAdvs(int productId, int advertiserId) throws ProductIdNotFoundException, PersonIdNotFoundException;

Customer：消費者購買廣告中偏好匹配的產品來購買

    /*@ public normal_behavior
      @ requires contains(customerId)
      @ assignable people[*].advs, people[*].saledAdvs;
      @ ensures ((\forall int i; 0 <= i && i < getPerson(customerId).advs.length && getPerson(customerId).liked(getPerson(customerId).advs[i].product)
      @          (\forall int j; 0 <= j && j < people[getPerson(customerId).advs.advertiser].saledAdvs.length;
      @           (people[getPerson(customerId).advs.advertiser].saledAdvs[j].equals(getPerson(customerId).advs[i].product))) &&
      @          (\forall int j; 0 <= j && j < \old(people[getPerson(customerId).advs.advertiser].saledAdvs.length);
      @           (\exists int k; 0 <= k && k < people[getPerson(customerId).advs.advertiser].saledAdvs.length; 
      @             people[getPerson(customerId).advs.advertiser].saledAdvs[k].equals(\old(people[getPerson(customerId).advs.advertiser].saledAdvs[j]))));
      @ ensures getPerson(customerId).advs.length == 0;
      @ also
      @ public exceptional_behavior
      @ signals (PersonIdNotFoundException e) (contains(advertiserId));
      @*/
    public void buyLikedAdvs(int customerId) throws ProductIdNotFoundException, PersonIdNotFoundException;

五、學習體會

儘管jml在閱讀理解時並不如文字性的描述理解地快，在剛剛學習第三單元時覺得很繁瑣，尤其是在課上experiment時，經常由於jml的閱讀速度慢造成寫不完的情況。但是在進入第四單元的uml作業時，經過對比之後我非常明顯地發現了jml無與倫比的優勢：第三單元關於題目要求與實現的所有細節都可以通過jml獲取，而第四單元的文字性敘述卻帶來了相當多的理解上的混亂與困擾，需要不斷詢問助教獲取題目的細節。所以jml確實是一種非常高效明晰的編碼規範，可以規避很多不必要的理解偏差，所以儘管閱讀jml的能力需要花費一些時間來練習，但遵循jml規範來編碼是非常值得的。