第三單元的任務是通過理解JML規格在面向物件設計與構造中的重要意義，並掌握利用JML規規格，實現一個社交網路圖，並進一步實現最小生成樹和最小路徑演算法。

一、利用JML規格準備測試資料

1. 資料準備

　　根據功能行為的不同，我準備測試的資料分為normal_behavior類的正常資料和導致異常行為exceptional_behavior的資料。對於正常資料，具體可以根據指導書的輸入要求來進行資料的生成；對於異常資料，則根據官方包的JML原始碼的要求進行初始化。

2. 使用Junit對程式碼進行測試

　　本單元，通過初步學習瞭解Junit的使用，使用其對程式碼進行了單元測試，對於作業中的演算法相關指令bug的發現發揮了很大的作用。

二、架構設計

　　本單元我們是按照JML規格來實現介面，每次程式碼是在前一次的基礎上逐漸增加，架構大體相同，故在此展示的是第三次作業中實現的類和彼此間的聯絡：

三、效能問題和修復情況

1. 效能問題

　　第一次作業的qbs操作(query_block_sum)相對其他操作比較耗時。如果通過二重迴圈和qci操作(query_circle)，且qci操作通過廣度/深度優先搜尋實現，會導致較高的時間複雜度。故我們可以使用並查集提高效能。

　　第二次作業中需要我們實現最小生成樹。對於一個連通圖GG，其生成樹是一個極小的連通子圖，它需要包括圖中全部的nn個頂點以及構成一棵樹的n-1n−1條邊。而在一個帶權圖中，我們稱圖中邊權值和最小的生成樹為最小生成樹。可採用的演算法為Prim演算法和Kruskal演算法來提高效能。

　　第三次作業需要實現最短路徑，我們可以使用基於堆優化的 dijsktra 演算法進行效能的優化。

2. bug分析

　　本單元由於已經有了官方給出的JML，相比前兩個單元，思路上並不容易出錯，只需要根據要求進行程式碼的編寫即可。同時，我們可以使用Junit工具進行單元測試。

四、擴充套件Network

Network新增四個方法：addAdvertiseMessage，sendAdvertiseMessage，addSaleMessage，sendSaleMessage。

/*@ public normal_behavior
      @ requires !(\exists int i; 0 <= i && i < messages.length; messages[i].equals(message)) &&
      @            (message.getType() == 0) ==> (message.getPerson1() != message.getPerson2()) &&
      @             (message instanceof AdvertiseMessage);
      @ 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 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()) &&
      @             !(message instanceof AdvertiseMessage);
      @ assignable nothing;
      @ also
      @ public exceptional_behavior
      @ signals (EqualMessageIdException e) (\exists int i; 0 <= i && i < messages.length;
      @                                     messages[i].equals(message));
      @*/
    public void addAdvertiseMessage(Message message) throws EqualMessageIdException;

/*@ public normal_behavior
      @ requires !(\exists int i; 0 <= i && i < messages.length; messages[i].equals(message)) &&
      @            (message.getType() == 0) ==> (message.getPerson1() != message.getPerson2()) &&
      @             (message instanceof SaleMessage);
      @ 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 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()) &&
      @             !(message instanceof SaleMessage);
      @ assignable nothing;
      @ also
      @ public exceptional_behavior
      @ signals (EqualMessageIdException e) (\exists int i; 0 <= i && i < messages.length;
      @                                     messages[i].equals(message));
      @*/
    public void addSaleMessage(Message message) throws EqualMessageIdException;

/*@ public normal_behavior
  　　@ requires containsMessage(id) && getMessage(id).getType() == 2 &&
  　　@          getMessage(id).getPerson1() != getMessage(id).getPerson2() &&
　　  @          getMessage(id).getPerson1() instanceof Advertiser &&
　　  @          getMessage(id).getPerson2() instanceof Customer &&
  　　@          ((Customer) getMessage(id).getPerson1()).getPreference == prefertype;
  　　@ assignable messages;
  　　@ assignable getMessage(id).getPerson2().messages;
  　　@ 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 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 exceptional_behavior
  　　@ signals (MessageIdNotFoundException e) !containsMessage(id);
  　　@*/
　　public void sendAdvertiseMessage(int id) throws MessageIdNotFoundException;

/*@ public normal_behavior
  　　@ requires containsMessage(id) && getMessage(id).getType() == 3 &&
　　  @ 　　　　  getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()) &&
　　  @ 　　　　  getMessage(id).getPerson1() instanceof Advertiser &&
　　  @          getMessage(id).getPerson2() instanceof Producer &&
  　　@          getMessage(id).getPerson1() != getMessage(id).getPerson2();
  　　@ assignable messages;
  　　@ assignable getMessage(id).getPerson2().messages;
  　　@ 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 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 exceptional_behavior
  　　@ signals (MessageIdNotFoundException e) !containsMessage(id);
　　  @ signals (RelationNotFoundException e) containsMessage(id) && getMessage(id).getType() == 3 &&
　　  @          !(getMessage(id).getPerson1().isLinked(getMessage(id).getPerson2()));
  　　@*/
　　public void sendSaleMessage(int id) throws RelationNotFoundException, MessageIdNotFoundException;

五、本單元學習體會

　　第三單元主要是按照規格實現介面，認真閱讀JML十分重要，不能放過任何一個細節，另外，還要要結合課程組給出的資料範圍以及標程複雜度從全域性出發考量方法實現的複雜度。通過本單元的學習，我對於OO的理解更加深入了。