JML規格及測試：

JML規格：

JML規格提供了一種對於資料的約束，通過更加形式化的語言來對於前置條件、後置條件進行約束，從而保證程式在正確執行後能得到正確的結果。

總體來說，JML規格相較於平時使用的自然語言來說更加複雜，這在作業中也有很明顯的體現，例如最短路、最小生成樹的描述，讓人看著感到不適。

但這樣也有效的避免了二義性的出現，同時也使得實現的過程中的邏輯更加清晰。

測試：

首先是介紹了一種新的測試手段JUnit。它需要你實現一個testcase子類，通過斷言的方式來進行驗證。

其次還是通過自己手寫評測機的方式，進行對拍。我在測試的過程中主要還是通過對拍的方式進行。

JML規格提供了對於資料的約束，通過這些約束，可以進行資料的構造，也可以進行評測機的編寫。

資料主要還是根據規格進行make，通過隨機資料進行全面覆蓋的測試，再通過構造corner case的方式進行邊界測試，最後對於時間複雜度進行測試以及優化。

架構設計：

這三次的作業是實現一個人際網路關係，主要有Network，Group，Person這幾個主要的類需要實現以及增量開發。

NetWork作為最頂層的類，內部包含了Group和Person。Group可以理解為群聊，訊息的發出可以是P2P也可以是P2G，通過不同訊息的類來實現。

除了JML規格需要實現正確性，還需要引入一些圖論演算法或者是預處理對於詢問進行加速。

例如並查集、kruskal實現最小生成樹、堆優化的dijkstra演算法等。

在增量開發的過程中，會遇到一個類的長度大於500行的問題，這就需要我們進行解耦，專門抽離出一部分內容單獨實現，我是通過新開了一個algorithm類，將所有需要使用的演算法放入其中。

具體實現如下：

最小生成樹：

public int mst(int id) {
        int rt = 0;
        int totalNode = 0;
        ArrayList<Edge> edges = new ArrayList<>();
        ArrayList<Person> people1 = new ArrayList<>();
        MyPerson fa 
 
= find(id);
        for (Person person : people) {
            if (!find(person.getId()).equals(fa)) {
                continue;
            }
            totalNode++;
            people1.add(person);
            ArrayList<Person> node = ((MyPerson) (person)).getAcquaintance();
            for (Person p : node) {
                if (find(p.getId()).equals(fa)) {
                    edges.add(new Edge(person.getId(), p.getId(), person.queryValue(p)));
                }
            }
        }
        for (Person person : people1) {
            ((MyPerson) (person)).setFa(person.getId());
        }
        edges.sort(Comparator.comparingInt(Edge::getValue));
        int totalEdge = 0;
        for (Edge edge : edges) {
            MyPerson fa1 = find(edge.getNode1());
            MyPerson fa2 = find(edge.getNode2());
            if (!fa1.equals(fa2)) {
                rt += edge.getValue();
                fa1.setFa(fa2.getId());
                totalEdge++;
            }
            if (totalEdge == totalNode - 1) {
                break;
            }
        }
        return rt;
    }

並查集：

    private MyPerson find(int id) {
        MyPerson temp = ((MyPerson)getPerson(id));
        if (id == temp.getFa()) {
            return temp;
        }
        int fa = temp.getFa();
        MyPerson person = find(fa);
        temp.setFa(person.getId());
        return person;
    }

dijkstra：

HashMap<Integer, Integer> ans = new HashMap<>();
                PriorityQueue<Node> pq = new PriorityQueue<>();
                pq.add(new Node(getMessage(id).getPerson1(), 0));
                ans.put(getMessage(id).getPerson1().getId(), 0);
                Person end = getMessage(id).getPerson2();
                while (!pq.isEmpty()) {
                    Node temp = pq.poll();
                    if (temp.getDis() != ans.get(temp.getPerson().getId())) {
                        continue;
                    }
                    if (temp.getPerson().equals(end)) {
                        break;
                    }
                    ArrayList<Person> person = ((MyPerson)temp.getPerson()).getAcquaintance();
                    ArrayList<Integer> val = ((MyPerson)temp.getPerson()).getValue();
                    int size = person.size();
                    for (int i = 0; i < size; i++) {
                        if (!ans.containsKey(person.get(i).getId()) ||
                                temp.getDis() + val.get(i) < ans.get(person.get(i).getId())) {
                            ans.put(person.get(i).getId(), temp.getDis() + val.get(i));
                            pq.add(new Node(person.get(i), temp.getDis() + val.get(i)));
                        }
                    }
                }

通過這樣的形式可以很大程度上使得network的實現更加清晰，閱讀程式碼和debug也相對更加輕鬆。

問題以及修復：

在作業中主要是遇到的效能問題，一部分原因是由於做本地測試的時候評測環境比較好，速度較快，從而忽略了一些寫法上的優化。

第一次作業因為QBS（Query Block Sum）操作的複雜度過高導致TLE，後面改成了在加入或者刪除一個人或者一條邊的時候，考慮對答案的改變。

第二次作業和第三次作業主要問題都是JML閱讀不仔細，第二次是QVS（Query Value Sum）想當然的認為一條邊的貢獻只算一次，導致答案只有正確答案的一半。

第三次作業是對於紅包訊息的傳送，是傳送到除自己以外的所有人，我傳送到了group內部包括自己的所有人，這導致QM的時候會出現錯誤。

但由於評測機是根據自己錯誤理解寫的，跟別人進行對拍的時候主要也是集中於需要演算法實現的幾個方法，因此導致最後錯誤了幾個點。

第三次作業由於dijkstra演算法寫的不是很好，雖然在本地能夠很好的完成，但在評測的時候出現了TLE的情況。

最後發現在最開始的時候初始化HashMap，就將HashMap填入了1000+個元素，導致取用的時候複雜度高。

後來改成了在取用的時候先判斷是否存在，不存在就應該為INF，然後修改之後再加入HashMap，這樣減少了HashMap取值的複雜度，在最終評測的時候能優化1倍以上的時間。

NetWork拓展：

Advertiser、Producer、Customer可以在Person的基礎上繼承。

Person吃瓜群眾不接受任何購買資訊，可以直接忽略。

Producer在生產了物品之後，將資訊傳送給Advertiser，Advertiser再將這些資訊傳送到需要的Customer。

對於Producer或者通過Advertiser的銷售額統計：

/*@public normal_behavior
    @requires contains(id) && getPerson(id) instanceof Producer;
    @ensures \result == getPerson(id).getTotalSales();
    @also
    @public exceptional_behavior
    @signals (PersonIdNotFoundException e) !contains(id);
    */
public int querySales(int id);

對於Advertiser傳送的廣告進行統計：

/*
 @ public normal_behavior
 @ requires (\exists int i; 0 <= i && i < people.length; people[i].getId() == id && people[i] instanceof Advertiser && 
            (\forall int j; 0 <= j && j < people.length; people[j].getId() == id && people[j] instanceof Customer && 
            (\forall int k; 0 <= k && k < people[j].ads.length; people[j].ads[k].getId() != people[i].getAdId()))) ;
 
 @ assignable people[*];
 @ ensures  (\exists int i; 0 <= i && i < people.length; people[i].getId() == id && people[i] instanceof Advertiser && 
            (\forall int j; 0 <= j && j < people.length; people[j].getId() == id && people[j] instanceof Customer && 
            (\exists int k; 0 <= k && k < people[j].ads.length; people[j].ads[k].getId() == people[i].getAdId()))) ;
 @ also
 @ public exceptional_behavior
 @ signals (PersonIdNotFoundException e) !(\exists int i; 0 <= i && i < people.length; people[i].getId() == id && people[i] instanceof Producer);
 @ also
 @ public exceptional_behavior
 @ signals (AdIdNotFoundException e) (\exists int i; 0 <= i && i < people.length; people[i].getId() == id && people[i] instanceof Advertiser && 
                                     (\forall int j; 0 <= j && j < people.length; people[j].getId() == id && people[j] instanceof Customer && 
                                     (\exists int k; 0 <= k && k < people[j].ads.length; people[j].ads[k].getId() == people[i].getAdId()))) ;
 */
 public sendAd(int id) throws PersonIdNotFoundException, AdIdNotFoundException;

Producer生產一個新產品：

    /*@ public normal_behavior
      @ requires contains(id1) && getPerson(id1) instanceof Producer && containsMessage(id2) 
　　　 @&& getMessage(id2) instanceof ProduceMessage && getPerson(id1) == getMessage(id2).getPerson1();
      @assignable messages;
      @assignable getMessage(id2).getPerson2().getProduct();
      @ensures !containsMessage(id2) && 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(id2).getPerson2().getProducts().size());
      @          \old(getMessage(id2)).getPerson2().getProducts().get(i+1) == \old(getMessage(id2).getPerson2().getProducts().get(i)));
      @ ensures \old(getMessage(id2)).getPerson2().getProducts().get(0) == \old(getMessage(id2));                         
      @ ensures \old(getMessage(id2)).getPerson2().getProducts().size() == \old(getMessage(id2).getPerson2().getProducts().size()) + 1;
      @also
      @public exceptional_behavior
      @ signals (MessageIdNotFoundException e) !containsMessage(id2);
      @signals (PersonIdNotFoundException e) !contains(id1);
      @*/
public void produce(int id1, int id2) throws MessageIdNotFoundException, PersonIdNotFoundException

心得體會：

總體來說這個單元的作業難度不高，根據JML規格就可以寫出對應的實現。

出現的最多的問題就是JML太多太雜，在閱讀中不仔細就會出現問題，導致強測、互測中失分。

還需要更加適應形式化語言的複雜與嚴謹