利用JML規格準備測試資料

沒有使用Junit工具，而是採用生成大量資料與同學程式對拍的方法。為了保證資料的覆蓋率，採用以下幾點措施：

1、在資料開始時新增大量的點，減少無用的加邊操作。

2、靈活控制每條指令的權重，根據測試的需要進行調整。

3、為了構造特殊資料，在每次生成資料前隨機把一部分指令的權重變為零。

4、控制點數，使得圖即不會太稀疏也不會太小。

當然，也會手動構造一些測試資料以測試特殊的JML規格（如每組人數\(1111\)的限制）。

本單元架構設計及圖模型構建和維護策略

這一單元似乎並不很強調架構設計，因為JML已經把要怎麼做給規定好了。

圖模型的構建：

將人看做點，關係看作邊，value

對於某一個人，用HashMap維護其連出去的所有邊：key為邊的另一個人，value為這條邊的邊權（即value）。

維護策略：

由於指令數不多，給的時間也十分充足，很多資訊不需要動態維護，只需要低於平方級別的複雜度內完成一次詢問即可。

比如：

qci：用並查集維護，總複雜度\(\mathcal{O}(n\alpha(n))\)。

qlc：用Kruskal演算法，單次詢問複雜度\(\mathcal{O}(m\log m)\)。

sim：用Dijkstra演算法，單詞詢問複雜度\(\mathcal{O}((n+m)\log n)\)。

其它指令均按照JML規格暴力搞即可。（qgvs

由於每個指令至多加入一個點或一條邊，設\(T=\)總的指令條數，所以\(n,m\le T\)，總複雜度為\(\mathcal{O}(T^2\log T)\)。

程式碼實現出現的效能問題和修復情況

僅有第二次作業的強測沒有得到滿分，原因是中測資料太弱，dfg指令我沒有把人刪掉也沒有測出來。

其實我有對拍，拍了幾萬組資料都沒有問題。但我突然發現我qgvs的寫法會超時，改了寫法之後再對拍，似乎是對拍的引數設定錯了，沒有拍出來。

加了一兩行就修復了。

Network拓展

Advertiser類：投放廣告

每個 advertiser 有待投放的廣告列表，以及可能的目標人群。

在投放廣告的時候，針對特定的消費者人群，不浪費資源。

實現抽象方法：void putAdvertise(int id)，投放編號為 id 的廣告，如果不存在對應 id 的廣告，丟擲異常。

JML規格如下：

public interface Advertiser {
    /*@ public instance model non_null Person[] people;
      @ public instance model non_null Advertise[] advertise;
      @*/

    //@ ensures \result == (\exists int i; 0 <= i && i < advertise.length; advertise[i].getId() == id);
    public /*@ pure @*/ boolean contains(int id);

    /*@ public normal_behavior
      @ requires contains(id);
      @ assignable people[*].receivedAd;
      @ ensures people.length == \old(people.length);
      @ ensures (\forall int i; 0 <= i && i < \old(people.length);
      @          (\exists int j; 0 <= j && j < people.length; people[j] == \old(people[i])));
      @ ensures (\forall int i; 0 <= i && i < people.length && !(people[i] instanceof Customer); \not_assigned(people[i].receivedAd));
      @ ensures (\forall int i; 0 <= i && i < people.length && (people[i] instanceof Customer) ==>
      @ ( (people[i].receivedAd.length == \old(people[i].receivedAd.length) + 1) &&
      @ (\forall int k; 0 <= k && k < \old(people[i].receivedAd.length);
      @          (\exists int j; 0 <= j && j < people[i].receivedAd.length; people[i].receivedAd[j] == \old(people[i].receivedAd[k]))) &&
      @ (\exists int j; 0 <= j && j < people[i].receivedAd.length; people[i].receivedAd[j] == advertise[id]) );
      @ also
      @ public exceptional_behavior
      @ assignable \nothing;
      @ requires !contains(id1);
      @ signals (AdvertiseIdNotFoundException e) !contains(id);
      @*/
    public void putAdvertise(int id) throws AdvertiseIdNotFoundException;
}

Producer類：銷售商品

類中維護該 producer 銷售的商品列表、商品的庫存量以及營業額。

實現抽象方法：void sellCommodity(int id)，銷售編號為 id 的商品，銷售商品時，如果不存在對應 id 的商品，丟擲異常。

JML規格如下：

public interface Producer {
    /*@ public instance model non_null Commodity[] commodity;
      @ public instance model non_null int[] turnover;
      @ public instance model non_null int[] storage;
      @*/

    //@ ensures \result == (\exists int i; 0 <= i && i < commodity.length; commodity[i].getId() == id);
    public /*@ pure @*/ boolean contains(int id);

    /*@ public normal_behavior
      @ requires contains(id);
      @ assignable turnover, storage;
      @ ensures turnover.length == \old(turnover.length);
      @ ensures storage.length == \old(storage.length);
      @ ensures (\forall int i; 0 <= i && i < commodity.length && (commodity[i].getId() != id) == >
      @     ( turnover[i] == \old(turnover[i]) && storage[i] == \old(storage[i]) ) );
      @ ensures (\forall int i; 0 <= i && i < commodity.length && (commodity[i].getId() == id) == >
      @     ( turnover[i] == \old(turnover[i]) + cnt * commodity.price && storage[i] == \old(storage[i]) - cnt ) );
      @ also
      @ public exceptional_behavior
      @ assignable \nothing;
      @ requires !contains(id1);
      @ signals (CommodityIdNotFoundException e) !contains(id);
      @*/
    public void sellCommodity(int id, int cnt) throws CommodityIdNotFoundException;
}

Customer類：選擇自己偏好匹配的產品購買

類中維護該 customer 擁有的商品 id、收到的廣告、擁有的錢、對商品的偏好（假設對所有商品的偏好值都不同）。

實現抽象方法：int buyCommodity()，根據當前收到的廣告、擁有的錢和商品的偏好，購買一種商品，返回對應的商品 id。若當前的錢不足以購買任意一種商品，返回\(-1\)。

JML規格如下：

public interface Customer {
    /*@ public instance model int[] commodity;
      @ public instance model Advertise[] receivedAd;
      @ public instance model int money;
      @ public instance model Map<Integer, Integer> preference;
      @*/

    /*@ public normal_behavior
      @ requires (\exist int i; 0 <= i && i < receivedAd.length; receivedAd[i].commodity.price <= \old(money));
      @ assignable commodity, money;
      @ ensures (\exist int i; 0 <= i && i < receivedAd.length; receivedAd[i].commodity.getId() == \result && money == \old(money) - receivedAd[i].commodity.getPrice());
      @ ensures !(\exist int i; 0 <= i && i < receivedAd.length; \old(money) >= receivedAd[i].commodity.getPrice() &&
      @     preference.get(receivedAd[i].commodity.getId()) > preference.get(\result));
      @ ensures commodity.length == \old(commodity.length) + 1;
      @ ensures (\forall int i; 0 <= i && i < \old(commodity.length);
      @          (\exists int j; 0 <= j && j < commodity.length; people[j] == \old(commodity[i])));
      @ ensures (\exist int i; 0 <= i && i < commodity.length); commodity[i] == \result);
      @ also
      @ public normal_behavior
      @ assignable \nothing;
      @ requires (\forall int i; 0 <= i && i < receivedAd.length; receivedAd[i].commodity.price > \old(money));
      @ ensures \result == -1;
      @*/
    public int buyCommodity();
}

本單元學習體會

本單元學習了JML規格，在我看來是一種形式化表述，規定了程式應該達到怎樣的效果。閱讀JML規格其實並沒有太大障礙，即使沒有系統地學習，也能猜個大概。但編寫JML規格確實挺困難的，一方面寫出來的不規範，一方面總會遺漏掉一些條件。如果真的想學好的話，還是應該多練練。另外，本單元的測試格外重要，花在測試上的時間甚至比編寫程式碼的時間還要長。測試的時候一定要認真仔細，一不小心就翻車了。