【2022春-面向物件】第三單元總結
【2022春-面向物件】第三單元總結
目錄寫在前面
本單元的主題是JML。
JML是一種形式化的語言，用來對類和方法進行規格化的描述。初見JML時可能需要花一定時間去理解其語法，而且會發現這樣的語言理解起來十分費勁。例如一個“求圖的最短路徑”的方法可能需要幾十行的JML描述。
這就是諸如JML這類形式化語言的特點：用一種規範的語法，去嚴謹的定義一個類的規格，及其各種方法。相比於人們交流時所使用的自然語言，形式化語言更為“規範”，避免了歧義的產生。當然任何事物都有兩面性，如此“規範”的語言的代價就是理解難度高。
在初學JML時也許會感覺用JML描述規格是多此一舉：例如，為了定義一種類的“求最短路徑”方法，設計者需要把“求最短路徑”這樣的自然語言翻譯成JML，然後實現者又需要把JML語言翻譯成更易於理解的“求最短路徑”這樣的理解方式，然後再套用求最短路徑的演算法。試想一下如果設計者直接告訴實現者：“這個方法需要傳入兩個節點的編號，返回最短路徑長度。”這樣不是更方便嗎？沒錯這顯然更方便，減少了理解的難度，但是有產生歧義的風險。如果實現者的實現有問題，他可以說“是設計者沒說清楚”。但如果設計者給出的是JML，實現有問題的話，實現者就沒法找藉口了。
其實實際的工程中，JML的應用不是很廣泛，也許原因就在於太晦澀難懂了。但JML確實能在一定程度上幫助設計者明確規格，並不是一無是處。從學習的角度來說，學習JML也能更好學習面向物件的思想。設計者只關心需求，不關心具體實現，所以需要JML提出“需求”。而實現者要確保需求得以實現。
一.本單元架構
本單元聚焦於社交網路的建模及處理。
社交網路可以抽象為圖論中的圖結構：每個人是圖中的節點，人與人的關係是圖中的邊。而作業中的需求涉及到許多對圖結構的詢問：例如連通塊個數，最小生成樹等等。如果從JML本身出發也許可以不用維護圖結構，但顯然複雜度過高，作為實現者，有必要引入圖的資料結構，並維護之，以解決問題。
第一次作業
首先觀察需求：最基本的addPerson, addRelation等方法，表示增加節點，增加關係等等。大部分這樣的方法都可以直接根據JML來一板一眼的寫程式碼即可。（當然查詢操作不適用JML中陣列那樣的方式，而是採用HashMap增加效率。）
需求：連通性相關查詢
要格外關注的是isCircle queryBlockSum：查詢兩個節點是否聯通；查詢連通塊個數。如果看這兩個方法給出的JML會很有意思，似乎不是很好理解：
isCircle:
/*
@ ensures \result == (\exists Person[] array; array.length >= 2;
@ array[0].equals(getPerson(id1)) &&
@ array[array.length - 1].equals(getPerson(id2)) &&
@ (\forall int i; 0 <= i && i < array.length - 1;
@ array[i].isLinked(array[i + 1]) == true));
@*/
public /*@ pure @*/ boolean isCircle(int id1, int id2) throws PersonIdNotFoundException;
JML的意思是“存在一個Person序列，使得第一個Person的id是id1，且最後一個Person的id是id2，且相鄰兩個Person鄰接”，也就是存在一條連線兩點的路徑。
queryBlockSum:
/*@ ensures \result ==
@ (\sum int i; 0 <= i && i < people.length &&
@ (\forall int j; 0 <= j && j < i; !isCircle(people[i].getId(), people[j].getId()));
@ 1);
@*/
public /*@ pure @*/ int queryBlockSum();
JML的意思是統計所有person中“id小於它的person都不與它聯通”的person的個數。再翻譯一下，每個連通塊中只有id最小的person被計數。也就是統計了連通塊個數。
通過觀察這兩個方法的JML也能發現JML的一大特點：確實相對不利於理解。
實現：並查集
理解上述方法後，兩個方法具體該如何實現？答案是並查集。並查集可以很好的維護連通性相關的資訊。
我們可以引入新的類:DisjointSetUnion，提供的public方法：
-
void add(int):增加節點編號為id -
void merge(int, int):使兩個節點聯通 -
boolean check(int, int):查詢兩節點是否連通 -
int qbs()：查詢連通塊個數
並查集具體的實現方法網上的資料已經很多了，這裡不再贅述。我們只關心架構設計。
在Network中增加了並查集物件，在addPerson以及addRelation中對並查集維護即可。
第二次作業
我們關心新增的方法。
需求
message相關：新增message，傳送message等等。照著JML一點一點實現即可。
group相關：新增qgas,qgav等方法，查詢一個Group內的資訊。這裡需要注意下複雜度的控制，如果按照JML實現的複雜度為\(O(n^2)\),\(n\)為group中person個數。這裡恰好能說明：JML只是給出了設計者所期望的需求，具體實現以及效能的控制由實現者自行考慮。
qlc：查詢最小生成樹邊權和。
/* @ ensures \result ==
@ (\min Person[] subgroup; subgroup.length % 2 == 0 &&
@ (\forall int i; 0 <= i && i < subgroup.length / 2; subgroup[i * 2].isLinked(subgroup[i * 2 + 1])) &&
@ (\forall int i; 0 <= i && i < people.length; isCircle(id, people[i].getId()) <==>
@ (\exists int j; 0 <= j && j < subgroup.length; subgroup[j].equals(people[i]))) &&
@ (\forall int i; 0 <= i && i < people.length; isCircle(id, people[i].getId()) <==>
@ (\exists Person[] connection;
@ (\forall int j; 0 <= j && j < connection.length - 1;
@ (\exists int k; 0 <= k && k < subgroup.length / 2; subgroup[k * 2].equals(connection[j]) &&
@ subgroup[k * 2 + 1].equals(connection[j + 1])));
@ connection[0].equals(getPerson(id)) && connection[connection.length - 1].equals(people[i])));
@ (\sum int i; 0 <= i && i < subgroup.length / 2; subgroup[i * 2].queryValue(subgroup[i * 2 + 1])));
@*/
public /*@ pure @*/ int queryLeastConnection(int id) throws PersonIdNotFoundException;
這裡的JML為了定義最小生成樹，給出了一個邊集subgroup,其需要滿足條件：
- 相鄰兩個person鄰接（因為是邊集）
- 所有與查詢的id聯通的點都出現在subgroup裡
- 所有與查詢的id聯通的點都可以用subgroup裡面的邊組成一條路徑
如此便定義了最小生成樹。
實現
引入MstSolver類，提供方法：
int solve(List<MyPerson> people);
傳入person的集合（保證輸入引數是連通圖），給出最小生成樹邊權和。對於具體的演算法，本次使用了Kruscal演算法，方法內部還可以藉助上次作業的並查集物件進行維護。
第三次作業
我們關心新增的方法。
需求
此次涉及到新的三種不同的message型別。以及需要查詢最短路徑的sendIndirectMessage方法。
/*@ ensures (\exists Person[] pathM;
@ pathM.length >= 2 &&
@ pathM[0].equals(\old(getMessage(id)).getPerson1()) &&
@ pathM[pathM.length - 1].equals(\old(getMessage(id)).getPerson2()) &&
@ (\forall int i; 1 <= i && i < pathM.length; pathM[i - 1].isLinked(pathM[i]));
@ (\forall Person[] path;
@ path.length >= 2 &&
@ path[0].equals(\old(getMessage(id)).getPerson1()) &&
@ path[path.length - 1].equals(\old(getMessage(id)).getPerson2()) &&
@ (\forall int i; 1 <= i && i < path.length; path[i - 1].isLinked(path[i]));
@ (\sum int i; 1 <= i && i < path.length; path[i - 1].queryValue(path[i])) >=
@ (\sum int i; 1 <= i && i < pathM.length; pathM[i - 1].queryValue(pathM[i]))) &&
@ \result==(\sum int i; 1 <= i && i < pathM.length; pathM[i - 1].queryValue(pathM[i])));
*/
這裡給出了sendIndirectMessage方法的部分JML，此部分JML定義了最短路徑。翻譯過來的意思是：存在一個Person陣列，使得相鄰兩個person鄰接，並且相鄰Person的邊權和是所有這樣的陣列之中最小的。返回最小的邊權和。
實現
新建graph類，維護圖的資訊。方法int getShortestPath(int start, int end);提供查詢最短路徑的服務。
總結
實際上本次的三次作業實現都有圖相關的修改或者查詢等操作。並查集，最小生成樹，最短路徑，都屬於圖相關的詢問。但是在這三次作業的迭代中，這三種詢問用了三個不同的類來實現，顯得有些複雜。如果考慮重構的話，將這些圖相關的操作封裝到一個統一的類中會更好。
二.測試資料構造（利用JUnit）
眾所周知JUnit是一種用來測試的工具。它提供了一個方便進行測試的環境，利於使用者構造資料開展測試，並快速找到bug的來源。
但是歸根到底它只是一個工具，真正的測試資料的構造還需要人類的主觀能動性。
測試可以採取逐步遞進的策略：對單一類單一方法的功能性測試，和對單一類多方法間協同的測試，和對多個類的綜合性測試。
單一方法測試
對單一方法測試相對簡單。需要改變的有兩個地方：一是物件本身的狀態；二是傳入的引數。而驗證正確性則要編寫對應的物件狀態檢查函式repOk()以及每個方法的返回值檢查函式，來檢查物件本身和返回值的正確性。因為涉及到物件狀態的改變，所以測試時要優先保證一些改變物件狀態，且較為重要的方法優先測試。
（這裡的“重要”比較泛，這樣的方法的特點一般有：實現不是很複雜，使用很頻繁，等等。例如本次的addPerson addRelation等等）
對於一般的方法，其測試方式便是：儘可能利用測試好的方法改變物件狀態，在不同的狀態下傳入不同的引數進行測試。
單一類測試
對於一個類來說，測試的一個重要的事情是各方法呼叫的次序。就像學習計組時做測試，常常需要通過隨機構造指令序列，製造各種資料衝突。對於類的測試可能也需要隨機構造呼叫方法的次序。
除了隨機，也可以嘗試手造一些極限資料，往往是為了彌補隨機測試不夠全面的地方。
綜合性測試
對多個類的協同工作進行測試。對於隨機的測試策略而言，可以將隨機的範圍擴大：每個類的新建，所有類的所有方法，都需要隨機其順序。這樣的資料構造往往相對困難，因為需要保證呼叫方法的順序是合理的，因此需要斟酌隨機產生的次序。當然對於這次作業而言，可以僅僅隨機輸入的指令，這也是最為方便的方法之一，但是缺點在於容易有測試不到的地方。
總結
上述三種測試方法的範圍從小到大。在測試時間一定的情況下，範圍越大，相對來講對每一個類或方法而言的測試強度則會減弱。至於優先做哪種測試還要具體問題具體分析，如果規模不大可以直接做綜合性測試，如果規模較大最好先對單一類或方法進行測試。此外對於一些容易出問題的類或方法，複雜程度很高的類或方法，最好要進行額外的單一的針對性測試。
三.程式碼修復及效能分析
bug修復
本單元的作業相對而言難度不大，bug僅在第一次測試中出現過，原因是沒有實現“異常中的兩個傳入的id相同時，只統計一次異常”。這說明測試是基於需求的。如果需求有所遺漏，那麼測試時自然不會考慮到這樣的需求，從而導致檢測不出這樣的錯誤。也就是說，無論是程式碼實現還是測試，明確需求總是第一位的。
效能分析
本單元作業涉及到的各個查詢需要進行復雜度的控制。需要儘可能保證每個輸入的指令，執行的最壞複雜度不能到達\(O(n^2)\)量級，否則不能在規定時間內執行完畢。
-
int queryGroupValueSum(int id)：查詢一組person之間的所有邊權和。解決方案：在Group類中新建成員變數valueSum，每次增加組內成員時，以及每次增加邊時，更新valueSum，在查詢時直接輸出此變數值。複雜度變為\(O(1)\). -
int queryGroupAgeVar(int id)：查詢組內年齡方差。若完全按JML實現複雜度為\(O(n^2)\).解決方案：只調用一次getAgeMean()獲取平均值再計算。複雜度\(O(n)\). -
boolean isCircle(int id1, int id2):查詢是否聯通。通過維護並查集即可。採取路徑壓縮的並查集優化後，複雜度約為常數級別。 -
int queryBlockSum()：查詢連通塊個數。在並查集物件中維護此值即可：每次新增節點，連通塊個數+1；每次合併兩個不連通的節點，連通塊個數-1。複雜度為\(O(1)\)。 -
int queryLeastConnection(int id)：查詢最小生成樹。採用Kruscal演算法加並查集維護。複雜度\(O(E\times logE)\),\(E\)為邊的個數。 -
int sendIndirectMessage(int id):查詢最短路徑。採用堆優化的Dijkstra演算法的複雜度為\(O(n\times logn)\)。
四.對Network進行擴充套件
假設出現了幾種不同的Person
- Advertiser：持續向外傳送產品廣告
- Producer：產品生產商，通過Advertiser來銷售產品
- Customer：消費者，會關注廣告並選擇和自己偏好匹配的產品來購買
-- 所謂購買，就是直接通過Advertiser給相應Producer發一個購買訊息- Person：吃瓜群眾，不發廣告，不買東西，不賣東西
如此Network可以支援市場營銷，並能查詢某種商品的銷售額和銷售路徑等
需求分析
我們先從需求的角度出發，對於一個需要支援市場營銷的NetWork來說，可能會存在哪些需求。
-
對消費者：查詢收到的所有廣告列表；從某個Advertiser購買某件商品。
-
對生產商：新建某個商品；查詢某商品的銷售額，庫存等；
-
對Advertiser：新建和傳送某個廣告（藉助addMessage，sendMessage）；查詢某個廣告有多少消費者通過此廣告購買了產品（通過這種查詢瞭解廣告的效果）；
介面設計
- 新建Item類，表示商品。屬性有ID號與價格。支援ID查詢，價格的查詢與修改。
public interface Item {
/*@ public instance model int id;
@ public instance model int price;
@*/
public void setPrice();
public /*@ pure @*/ int getPrice();
public /*@ pure @*/ int getId();
}
- 新建訊息類，繼承自Message。Advertisement類是Advertiser傳送給Customer的訊息。作為Customer可以查詢所有收到的廣告，可以依據某個廣告購買。
public interface Advertisement extends Message {
//@ public instance non_null Item item;
//@ public invariant socialValue == item.getPrice();
}
-
新建各種不同類別的
Person：Customer，Advertisor，Producer -
新增異常
InvalidPersonTypeException：只有特定型別的person能使用特定的方法。 -
其他：在Person中新增相應查詢方法，等等。
方法設計
關於Network，新增模型Item[] items.
public interface 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;
@ public instance model non_null Item[] items;
@*/
}
- 查詢Customer的所有廣告
/*@ public normal_behavior
@ requires contains(id) && (getPerson(id) instance of Customer);
@ ensures \result == ((Customer) getPerson(id)).getReceivedAdvertisements();
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(id);
@ public exceptional_behavior
@ signals (InvalidPersonTypeException e) contains(id) && !(getPerson(id) instance of Customer);
@*/
public /*@ pure @*/ List<Advertisement> queryReceivedAdvertisements(int id) throws PersonIdNotFoundException, InvalidPersonTypeException;
-
購買某件商品,個數為count（通過某條廣告）
前置條件：對應person存在，且為Customer型別,且存在此Message。
/*@ public normal_behavior
@ requires contains(personId) && (getPerson(id) instance of Customer) && !(((Customer) getPerson(id)).haveAdvertisement(advertisementId));
@ assinable people;
@ ensures getPerson(id).getMoney() == \old(getPerson(id).getMoney) - getMessage(advertisementId).getItem().getPrice();
@ 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 && \old(people[i].getId()) != personId; \not_assigned(people[i]));
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(personId);
@ public exceptional_behavior
@ signals (InvalidPersonTypeException e) contains(personId) && !(getPerson(id) instance of Customer);
@ public exceptional_behavior
@ signals (MessageNotFoundException e) contains(personId) && (getPerson(id) instance of Customer) && !(((Customer) getPerson(id)).haveAdvertisement(advertisementId));
@*/
public void buy(int personId, int advertisementId， int count) throws PersonIdNotFoundException, InvalidPersonTypeException, MessageNotFoundException;
- 新建某個商品（在對應生產商處註冊商品）
/*@ public normal_behavior
@ requires contains(personId) && (getPerson(id) instance of Producer)
@ assinable people;
@ ensures ((Producer) getPerson(producerId)).containsItem(item.getId());
@ ensures ((Producer) getPerson(producerId)).getItemCount(item.getId()) == 0;
@ ensures \forall(int i = 0; 0 <= i && i < items.length; \old(((Producer)getPerson(producerId)).containsItem(item.getId())) ==>((Producer)getPerson(producerId)).containsItem(item.getId()));
@ ensures ((Producer)getPerson(producerId)).itemCount()) == \old(((Producer)getPerson(producerId)).itemCount())) + 1;
@ 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 && \old(people[i].getId()) != personId; \not_assigned(people[i]));
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(personId);
@ public exceptional_behavior
@ signals (InvalidPersonTypeException e) contains(personId) && !(getPerson(id) instance of Producer);
@*/
public void addNewItem(int producerId, Item item) throws PersonNotFoundException,InvalidPersonTypeException;
- 生產某件商品,個數為count。
public void produceItem(int itemId, int count) throws ItemNotFoundException,InvalidPersonTypeException;
- 查詢商品銷售額
public int queryItemValue(int itemId) throws ItemNotFoundException,InvalidPersonTypeException;
- 查詢庫存
public int queryItemCount(int itemId) throws ItemNotFoundException,InvalidPersonTypeException;
- 查詢某個廣告有多少消費者通過此廣告購買了產品
public int queryAdvertisementValue(int messageId) throws MessageIdNotFoundException, InvalidPersonTypeException;
五.學習體會
JML因其形式化的特點，可以對需求進行規範化設計，但因此複雜程度有所增高。儘管工程上可能用不上JML，但是利用此方法有利於進行面向物件思想的學習。這單元的難度在於對這種語言以及面向物件思想的理解，並不在於程式碼實現。在以後的學習中不管用不用JML，都要時刻記住要明確需求，嚴格在滿足需求的情況下給出相應實現。
最後衷心感謝老師助教同學在學習之路上的幫助。