前言

本單元的程式碼任務集中在了學習JML的使用，並根據所給JML實現相應的方法和類。

契約式程式設計、防禦式程式設計與進攻式程式設計

契約式程式設計

契約式程式設計要求我們在「前提條件」、「後繼條件」和「不變數條件」進行契約的檢查。類似的，例如檢查引數，一旦引數不對，當即撕毀契約。

比如後端的方法因為傳入的引數不在設計範圍內而導致錯誤，這時就可以去找前端呼叫方，要求前端按照前置的設計來進行呼叫。

約束物件：呼叫者與被呼叫者

防禦式程式設計

“人類都是不安全、不值得信任的，所有的人，都會犯錯誤。”而你寫的程式碼，應該考慮到所有可能發生的錯誤，讓你的程式不會因為他人的錯誤而發生錯誤。

思路1：執行前檢查引數是否合規，不合規則報錯

思路2：對不合規的引數提供預設值

約束物件：被呼叫者

進攻式程式設計

認為是防禦式程式設計的分支，不同的是，進攻式程式設計讓錯誤明顯地存在。

進攻式程式設計針對的兩種錯誤：

可預期錯誤（Expectable errors）

1. 無效的使用者輸入（顧客走進酒吧要了一杯null）

2. 記憶體耗盡（陣列用完了）

3. 硬體出故障（突然斷網）

可預防錯誤（Preventable errors）

1. 函式引數不合法（傳進來一個null引數）

2. 值超出預定範圍（比如爆int）

3. 返回值異常（比如返回值不在switch的case中）

體現進攻式程式設計的操作：

1. 把陣列的大小開得剛剛好

2. 不初始化陣列，或者初始化成非0的值

3. 對所有可能錯誤的引數都進行檢查，出現異常直接throw

4. 不對不合規的引數提供預設值，而是直接報錯（區別於防禦式程式設計）

圖模型構建與維護策略

圖模型的構建

由於JML的規格已經給定，其實自行發揮的空間是比較小的。觀察別人的程式碼後，發現有人維護了JML規格以外的類去處理一些功能。但由於實際上，

由於每次架構都是迭代的增量開發，三次作業當中並未重構，因此，這裡直接展示第三次作業後的類圖：

理解java對於類的引用的原理，會發現其所有的引用使用的都是指標，因此，在傳送訊息這一功能的實現當中，遞迴下降地呼叫子類的子函式，和在Network中處理，效能上是差不多的。

由於編碼簡單，筆者在類似的問題中都選擇了在MyNetwork

效能問題和修復情況

效能優化策略

儲存中間變數

例如，求取Group中Person年齡的平均值，一般的做法如下：

    @Override
    public int getAgeMean() {
        int sum = 0;
        for (Person p : people) {
            sum += p.getAge();
        }
        return people.size() == 0 ? 0 : (sum / people.size());
    }

雖然取年齡的平均值並不是一個複雜度很高的指令，但這裡面其實是有優化空間的，比如小組中人的年齡的平方和是可以提前存好的，最終的的複雜度可以簡化成：

    @Override
    public int getAgeMean() {
        return (totalAgeSquare - 2 * mean * totalAge + mean * mean * people.size()) / people.size();
    }

無底線地使用HashMap

觀察所有待實現的方法，將所有本為陣列的元素都轉變為一個或多個“從檢索到被檢索元素”的HashMap，會讓後續的遍歷、篩選、檢索變得易於實現，且效能良好。

如我在Network類中，按照以下的方式實現了所需的幾個屬性。

    /*@ public instance model non_null Person[] people;
      @ public instance model non_null Group[] groups;
      @ public instance model non_null Message[] messages;
      @ public instance model non_null int[] emojiIdList;
      @ public instance model non_null int[] emojiHeatList;
      @*/
    private HashMap<Integer, Person> id2person = new HashMap<>();
    private HashMap<Person, Integer> person2id = new HashMap<>();
    private HashMap<Integer, Group> id2group = new HashMap<>();
    private HashMap<Integer, Message> id2message = new HashMap<>();
    private HashMap<Integer, Integer> emojiId2heat = new HashMap<>();
    private HashMap<Integer, HashSet<Integer>> emojiId2messages = new HashMap<>();

於是乎，所有的查詢操作都可以通過O(1)的方法完成，示例如下：

    @Override
    public Message getMessage(int id) {
        return id2message.get(id);
    }

但是這也就意味著，迭代的時候，增刪元素務必記住要處理所有hashmap的增刪。這一點非常容易出錯，這個在下文的bug修復中有提到。

演算法的優化

這一點在第一次作業方法queryBlockSum的實現中體現的最為明顯。其本質是一個判斷連通圖個數的問題。如果使用深搜的演算法，複雜度就會過高；最佳策略應該是使用並查集的演算法。

bug修復

第一次作業

無，比較順利。

第二次作業

BUG1：qgav的計算方式出錯

JML格式是這樣給出的

    /*@ ensures \result == (people.length == 0? 0 : ((\sum int i; 0 <= i && i < people.length; 
      @          (people[i].getAge() - getAgeMean()) * (people[i].getAge() - getAgeMean())) / 
      @           people.length));
      @*/
    public /*@ pure @*/ int getAgeVar();

由於java中int型別的整除問題，所以是先加還是先除會是一個影響結果的問題。寫的時候看錯了括號的範圍而誤寫成了先加再除。

BUG2：delPerson未處理用於處理新增指令的HashMap

在MyGroup中，為新增的指令建立了一個專用的HashMap<Integer, MyPerson>，用來直接找到發紅包的人。但是在為Group刪除人的時候忘記處理這個HashMap導致出錯。

第三次作業

BUG1：對Dijkstra的理解出錯

不細說了，就搞錯知識點了。

BUG2：遍歷刪除出錯

老生常談的bug，即以下的寫法是錯誤的

for(Object o : list){
    if(dosomething(o)){
        list.remove(o);
    }
}

嚴格使用ArrayList的下標進行遍歷，或使用removeif語句可以避免這個問題。

Network拓展

要求分析

假設出現了幾種不同的Person

1. Advertiser：持續向外傳送產品廣告

2. Producer：產品生產商，通過Advertiser來銷售產品

3. Customer：消費者，會關注廣告並選擇和自己偏好匹配的產品來購買 -- 所謂購買，就是直接通過Advertiser給相應Producer發一個購買訊息

4. Person：吃瓜群眾，不發廣告，不買東西，不賣東西

分析可知最主要的三個業務為：偏好設定、廣告發送、商品購買。

實現程式碼

偏好設定

    /*@ public normal_behavior
      @ requires contains(personId);
      @ requires getPerson(personId) instanceof Customer;
      @ assignable getPerson(personId);
      @ requires containsProduct(productId);
      @ ensures getPerson(personId).isFavorable(productId) == true;
      @ also
      @ public normal_behavior
      @ requires contains(personId);
      @ requires !(getPerson(personId) instanceof Customer);
      @ assignable \nothing;
      */
    public /*@ pure @*/void setPreference(int personId, int productId);

考慮到可能重複設定偏好，應該也可以被包容為一個正確的操作，因此，前置條件不需要要求此前該Customer對這一商品出於非偏好的狀態。

廣告發送

    /*@ public normal_behavior
      @ requires containsAdvertisement(id);
      @ assignable advertisements;
      @ ensures !containsAdvertisement(id) && advertisements.length == \old(advertisements.length) - 1;
      @ ensures (\exists int i; 0 <= i && i < \old(advertisements.length); \old(advertisements[i].getId()) == id);
      @ ensures (\forall int j; 0 <= j && j < advertisements.length;(\exists int i; 0 <= i && i < \old(advertisements.length); advertisements[j].equals(\old(advertisements[i]))));
      @ ensures (\forall int i; 0 <= i && i < people.length; people[i].isFavorable(id) ==> (\exists int j; 0 <= j && j < people[i].advertisements.length; people[i].advertisements.length == \old(people[i].advertisements.length) + 1) &&  people[i].advertisements[j] == id) );
      @ ensures (\forall int i; 0 <= i && i < people.length; !people[i].isFavorable(id) ==> !(\exists int j; 0 <= j && j < people[i].advertisements.length; people[i].advertisements[j] == id)) &&  people[i].advertisements.length == \old(people[i].advertisements.length));
      @ ensures (\forall int i; 0 <= i && i < people.length; (\forall int j; 0 <= j < \old(people[i].advertisements.length)(\exists int k; 0 <= k < people[i].advertisements.length;  \old(people[i].advertisements[j]) == people[i].advertisements[k])));
      @*/
    public void sendAdvertisement(int id);

考慮到Customer只會消費自己收到廣告，且此時對其有篇好的商品，故在Customer中設定一個廣告列表是有必要的，JML中也是按照這種思路進行描述的。

商品購買

    /*@ public normal_behavior
      @ requires contains(personId);
      @ requires getPerson(personId) instanceof Customer;
      @ requires containsProduct(productId);
      @ ensures getPerson(personId).isFavorable(productId) == true;
      @ ensures (\exists int cnt; cnt == (\sum int i;0<=i && i< \old(getPerson(personId).advertisements.length) && \old(getPerson(personId).advertisements[i].getId() == productId);1);getPerson(personId).advertisements.length == \old(getPerson(personId).advertisements.length) - cnt);
      @ also
      @ public normal_behavior
      @ requires !(getPerson(personId) instanceof Customer);
      @ assignable \nothing;
      @*/
    public /*@ pure @*/void buyProduct(int personId, int productId);

考慮到一個商品，Customer也許會重複地收到它的廣告，這裡設定：使用者買下產品後，他手中的關於該商品的廣告全部失效。

個人小發現：有關測試中可能算是遺漏的重要情況

在第三次作業Network類的addMessage方法中，判斷message相同的方法是這樣的。

      @ signals (EqualMessageIdException e) (\exists int i; 0 <= i && i < messages.length;
      @                                     messages[i].equals(message));

其採用的是呼叫messages[i].equals(message)的方法。

而觀察Message.equals方法

    /*@ also
      @ public normal_behavior
      @ requires obj != null && obj instanceof Message;
      @ assignable \nothing;
      @ ensures \result == (((Message) obj).getId() == id);
      @ also
      @ public normal_behavior
      @ requires obj == null || !(obj instanceof Message);
      @ assignable \nothing;
      @ ensures \result == false;
      @*/
    public /*@ pure @*/ boolean equals(Object obj);

會發現如果相比較的其中一個元素為null，則返回false。

然而大部分人判斷Message相同的方法，是建立一個HashMap或資訊ID的HashSet。實踐發現，當HashMap或HashSet當中存在null元素時，呼叫contains(null)或containsKey(null)將會返回true，與JML中的行為不符。

不過由於本次作業保證了不存在為null的Message，故這個遺漏並不會影響成績，但個人認為這作為一個考察點。

學習體會

這一單元如果僅僅為了通過測試的話，只需做一個無情的JML翻譯機器就可以了。但是如果能夠真正掌握JML的撰寫方法和撰寫規律，才能有更明顯的收穫。

本單元總體難度比之前低，但是要保證正確，思維的嚴謹性和視力的要求是很高的。到這一章的時候似乎大多數同學都已經用上了自己的評測機，我很慚愧到現在都還沒有做出來，希望下一單元能夠彌補這一缺憾。