2. 程式人生 > 其它 >2022年北航面向物件程式設計第三單元總結

2022年北航面向物件程式設計第三單元總結

阿新 • • 發佈：2022-06-06

2022年北航面向物件程式設計第三單元總結

目錄

本單元是一個快樂單元，作為OO的受難者，迄今第一次體會到”迭代開發“的感覺，並且JML的規格很詳細，寫起來非常快，為辛苦寫JML的助教xgg們點贊~

作業內容概述

這一單元的工作任務其實在指導書中寫的並不詳細，可能算是單元特色吧，實際的工作任務全都寫在了JML裡，或許不寫這個部落格我都不知道這一單元寫的是個什麼東西\doge

。

其實是JML寫太好了（手動狗頭），任務工作在JML裡面的表述要比從工作內容上講更加易於寫程式碼，所以這裡就大致講一下好了，下面會用JML舉例

本單元的主要內容是建立一個社交網路體系，主要有Person類，代表社交網路的個體；Group類，代表一個社交團體；Network類，作為社交網路的主要承載類和操作類；Message類，表示社交個體中的成員傳送訊息

從整體形式上，依舊是一個操作的大模擬，這很OO~

關於JML

\[有一門程式碼語言規格用來指導程式碼的實現，寫起來比實際的程式碼都長~ \]

我目前感受到的特點就是這樣的，本單元官方包JML中的JML的書寫帶給人一種離散數學上的嚴格的規格定義下的規範，感覺非常地嚴謹，第一週的時候還沒有開始做作業就進了上機實驗，因為沒看過JML，上機差點寄了，那會兒覺得JML好高大上，後來看了幾條之後習慣了就覺得套路還是比較明顯的，實現難度也不是很高

比如：

對於add等（以addMessage舉例）

JML中是這樣的

/*@ public normal_behavior
  @ requires !(\exists int i; 0 <= i && i < messages.length; messages[i].equals(message)) &&
  @           (message instanceof EmojiMessage) ==> containsEmojiId(((EmojiMessage) message).getEmojiId()) &&
  @            (message.getType() == 0) ==> (message.getPerson1() != message.getPerson2());
  @ assignable messages;
  @ ensures messages.length == \old(messages.length) + 1;
  @ ensures (\forall int i; 0 <= i && i < \old(messages.length);
  @          (\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i]))));
  @ ensures (\exists int i; 0 <= i && i < messages.length; messages[i].equals(message));
  @ also
  @ public exceptional_behavior
  @ signals (EqualMessageIdException e) (\exists int i; 0 <= i && i < messages.length;
  @                                     messages[i].equals(message));
  @ signals (EmojiIdNotFoundException e) !(\exists int i; 0 <= i && i < messages.length;
  @                                       messages[i].equals(message)) &&
  @                                       (message instanceof EmojiMessage) &&
  @                                       !containsEmojiId(((EmojiMessage) message).getEmojiId());
  @ signals (EqualPersonIdException e) !(\exists int i; 0 <= i && i < messages.length;
  @                                     messages[i].equals(message)) &&
  @                                     ((message instanceof EmojiMessage) ==>
  @                                     containsEmojiId(((EmojiMessage) message).getEmojiId())) &&
  @                                     message.getType() == 0 && message.getPerson1() == message.getPerson2();
  @*/
public void addMessage(Message message) throws
        EqualMessageIdException, EmojiIdNotFoundException, EqualPersonIdException;

實現起來是這樣的

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

翻譯以下這段JML就是：需要找的找不到或者已經有一個現在重複了就拋異常，其他情況正常進行，需要確保原來有的現在都要有，新的比原來的多了一個現在加入的

其實用一句話概括這段JML就是：需要找的找不到或者已經有一個現在重複了就拋異常，其他情況就把這個直接新增進所用的容器中

掌握了指導書中的JML的規格寫起來真的飛快，畢竟寫的比程式碼還要詳細~

一些tips

  1. 在同學們互相討論的時候也聽過很多同學提到過新舊比對的過程（因為指導書都在不停地更新），所以判斷當前的要求與已經做完的部分有無差異還是很有必要的，我第二週作業的時候是用的線上的文字比較工具線上文字差異對比,文字比對、文字比較工具 (jq22.com)（老CO人了），第三週的時候用的同學推薦的IDEA外掛，個人感覺還是比較有意義的
  2. 對於JML的測試，聽指導書和助教說的Junit和OpenJML測試，個人感覺效率上實在很難保證，我通過官方給的案例分析，感覺我們的專案的複雜度還遠不及需要單一模組測試的程度，and 還有一個非常重要的點就是，直接通過JML實現出來的某些部分是無法完全滿足測試要求的，這部分程式碼也非常不易於使用JML測試，而這部分卻通常是測試的重點，因此我在本單元的測試精力並沒有放在JML測試上
  3. JML閱讀，在IDEA裡面其實不太方便，特別是括號匹配的上的高亮，感覺在閱讀過程中對提高效率很有幫助，IDEA裡面檢視的話除非找一些外掛載入（或者像配置vim一樣手寫指令碼？），但相比與直接複製到VS Code中去掉註釋符，我還是感覺後者比較方便
  4. 剛開始做JML的時候可以多看看《JML Level 0手冊》，擺個連結，需要可以自取（連結：https://pan.baidu.com/s/1Iw0CQPOqwJ_fCs2-XyRazA 提取碼：6666 ，裡面還有一些其他的資料，但最推薦先閱讀的還是JML Level 0手冊）

homework~

模型構建和維護策略

除了Person中的message為了更好地契合JML的要求，選用了LinkedList之外，其他一律選擇了Map作為容器（畢竟直接getId實在是太方便了），為了更好地對輸出進行toString方式的斷點測試，我所有的Map都用的TreeMap，但實際應該還是HashMap更快一點，在這裡還是推薦HashMap（我以前一直以為HashMap的尋找是O(n)的，最近才發現是O(1)的，之前只是想用一個穩定的方案，後面知道了也因為除錯的關係不想改了）

各個版本的迭代和維護其實今年個人感覺課程組很良心，沒有那種設坑型的誘導開發，感覺每週的工作基本都是獨立的，比如第一週的並查集，只考慮新增和查詢，並不需要刪除，後兩週也沒有相關的刪除操作，在實現上非常地舒服，只需要保證往期的bug都修復了就基本沒什麼問題了

演算法

本單元的形式大概就是通過JML實現絕大多數的類方法的開發+1個圖論基礎演算法的考察，總的來看還是非常輕鬆的，任務也很明確，第一單元是考察並查集，第二單元是考察最小生成樹，第三單元是考察最短路，都是圖論最基礎的演算法，整體的實現也非常地簡單

  1. 並查集

    相比於裸的遍歷查詢，裸的並查集查詢可以限制搜尋區域僅在自己的祖先團體中，但這二者的複雜度仍停留在\(O(n)\)，而並查集可以通過對合並優化或路徑壓縮變成複雜度小於\(O(log_2n)\)的演算法，所以並查集的優化非常重要

    並查集的優化是可以二選其一的，相比於合併優化的冗長程式碼+一個height陣列（或其他容器）的引入，路徑壓縮的實現會非常優雅（使用遞迴的方式甚至只比原非路徑壓縮多1行程式碼，避免爆棧使用非遞迴的方式也會比合並優化簡單），所以這裡就直接講路徑壓縮了（這會兒找不到之前學的時候看的那個資料了，只記得這個結論）

    實現中主要的方法為下面兩個，即合併和查詢（這裡的查詢已經使用了路徑壓縮）

    private final TreeMap<Integer, Integer> disjointSet;

private void unionSet(int id1, int id2) {
    int idn1 = findSet(id1);
    int idn2 = findSet(id2);
    if (idn1 != idn2) {
        disjointSet.put(idn1, disjointSet.get(idn2));
    }
}

private int findSet(int id) {
    if (id != disjointSet.get(id)) {
        disjointSet.put(id, findSet(disjointSet.get(id)));
    }
    return disjointSet.get(id);
}

    除此之外，其他需要加入並查集邏輯的就是在新新增一個Person的時候需要在該並查集中加入其並查集的元素（key和value都設定為其ID）

    @Override
public void addPerson(Person person) throws EqualPersonIdException {
    for (Integer id : people.keySet()) {
        if (people.get(id).equals(person)) {
            throw new MyEqualPersonIdException(id);
        }
    }
    people.put(person.getId(), person);
    disjointSet.put(person.getId(), person.getId()); // Here
}

    然後在addRelation的時候進行合併操作即可

    @Override
public void addRelation(int id1, int id2, int value)
    throws PersonIdNotFoundException, EqualRelationException {
    if (!people.containsKey(id1)) {
        throw new MyPersonIdNotFoundException(id1);
    } else if (!people.containsKey(id2)) {
        throw new MyPersonIdNotFoundException(id2);
    } else if (people.get(id1).isLinked(people.get(id2))) {
        throw new MyEqualRelationException(id1, id2);
    }
    ((MyPerson) people.get(id1)).addRelation(id2, people.get(id2), value);
    ((MyPerson) people.get(id2)).addRelation(id1, people.get(id1), value);
    for (Integer id : groups.keySet()) {
        ((MyGroup) groups.get(id)).addRelation(id1, id2, value);
    }
    unionSet(id1, id2); // Here
}

    接著再補充一下路徑壓縮的方法，先放上三個查詢的優化的程式碼

    // 無優化版查詢
private int findSet(int id) {
    return id == disjointSet.get(id) ? id : findSet(disjointSet.get(id));
}

// 遞迴版路徑壓縮
private int findSet(int id) {
    if (id != disjointSet.get(id)) {
        disjointSet.put(id, findSet(disjointSet.get(id)));
    }
    return disjointSet.get(id);
}

//非遞迴版路徑壓縮
private int findSet(int id) {
    int r = id;
    while (disjointSet.get(r) != r) {
        r = disjointSet.get(r);
    }
    int i = id, j;
    while (i != r) {
        j = disjointSet.get(i);
        disjointSet.put(i, r);
        i = j;
    }
    return r;
}

    因為本單元測試中的公測和互測的資料量都不足以爆棧，我更推薦遞迴版的路徑壓縮演算法

    （我在寫這篇部落格的時候聽同學說可以合併秩優化+路徑壓縮，但我改了TreeMap之後沒用合併秩也比他快，感興趣的同學可以在寫這裡的時候做一下兩種寫法的測試，合併秩+路徑壓縮可以參考我的hxd的blogOO 第三單元總結 - cywuuuu - 部落格園 (cnblogs.com)）

  2. 最小生成樹

    經過了大量的資料測試，本單元的資料強度對於person量的依賴度非常高，以互測的5000上限為例，至少需要600人才能達到有效的測試Hack（實際生成的時候，最適的個人預估在1200個Person上下），而在這種的人數限制下，5000條資料對於圖的構建，必然是一個稀疏圖，因此Kruskal演算法肯定是要優於Prim的（兩個實現起來都不是很難，有興趣的同學可以做一下測試）

    首先擺一下我的qlc的處理演算法

    private TreeMap<Integer, Integer> kruskal;

private int findAdd(int id) {
    if (id != kruskal.get(id)) {
        kruskal.put(id, findAdd(kruskal.get(id)));
    }
    return kruskal.get(id);
}

@Override
public int queryLeastConnection(int id) throws PersonIdNotFoundException {
    if (!people.containsKey(id)) {
        throw new MyPersonIdNotFoundException(id);
    }
    ArrayList<Edge> edges = new ArrayList<>();
    TreeMap<Integer, TreeSet<Integer>> hasAdd = new TreeMap<>();
    kruskal = new TreeMap<>();
    kruskal.put(id, id);
    for (Integer personId : people.keySet()) {
        if (findSet(personId) == findSet(id) && personId != id) {
            TreeMap<Integer, Person> acquaintance =
                ((MyPerson) people.get(personId)).getAcquaintance();
            TreeMap<Integer, Integer> value = ((MyPerson) people.get(personId)).getValue();
            for (Integer acquaintanceId : acquaintance.keySet()) {
                if ((hasAdd.get(personId) != null &&
                     hasAdd.get(personId).contains(acquaintanceId)) ||
                    hasAdd.get(acquaintanceId) != null &&
                    hasAdd.get(acquaintanceId).contains(personId)) {
                    continue;
                }
                if (hasAdd.get(personId) == null) {
                    TreeSet<Integer> hasAddAcquaintance = new TreeSet<>();
                    hasAddAcquaintance.add(acquaintanceId);
                    hasAdd.put(personId, hasAddAcquaintance);
                } else {
                    hasAdd.get(personId).add(acquaintanceId);
                }
                Edge edge = new Edge(personId, acquaintanceId,
                                     value.get(acquaintanceId), false);
                edges.add(edge);
            }
            kruskal.put(personId, personId);
        }
    }
    Collections.sort(edges); // Attention！
    // kruskal
    int ans = 0;
    for (int i = 0; i < edges.size(); i++) {
        int b = findAdd(edges.get(i).getStart());
        int c = findAdd(edges.get(i).getEnd());
        if (b == c) {
            continue;
        }
        kruskal.put(c, kruskal.get(b));
        ans += edges.get(i).getWeight();
    }
    return ans;
}

    首先還是需要一個Map當作並查集使用，操作方式跟第一週的相同，這裡直接把合併操作寫在了程式碼中

    可以看到kruskal的核心程式碼非常少，主要的操作都是在處理並查集（qlc的集合的建立），實際的實現只需要從小到大加入邊，不成環的就進行加入即可（實際還可以加一個變數進行計數，到n-1時即可break，但感覺這樣的剪枝優化有限，主要是沒那麼優雅，而且也不會導致超時，遂沒寫）

    這裡提一個可能被忽略的點：即程式碼中標出的Collections.sort(edges)

    使用Kruskal演算法需要生成一個用於表達邊的類，先擺上自己的程式碼來講（因為不算太長，就全擺了，強迫症狂喜）

    package run;

public class Edge implements Comparable<Edge> {
    private final int start;
    private final int end;
    private final int weight;

    public Edge(int start, int end, int weight, boolean flag) {
        this.start = flag ? start : Math.min(start, end);
        this.end = flag ? end : Math.max(start, end);
        this.weight = weight;
    }

    @Override
    public int compareTo(Edge edge) {
        if (this.weight != edge.getWeight()) {
            return this.weight < edge.getWeight() ? -1 : 1;
        } else if (this.start != edge.getStart()) {
            return this.start < edge.getStart() ? -1 : 1;
        } else {
            return this.end < edge.getEnd() ? -1 : 1;
        }
    }

    @Override
    public boolean equals(Object o) {
        if (o == null || !(o instanceof Edge)) {
            return false;
        }
        return (this.start == ((Edge) o).getStart()) && (this.end == ((Edge) o).getEnd());
    }

    public int getStart() {
        return start;
    }

    public int getEnd() {
        return end;
    }

    public int getWeight() {
        return weight;
    }
}

    這裡主要是compareTo這個點需要注意

    /* 錯誤寫法 */
@Override
public int compareTo(Edge edge) {
    return this.weight < edge.getWeight() ? -1 : 1;
}

/* 正確寫法 */
@Override
public int compareTo(Edge edge) {
    if (this.weight != edge.getWeight()) {
        return this.weight < edge.getWeight() ? -1 : 1;
    } else if (this.start != edge.getStart()) {
        return this.start < edge.getStart() ? -1 : 1;
    } else {
        return this.end < edge.getEnd() ? -1 : 1;
    }
}

    在C/C++中，使用STL或qsort的時候寫cmp的函式經常會使用類似上面的第一種寫法，但是在java中這種寫法會導致Collections.sort()中出現監視器異常的錯誤。這兩種寫法的區別是在weight相等的時候，如果集合中有兩個相同的元素，第一個的執行的結果判斷僅與當前取出的有關，比如有Object1和Object2他們的weight相同，如果取出的是Object1那麼Object1就會排在Object2後面，如果取出的是Object2那麼Object1就會排在Object2前面，而如果一次排序中出現了兩次或以上Object1和Object2的比較，且二者都有取出過，那麼java就會認為未定義這種情況的排序規則，就會丟擲相應的異常，因此使用Collections.sort()的時候一定需要保證兩個物件在比較的過程中的大小關係是固定的（第二種寫法是因為start、end和weight不會完全相同，所以可以用這種寫法分開）

  3. 最短路

    最短路演算法我是直接莽了一個無優化的dijkstra，強測CTLE了一個點，悲，懶是萬惡之源，這裡就給大家做錯誤示範了

    （我自測的時候使用隨機資料幾乎不可能Hack到這個點，後面我會講這個點的Hack資料）

    private int dijkstra(Message message) {
    int start = message.getPerson1().getId();
    dis.put(start, 0);
    PriorityQueue<Node> queue = new PriorityQueue<>();
    queue.add(new Node(start, dis.get(start)));
    while (!queue.isEmpty()) {
        Node u = queue.poll();
        if (done.get(u.getId())) {
            continue;
        }
        done.put(u.getId(), true);
        ArrayList<Edge> neighboor = nodeEdges.get(u.getId());
        for (Edge y : neighboor) {
            if (done.get(y.getEnd())) {
                continue;
            }
            if (dis.get(y.getEnd()) > y.getWeight() + u.getDis()) {
                dis.put(y.getEnd(), y.getWeight() + u.getDis());
                queue.add(new Node(y.getEnd(), dis.get(y.getEnd())));
                preNode.put(y.getEnd(), u.getId());
            }
        }
    }
    return dis.get(message.getPerson2().getId());
}

    （正確寫法推薦參考下ywxgg的blog，OO 第三單元總結 - cywuuuu - 部落格園 (cnblogs.com)）

測試思路與互測策略

本單元的JML限制下，特別是add與查詢在指令裡面是共享總資料量的限制的，因此全部指令直接隨機生成的資料強度非常有限，只能做一些基礎的指令測試

自從厭倦與追尋，我已學會一覓即中，自從一股逆風襲來，我已能御八面來風駕舟而行，自從前兩個單元都借了ygg和ywgg的資料生成器，我已學會了在測試前不經思考要不要自己寫資料生成器而是直接去問ygg和ywgg有沒有寫資料生成器

我的作用就是提一點資料生成建議和問題反饋（

但二位又是同以前一樣，都沒有寫自己的資料生成思路，不過還是擺擺blog吧，苟富貴，勿相忘，\doge（OO_Unit3_JML - 青衫染墨 - 部落格園 (cnblogs.com), OO 第三單元總結 - cywuuuu - 部落格園 (cnblogs.com))

下面講下我的資料生成測試吧，或許我的作用又多了一個

框架呢，當然是直接用二位xgg的python函式，對於三週公共資料構造方向，首先是add與查詢與演算法測試分離，先保證已有一定的資料量之後再進行查詢，並做查詢與add的混合測試，然後再全部的add構建完後進行演算法測試（因為互測的資料限制，重建圖或者重搜尋新增的優化沒做的也Hack不到，因此沒必要做add與演算法的混合測試），所以總的資料情況大致生成為3000-4500條add，然後加入各查詢進行測試，此外對於組內測試，僅生成一個組更利於組內的功能複雜度測試，對於異常測試，不通過上述規律，直接進行可控異常資料佔比的隨機資料的分佈測試效果更優

對於每週的互測情況

我第一週的房間裡全部都沒bug，評測姬忙乎了一整天一個也沒測出來，最終就是和平房，整個房間都沒人Hack成功過

第二週我出了個非常沙雕的錯誤

/* bug */
@Override
public void print() {
    System.out.printf("emi-%d, %d-%d", count, id, EXCEPTIONS.get(id));
}

/* 正確寫法 */
@Override
public void print() {
    System.out.printf("emi-%d, %d-%d\n", count, id, EXCEPTIONS.get(id));
}

於是第一次進了C房，and 給大家講講C房的狀況奧，首先只有6個人，然後只有6個人，最後只有6個人

所以不要相信中測。。。我這學期只有這一週沒有搭評測姬，直接用的ywgg的評測姬，他使用的資料比對的方式沒有測\n的問題，哭哭o(╥﹏╥)o

C房真的就是隨便交大一點的資料就能亂殺。。。但我實在不好意思接著Hack下去了，只交了5次，中了20個就run了，最後也是改了倆字元就bugfree了（

這裡講個手捏送給同學的測試案例吧（這個資料是受傑哥提示的\doge）

首先就是Group有的一個1111的限制，這個1111的限制中測和強測都沒測到，因此ABC通殺

然後就是JML的qgvs指令，如果按照JML來寫，就是兩次迴圈求和，如果針對性的構造卡住Group的資料，並使用1000+的qgvs指令就可以直接Hack到TLE，這一個也是中測強測都沒測到，依舊ABC通殺

因此可以混合兩個測試點構造如下

ap 1 1 152
ap 2 2 21
ap 3 3 68
ap 4 4 160
ap 5 5 0
ap 6 6 12
ap 7 7 86
ap 8 8 5
''' 共1112個
ag 1
atg 1 1
atg 2 1
atg 3 1
atg 4 1
atg 5 1
atg 6 1
atg 7 1
''' 共1112個
qgvs 1
qgvs 1
qgvs 1
qgvs 1
''' 然後qgvs到資料上限

需要注意的是需要卡一下ap 1112的qgvs要與 ap 前1111的不同，不然中不了1111的bug

也可以直接一手2400人塞進去，然後直接qgvs來Hack 1111的bug

第三週是隨機資料殺了一波（以及1111的bug我又中了一個人），然後又Hack了一下sim的超時bug

隨機資料如上面的資料的公共特點中所述，1111如2中的資料

sim的資料構造如下

''' 建立1111個人
ag 1
''' 把1111個人加入group1中
ar 1 138 536
ar 1 595 852
ar 1 632 678
ar 1 634 197
ar 1 836 797
ar 1 950 656
ar 2 718 120
ar 2 769 25
''' 然後隨機addRelation，排序輸出
am 1 -869 0 2 718
am 2 528 0 4 29
am 3 -171 0 4 930
am 4 845 0 4 1075
am 5 1000 0 6 284
am 6 777 0 7 837
am 7 -180 0 7 1089
am 8 -101 0 8 156
am 9 612 0 9 671
am 10 -335 0 10 208
''' 隨機add 500條message
sim 1
sim 2
sim 3
sim 4
sim 5
sim 6
sim 7
sim 8
sim 9
sim 10
''' 對500條message分別sim

這個資料我中了4個人，估計都是跟我一樣ddl前夜懶得優化的（

Network JML拓展

拓展要求

假設出現了幾種不同的Person

  • Advertiser：持續向外傳送產品廣告
  • Producer：產品生產商，通過Advertiser來銷售產品
  • Customer：消費者，會關注廣告並選擇和自己偏好匹配的產品來購買 -- 所謂購買，就是直接通過Advertiser給相應Producer發一個購買訊息
  • Person：吃瓜群眾，不發廣告，不買東西，不賣東西

如此Network可以支援市場營銷，並能查詢某種商品的銷售額和銷售路徑等 請討論如何對Network擴充套件，給出相關介面方法，並選擇3個核心業務功能的介面方法撰寫JML規格（借鑑所總結的JML規格模式）

我的設計

首先約定一下需要新加的屬性

對於廣告發布過程，需要引入一個新的Message子類，暫且命名為Advertisement

對於購買過程，同樣需要引入一個新的Message子類，暫且命名為Purchase

由於要實現Customer通過貨物的喜好程度進行購買，Producer通過傳遞來的購買資訊確認貨物資訊進行增加收入

所以首先需要新增一個貨物類，加入一個貨物ID（或名稱）、貨物吸引力和貨物價格，並加入一個貨物來源

已存在類新增/修改：

Person類需要新增

  1. 四種類型的人的標識（約定每個人只能扮演一種角色，可以用繼承來實現）
  2. 貨物列表（僅Producer類使用並負責初始化）和其當前的銷售額
  3. 新增貨物的方法
  4. 篩選最喜歡的貨物決定是否傳送購買資訊的方法
  5. 幫助傳送購買資訊的方法
  6. 將自己的某個貨物請求廣告商做宣傳的方法
  7. 向與自己聯絡的所有顧客釋出貨物廣告的方法（假定給與自己聯絡的所有人都發，這樣比較符合廣告商的身份）

Network裡需要新增或修改

  1. 新增貨物ID與銷售情況的Map關係（下面新建了一個Sales類和Trace類，用來記錄銷售情況和銷售路徑）
  2. 新增貨物的方法
  3. 新增令某一個顧客開始挑選是否有喜歡的貨物的方法，如果有則生成一個Purchase的Message
  4. 新增令生產商決定push某個貨物去做宣傳的方法，並生成一個Advertisement的Message
  5. 修改sendMessage方法，新增Purchase和Advertisement的傳送的執行

新引入：

Product類需要包含

  1. 貨物ID（或名稱）
  2. 貨物價格
  3. 貨物吸引力
  4. 貨物來源（生產商ID）
  5. 各屬性的get方法

Purchase類需要包含

  1. 購買的貨物ID

Advertisement類需要包含

  1. 貨物

Sales類需要包含

  1. 銷售額
  2. Trace的列表

Trace類需要包含

  1. Producer
  2. Advertiser
  3. Customer
  4. isSold （標記該貨物是否以及被售賣）

整個流程可以大致描述如圖

感覺這裡面最核心的幾個分別是：

  1. 新增令某一個顧客開始挑選是否有喜歡的貨物的方法，如果有則生成一個Purchase的Message
  2. 新增令生產商決定push某個貨物去做宣傳的方法，並生成一個Advertisement的Message
  3. 修改sendMessage方法，新增Purchase和Advertisement的傳送的執行

所以這裡就以這三個為例書寫在我的約定下的JML

首先對於讓顧客開始挑選喜歡的貨物：

方法定義：boolean pickTheGoods(int personId, int limit)

思路為：輸入personId，和確定為喜歡的貨物的下限，在該person的receiveMessage（至多前三個）中搜索Advertise的貨物的吸引力有沒有超過limit的，如果有則取吸引力最高的，確定取的情況下最高吸引力若相同則取id小的，以此生成購買資訊

對應的JML如下：

	/*@ public normal_behavior
      @ requires contains(personId)
      @ assignable messages, productSales;
      @ ensures contains(personId) && (\exist int i; 0 <= i && i < people.get(personId).getReceivedMessages.length && 
      @          (people.get(personId).getReceivedMessages[i] instanceof Advertisement && 
      @          ((Advertisement)people.get(personId).getReceivedMessages[i]).getProduct().getAttractive() >= limit) ==> 
      @            messages.length == \old(messages.length) + 1 && (\forall int i; 0 <= i && i < \old(messages.length); 
      @            !(\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i]))) ==> 
      @              messages[i] instanceof PurchaseMessage && ((PurchaseMessage)messages[i]).getProductId == people.get(personId).getMaxAttributeId()) && 
      @            product.length == \old(product.length) + 1 && (\forall int i; 0 <= i && i < \old(product.length); 
      @            (\exists int j; 0 <= j && j < product.length; product[j].equals(\old(product[i])))) && products.get(((Purchase)messages[i]).getProductId()) != null && 
      @            productSales.getProductSale(people.get(personId).getMaxAttributeId()).getProducer() == products.get(((Purchase)messages[i]).getProductId()).getProducer() && 
      @            (\exist int i; 0 <= i && i < people.get(personId).getAcquaintance().length; people.get(personId).getAcquaintance()[i].isLinked(people.get(personId)) && 
      @            people.get(personId).getAcquaintance()[i].isLinked(people.get(productSales.getProductSale(people.get(personId).getMaxAttributeId()).getProducer().getId())) ==> 
      @            productSales.getProductSale(people.get(personId).getMaxAttributeId()).getAdvertiser() == people.get(personId).getAcquaintance()[i]) && 
      @          productSales.getProductSale(people.get(personId).getMaxAttributeId()).getCustomer() == people.get(personId));
      @ ensures contains(personId) && !(\exist int i; 0 <= i && i < people.get(personId).getReceivedMessages.length && (people.get(personId).getReceivedMessages[i] instanceof Advertisement && 
      @          ((Advertisement)people.get(personId).getReceivedMessages[i]).getProduct().getAttractive() >= limit) ==> (\not_assigned(messages[*]) && \not_assigned(productSales[*]));
      @ also
      @ public exceptional_behavior
      @ signals (PersonIdNotFoundException e) !contains(personId);
      @*/
	boolean pickTheGoods(int personId, int limit) throws PersonIdNotFoundException;

對於生產商push貨物做宣傳：

方法定義：void advertiseGoods(int personId, int productId)

思路為：輸入personId，在該Advertiser下對其相連的People進行遍歷，對每個Customer以輸入的productId為依據生成一個Advertisement

對應的JML如下：

	/*@ public normal_behavior
      @ requires contains(personId) && people.get(personId) instanceof Advertiser && containProducts(productsId) && (Advertiser)people.get(personId).isLinked(products.get(productId).getProducer())
      @ assignable messages;
      @ ensures messages.length == \old(messages.length) + (\count int i; 0 <= i && i < people.get(personId).getAcquaitance().length; people.get(personId).getAcquaitance()[i] instanceof Customer);
      @ ensures (\forall int i; 0 <= i && i < \old(messages.length); (\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i]))));
      @ ensures (\forall int i; 0 <= i && i < messages.length; !(\exists int j; 0 <= j && j < \old(messages).length; \old(messages[j]).equals(messages[i])) ==> messages[i] instance of Advertisement && 
      @         ((Advertisement)messages[i]).getPerson1 == people.get(personId) && (\exist int i; 0 <= i && i < people.get(personId).getAcquaitance().length; 
      @           people.get(personId).getAcquaitance()[i] instanceof Customer && ((Advertisement)messages[i]).getPerson2 == people.get(personId).getAcquaitance()[i]) && 
      @         ((Advertisement)messages[i]).getProduct() == products.get(productId));
      @ also
      @ public exceptional_behavior
      @ signals (PersonIdNotFoundException e) !contains(personId);
      @ signals (PersonTypeNotCorrespondingException e) contains(personId) && !(people.get(personId) instanceof Advertiser);
      @ signals (ProductIdNotFoundException e) contains(personId) && people.get(personId) instanceof Advertiser && !containProducts(productsId);
      @ signals (AdvertiserNotLinkedException e) contains(personId) && people.get(personId) instanceof Advertiser && containProducts(productsId) && 
      @                                          !(Advertiser)people.get(personId).isLinked(products.get(productId).getProducer())
      @*/
	void advertiseGoods(int personId, int productId) throws PersonIdNotFoundException, PersonTypeNotCorrespondingException, ProductIdNotFoundException, AdvertiserNotLinkedException;

對於sendMessage引入Purchase和Advertisement

思路為：

對Purchase資訊：需要修改其中的貨物銷售額，和isSold資訊，並使生產商獲得相當於該貨物銷售額的money，使消費者減少相當於該貨物銷售額的money

對Advertisement資訊：無特殊處理

對應的JML如下：

/*@ public normal_behavior
      @ requires containsMessage(id) && getMessage(id).getType() == 0 &&
      @          getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) &&
      @          getMessage(id).getPerson1() != getMessage(id).getPerson2();
      @ assignable messages, emojiHeatList;
      @ assignable getMessage(id).getPerson1().socialValue, getMessage(id).getPerson1().money;
      @ assignable getMessage(id).getPerson2().messages, getMessage(id).getPerson2().socialValue, getMessage(id).getPerson2().money;
      @ 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 \old(getMessage(id)).getPerson1().getSocialValue() ==
      @         \old(getMessage(id).getPerson1().getSocialValue()) + \old(getMessage(id)).getSocialValue() &&
      @         \old(getMessage(id)).getPerson2().getSocialValue() ==
      @         \old(getMessage(id).getPerson2().getSocialValue()) + \old(getMessage(id)).getSocialValue();
      @ ensures (\old(getMessage(id)) instanceof RedEnvelopeMessage) ==>
      @         (\old(getMessage(id)).getPerson1().getMoney() ==
      @         \old(getMessage(id).getPerson1().getMoney()) - ((RedEnvelopeMessage)\old(getMessage(id))).getMoney() &&
      @         \old(getMessage(id)).getPerson2().getMoney() ==
      @         \old(getMessage(id).getPerson2().getMoney()) + ((RedEnvelopeMessage)\old(getMessage(id))).getMoney());
      @ ensures (\old(getMessage(id)) instanceof PurchaseMessage) ==>
      @         (\old(getMessage(id)).getPerson1().getMoney() ==
      @         \old(getMessage(id).getPerson1().getMoney()) - ((PurchaseMessage)\old(getMessage(id))).getProduct().getPrice() &&
      @         \old(getMessage(id)).getPerson2().getMoney() ==
      @         \old(getMessage(id).getPerson2().getMoney()) + ((PurchaseMessage)\old(getMessage(id))).getProduct().getPrice());
      @ ensures (!(\old(getMessage(id)) instanceof RedEnvelopeMessage) && !(\old(getMessage(id)) instanceof Purchase)) ==> (\not_assigned(people[*].money));
      @ ensures (\old(getMessage(id)) instanceof EmojiMessage) ==>
      @         (\exists int i; 0 <= i && i < emojiIdList.length && emojiIdList[i] == ((EmojiMessage)\old(getMessage(id))).getEmojiId();
      @         emojiHeatList[i] == \old(emojiHeatList[i]) + 1);
      @ ensures (!(\old(getMessage(id)) instanceof EmojiMessage)) ==> \not_assigned(emojiHeatList);
      @ ensures (\forall int i; 0 <= i && i < \old(getMessage(id).getPerson2().getMessages().size());
      @          \old(getMessage(id)).getPerson2().getMessages().get(i+1) == \old(getMessage(id).getPerson2().getMessages().get(i)));
      @ ensures \old(getMessage(id)).getPerson2().getMessages().get(0).equals(\old(getMessage(id)));
      @ ensures \old(getMessage(id)).getPerson2().getMessages().size() == \old(getMessage(id).getPerson2().getMessages().size()) + 1;
      @ also
      @ public normal_behavior
      @ requires containsMessage(id) && getMessage(id).getType() == 1 &&
      @           getMessage(id).getGroup().hasPerson(getMessage(id).getPerson1());
      @ assignable people[*].socialValue, people[*].money, messages, emojiHeatList;
      @ 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 Person p; \old(getMessage(id)).getGroup().hasPerson(p); p.getSocialValue() ==
      @         \old(p.getSocialValue()) + \old(getMessage(id)).getSocialValue());
      @ ensures (\forall int i; 0 <= i && i < people.length && !\old(getMessage(id)).getGroup().hasPerson(people[i]);
      @          \old(people[i].getSocialValue()) == people[i].getSocialValue());
      @ ensures (\old(getMessage(id)) instanceof RedEnvelopeMessage) ==>
      @          (\exists int i; i == ((RedEnvelopeMessage)\old(getMessage(id))).getMoney()/\old(getMessage(id)).getGroup().getSize();
      @           \old(getMessage(id)).getPerson1().getMoney() ==
      @           \old(getMessage(id).getPerson1().getMoney()) - i*(\old(getMessage(id)).getGroup().getSize() - 1) &&
      @           (\forall Person p; \old(getMessage(id)).getGroup().hasPerson(p) && p != \old(getMessage(id)).getPerson1();
      @           p.getMoney() == \old(p.getMoney()) + i));
      @ ensures (\old(getMessage(id)) instanceof RedEnvelopeMessage) ==>
      @          (\forall int i; 0 <= i && i < people.length && !\old(getMessage(id)).getGroup().hasPerson(people[i]);
      @           \old(people[i].getMoney()) == people[i].getMoney());
      @ ensures (!(\old(getMessage(id)) instanceof RedEnvelopeMessage)) ==> (\not_assigned(people[*].money));
      @ ensures (\old(getMessage(id)) instanceof EmojiMessage) ==>
      @         (\exists int i; 0 <= i && i < emojiIdList.length && emojiIdList[i] == ((EmojiMessage)\old(getMessage(id))).getEmojiId();
      @          emojiHeatList[i] == \old(emojiHeatList[i]) + 1);
      @ ensures (!(\old(getMessage(id)) instanceof EmojiMessage)) ==> \not_assigned(emojiHeatList);
      @ also
      @ public exceptional_behavior
      @ signals (MessageIdNotFoundException e) !containsMessage(id);
      @ signals (RelationNotFoundException e) containsMessage(id) && getMessage(id).getType() == 0 &&
      @          !(getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()));
      @ signals (PersonIdNotFoundException e) containsMessage(id) && getMessage(id).getType() == 1 &&
      @          !(getMessage(id).getGroup().hasPerson(getMessage(id).getPerson1()));
      @*/
    public void sendMessage(int id) throws
            RelationNotFoundException, MessageIdNotFoundException, PersonIdNotFoundException;

（new一個id的問題假定可以通過指令限制下按序構造來保證ID的穩定）

心得體會

本單元感覺OO的壓力一下子就小了，感謝課程組的貼心關懷，以及“迭代開發”的體驗真不錯，yysy，在期末OS壓力起來的時候，莫名其妙每週多出了10多個小時的時間，那麼一種關愛感油然而生

相關推薦

2022年北航面向物件程式設計第三單元總結

2022年北航面向物件程式設計第三單元總結 目錄 2022年北航面向物件程式設計第三單元總結

面向物件程式設計第三單元總結

第三單元部落格作業 一、自測過程 在自測之間，我一般會反覆閱讀自己的程式碼，靜態地看一下可能的問題。

【2022春-面向物件】第三單元總結

【2022春-面向物件】第三單元總結 目錄 【2022春-面向物件】第三單元總結 寫在前面

面向物件程式設計第四單元總結

面向物件第四單元總結 一、Unit 4分析總結 ​本單元作業基於UML的模型化設計，建立了一個支援三種UML圖的解析器，並具有有效性檢查功能。這單元的第一次作業是歷次最令我無從下手的一次，整個單元的核心在於讀懂UML圖

BUAA_2022面向物件_第三單元總結

BUAA_2022面向物件_第三單元總結 O、寫在前面 正如助教所說，本單元的設計與執行，難度不大，這得益於JML的功勞；但是，對細心的要求尤其的高。如何理解、高效和全面的實現JML，是本單元的關鍵。在該單元中，我們完成

程式設計與演算法（三）C++面向物件程式設計 第三週 相關筆記

1、this指標的運用 指向當前函式作用類的指標 相當於翻譯為C語言，r.run() = run(test * this)

面向物件程式設計-第四單元部落格

OO第四單元作業總結 本單元架構設計 本單元的作業架構，是基於課程組提供的需要實現的介面進行構建的。

2022面向物件設計與構造第三單元總結

一、測試策略 本單元作業我基本的測試策略就是單元測試 + 情況覆蓋 單元測試：使用JUnit工具，對每一個類建立一個測試類，然後再在測試類內編寫各方法對應的測試方法。

2022年北航OO第三單元總結

2022年北航OO第三單元總結 單元學習概要 本單元的主要學習內容是學習 JML 規格的相關知識，並根據給出的 JML 規格實現一個社交網路的模型，該模型中包括成員、群組以及相互之間的關係和流通的訊息，並支援其中各種各

PHP面向物件程式設計（三）

PHP靜態屬性和靜態方法 靜態屬性和方法的定義與呼叫 通過static關鍵字來修飾靜態屬性和方法。由於靜態屬性和方法可以直接通過類引用，所以又被稱為類屬性和方法（相應的非靜態屬性和非靜態方法需要例項化後通過物件引

面向物件程式設計(第2天):多型性和繼承(繼承)

下載PDF article - 847 KB 介紹 在本文的第一部分中，我們瞭解了方法過載的不同場景，並做了很多有趣的操作。在本系列的第2部分，我的文章將只關注OOP中的繼承概念。讓我們用一些要點來定義繼承: 路線圖 我們仍然堅

Java面向物件程式設計-第一個Java程式

Java面向物件程式設計-第一個Java應用 2.1 建立Java原始檔 本章例子包含兩個Java原始檔：Doll.java和AppMain.java

JAVA面向物件程式設計第八章-第九章課後習題答案--------面向物件中的多型+使用異常處理

技術標籤：java學習介面eclipsejava多型 第八章 1、要使程式執行出下面結果，修改程式

面向物件程式設計的三個基本特性

Java語言的三個基本特點 Java語言是面向物件的程式語言，故有三個基本特性，即：封裝性，繼承性，多型性。這三個特點主要體現在類上，下面對這三個特性逐一進行講解。

面向物件程式設計——前三次PTA題目集總結

一、前言 (1).第一次的題目集比較簡單，具體考察對java基本格式的掌握情況，如：輸入，輸出，條件判斷，迴圈等。對於演算法的要求較低，比較容易上手，題量也比較大。

淺談JavaScript的面向物件程式設計（三）

　　前面已經對JavaScript的面向物件程式設計作了簡單的介紹，包括了物件的屬性、物件的工廠模式、建構函式和原型等。通過介紹，這些建立物件的方法依然有不少優化和改進的地方。

讀書筆記-JavaScript面向物件程式設計（三）

第7章 瀏覽器環境 7.1 在HTML頁面中引入JavaScript程式碼 7.2概述BOM與DOM（頁面以外事物物件和當前頁面物件）

面向物件設計與構造第三單元總結

作業分析 題目簡述 根據給出的 JML 規格實現並維護一個社交網路的模型，包括人、群組、網路和各種訊息，還有各種異常。

面向物件第三單元總結

面向物件第三單元總結 〇.單元總覽 本單元的主要目的是建立一個社交通訊網路，程式碼已由課程組給出，我們只需根據給出的jml規格實現介面即可，主要包括人，群組，網路和各種訊息以及各種可能會產生的異常，部分方法

面向物件設計與構造第三單元總結部落格

面向物件設計與構造第三單元總結部落格 1 作業概述 第三單元作業的主要內容是根據給出的JML規格和介面定義實現一個社交系統，主要的功能包括社交關係的模擬與查詢、群組功能、不同型別訊息的接收與傳送等。