面向物件設計與構造2022第三單元總結-有解無憂

一、分析在本單元自測程序中如何利用JML規格來準備測驗資料

我在本單元的自測中主要采取了兩種測驗方法：普遍測驗和專項測驗，

所謂普遍測驗就是資料生成器生成的資料包含作業指導書給出的所有指令，進行覆寫檢查，但是每種指令的測驗不一定是邊界、極端情形，

而專項測驗就是基于JML規格，針對那些程序復雜、容易寫錯和出現性能問題的指令生成特殊資料來測驗，接下來舉幾個例子來說明，

首先是qgvs指令，從圖論的角度來說其實就是維護一個群組里面人員所有邊權和的兩倍，我們來看JML是如何描述的

//in Network.java
/*@ public normal_behavior
      @ requires (\exists int i; 0 <= i && i < groups.length; groups[i].getId() == id);
      @ ensures \result == getGroup(id).getValueSum();
      @ also
      @ public exceptional_behavior
      @ signals (GroupIdNotFoundException e) !(\exists int i; 0 <= i && i < groups.length;
      @          groups[i].getId() == id);
      @*/
public /*@ pure @*/ int queryGroupValueSum(int id) throws GroupIdNotFoundException;

//in Group.java
/*@ ensures \result == (\sum int i; 0 <= i && i < people.length; 
      @          (\sum int j; 0 <= j && j < people.length && 
      @           people[i].isLinked(people[j]); people[i].queryValue(people[j])));
      @*/
public /*@ pure @*/ int getValueSum();

所以直接從JML看，復雜度是\(O(指令數*組內人數^2)\)的

但其實從構造資料的角度我還需要關注的是

/*@ public normal_behavior
	  @ ...(省略)
      @ also
      @ public normal_behavior
      @ requires (\exists int i; 0 <= i && i < groups.length; groups[i].getId() == id2) &&
      @           (\exists int i; 0 <= i && i < people.length; people[i].getId() == id1) &&
      @            getGroup(id2).hasPerson(getPerson(id1)) == false && 
      @             getGroup(id2).people.length >= 1111;
      @ assignable \nothing;
      @ also
      @ public exceptional_behavior
      @ ...(省略)
      @*/
    public void addToGroup(int id1, int id2) throws GroupIdNotFoundException,
            PersonIdNotFoundException, EqualPersonIdException;

其實這個方法的JML就約束好了每個群組的人數不得超過1111個人，

因此可以構造人數達到上限的資料來檢驗時間復雜度是否合法，該部分的構造代碼如下

#include <bits/stdc++.h>
using namespace std;
mt19937 rng(time(0));
int main()
{
    freopen("testcase1.txt","w",stdout);
    for(int i=1;i<=1111;i++)
    {
        printf("ap %d AAJ %d\n",i,rng()%200);
    }
    printf("ag 114514\n");
    for(int i=1;i<=1111;i++)
    {
        printf("atg %d 114514\n",i);
    }
    for(int i=1;i<=2777;i++)
        printf("qgvs 114514\n");
    return 0;
}

然后，是qlc指令，我們來看一下它的JML，

    /*@ public normal_behavior
      @ requires contains(id);
      @ 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])));
      @ also
      @ public exceptional_behavior
      @ signals (PersonIdNotFoundException e) !contains(id);
      @*/
    public /*@ pure @*/ int queryLeastConnection(int id) throws PersonIdNotFoundException;

正如老師在總結課上所言，其實這種最優化的描述是不太直觀的，不過在閱讀qlc的JML之前我們已經在測驗環節中讀過一個求邊集的JML，所以有了經驗，這里說白了就是要求id這個人所在連通塊的最小生成樹大小，

從構造資料角度，要檢驗最小生成樹求解的效率和正確性，就是盡可能得讓這個連通塊的邊數要多，而且權值要隨機多樣，構造代碼如下

for(int i=1;i<=1111;i++)
{
     printf("ap %d AAJ %d\n",i,rng()%200);
}
printf("ag 114514\n");
for(int i=1;i<=1111;i++)
{
	printf("atg %d 114514\n",i);
}
for(int i=1;i<=1110;i++)
	printf("ar %d %d %d\n",i,i+1,rng()%1000);
for(int i=1;i<=1109;i++)
	printf("ar %d %d %d\n",i,i+2,rng()%1000);
for(int i=1;i<=538;i++)
	printf("ar %d %d %d\n",rng()%1111+1,rng()%1111+1,rng()%1000);
for(int i=1;i<=20;i++)
	printf("qlc %d\n",rng()%1111+1);

第三，是sim指令，JML太長就略去了，說白了就是除了發送資訊外要求出從發送者到接收者的最短路，考慮到樸素的Dijkstra的復雜度是\(O(n^2)\)，而堆優化的Dijkstra復雜度為\(O(m \log n)\)，所以從構造資料角度，人數要達到\(10^3\)量級，同時資訊數量與\(sim\)指令數一致達到上限，再加上邊權隨機性，就可以檢測實作的正確性和效率了，

for i in range(0, 1111):
    print("ap %d Jack%d %d" % (i, i, 20), file=file_out)
for i in range(0, 2889):
    print(
        "ar %d %d %d"
        % (random.randint(0, 1111), random.randint(0, 1111), random.randint(0, 1000)),
        file=file_out,
    )
for i in range(0, 500):
    print(
        "am %d %d 0 %d %d"
        % (
            i,
            random.randint(-1000, 1000),
            random.randint(0, 1111),
            random.randint(0, 1111),
        ),
        file=file_out,
    )
for i in range(0, 500):
    print("sim %d" % (i), file=file_out)

第四，是dce指令，如果說前面的三種指令可能構造更多著眼于性能考慮，那么dce指令的測驗就旨在檢查正確性，

通過閱讀JML，其實這條指令需要做兩件事

將已經保存的表情中，熱度小于\(limit\)的刪掉

@ ensures (\forall int i; 0 <= i && i < \old(emojiIdList.length);
      @          (\old(emojiHeatList[i] >= limit) ==>
      @          (\exists int j; 0 <= j && j < emojiIdList.length; emojiIdList[j] == \old(emojiIdList[i]))));

把所有資訊里面，只保留非表情資訊，和所含表情沒有在第一步刪掉的表情資訊

 @ ensures (\forall int i; 0 <= i && i < \old(messages.length);
      @          (\old(messages[i]) instanceof EmojiMessage &&
      @           containsEmojiId(\old(((EmojiMessage)messages[i]).getEmojiId()))  ==>
      @           (\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i])))));

所以從構造資料來說，一方面人數要少，但是資訊量要大，這樣才能讓每種表情的熱度盡量高，另一方面可以讓\(limit\)遞減來進行dce.故構造代碼如下

for i in range(0, 10):
    print("ap %d Jack%d %d" % (i, i, 20), file=file_out)
for i in range(0, 10):
    for j in range(1, 10 - i):
        print("ar %d %d %d" % (i, i + j, random.randint(0, 1000)), file=file_out )
for i in range(0, 20):
    print(
        "sei %d" % (i),
        file=file_out,
    )
for i in range(0, 1000):
    print(
        "aem %d %d 0 %d %d"
        % (i, random.randint(0, 19), random.randint(0, 9), random.randint(0, 9)),
        file=file_out,
    )
for i in range(0, 1000):
    print("sm %d" % (i), file=file_out)
for i in range(0, 50):
    print("dce %d" % (i), file=file_out)
    for j in range(0, 20):
        print("qp %d" % (j), file=file_out)

第五，是群發紅包問題，這個地方我也差點寫錯了，關鍵處的JML就是這一句

@ 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));

發送的總錢數按照群組總人數均分，但是這個除法和Java運算子一致——是整除，所以會出現\(getMoney()\not=i*getSize()\)的情況
發送者扣錢但不扣“自己的那一份”，同樣的，發錢也不發“自己的那一份”

但是在具體實作上，我是把這個\(i\)傳到群組里，在群組里實作了一個方法，就是給所有人發錢\(i\)元，這就導致這條資訊的發送者多得了一份錢，

這個問題是我在截止日那天上午才發現的，之所以大量的普遍測驗沒有觸發這個bug，原因就是紅包的錢數最多200，而普遍測驗中往往給一個組塞了一千多號人，結果按照整除規則，其他人一分錢沒得，發送者也根本沒有發出去錢，

因此在專項測驗中，人數一定要少，而且每發送一條訊息，必須要檢查發送者的錢數，再隨機抽查兩個人的錢數，這樣就能較為充分地檢查行為的正確性了，構造代碼如下

for i in range(0, 10):
    print("ap %d Jack%d %d" % (i, i, 20), file=file_out)
print("ag 114514", file=file_out)
for i in range(0, 10):
    print("atg %d 114514" % (i), file=file_out)
send_people = []
for i in range(0,990):
    sender = random.randint(0, 9)
    send_people.append(sender)
    print(
        "arem %d %d 1 %d 114514" % (i, random.randint(0, 200), sender),
        file=file_out,
    )
for i in range(0, 990):
    print("sm %d" % (i), file=file_out)
    print("qm %d" % (send_people[i]), file=file_out)
    for j in range(0, 2):
        print("qm %d" % (random.randint(0, 9)), file=file_out)

二、梳理本單元的架構設計，分析自己的圖模型構建和維護策略

首先還是放一張第三次作業時的UML圖

? 由圖片可知，其實主體框架根據JML基本上已經確定了，自主實作的部分主要是圖模型和一些輔助的方法上，

? 首先來說圖模型，在求qci和qlc指令時維護了并查集，體現在UML圖上就是MyNetwork里面的pp、ppqlc和sizeqlc三個HashMap，和ffind、ffindQlc和unionQlc三個方法，其中pp和ffind主要是用并查集維護圖的連通性，便于qci指令中回答兩個人是否連通，而ppqlc、sizeqlc和剩下兩個方法，其實是在用Kruskal演算法求最小生成樹中維護并查集的，為了避免混淆，所以單獨又實作了一下，當然，用于qci的并查集簡單采用路徑壓縮，而在Kruskal演算法中的并查集是路徑壓縮+按秩合并的，以盡可能提高效率，

? 為了方便Kruskal演算法，新建了一個MyEdge類，可以存盤一條邊的兩個節點和邊權，并實作了Comparable介面，使得其可以排序.

? 那么到了sim指令需要寫堆優化的Dijkstra演算法時，需要維護一個無向圖，鄰接表的出現就很有必要了，于是在MyNetwork中有了一個private HashMap<Integer, HashMap<Integer, Integer>> vec;來存起點、終點和這條邊的權值（本單元根據JML規格不會出現重邊，所以這么維護倒也無妨），那么在實作Dijkstra中，使用優先佇列PriorityQueue來選取當前起點所到達的各個點中路徑長度最小的一個點，這里也新建了一個Item類來方便PriorityQueue的操作，

? 還有一處圖模型，就是qgvs需要知道一個群組里所有連邊的權值和*2.不過這里僅僅需要一個數值，并不需要實際維護里面的圖結構，需要注意的就是在人員剛剛加入群組的時候，對群組權值和貢獻，人員退出的時候，減去貢獻，特殊的情形就是兩個人可能之前已經屬于一個（或多個）群組，但還沒有建立關系，這個時候addRelation需要考慮到對所有共同加入的群組進行貢獻，

三、按照作業分析代碼實作出現的性能問題和修復情況

? 由于在設計階段充分考慮了各種指令的最壞時間復雜度，并且在自測階段測驗較為充分，故最終提交的作業里沒有出現性能問題，

四、請針對下頁ppt內容對Network進行擴展，并給出相應的JML規格

? 假設出現了幾種不同的Person

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

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

首先，針對廣告和訂購兩種訊息新建介面

廣告訊息：繼承自Message介面，且要求type=2，（僅初始化Person1）JML如下

public interface AdMessage extends Message{
    /*@
      @ public instance model int productId;
      @ public instance model int price;
      @*/
    
    //@ public invariant socialValue =https://www.cnblogs.com/LaiAng80686/p/= price;
    
    //@ ensures /result == productId; 
    public /*@ pure @*/ int getProductId();
    
    //@ ensures /result == price;
    public /*@ pure @*/ int getPrice();
}

訂購訊息：繼承自Message介面，且要求type=3（初始化Person1和Person2），JML如下

public interface PurchaseMessage extends Message{
    /*@
      @ public instance model int productId;
      @ public instance model int quantity;
      @ public instance model int producerId;
      @*/
    
    //public invariant socialValue =https://www.cnblogs.com/LaiAng80686/p/= quantity;
    
    //@ ensures /result == productId;
    public /*@ pure @*/ int getProductId();
    
    //@ ensures /result == quantity;
    public /*@ pure @*/ int getQuantity();
    
    //@ ensures /result == producerId;
    public /*@ pure @*/ int getProducerId();
}

然后考慮除Person以外的三類人員，新建介面

public interface Advertiser extends Person{
   	/*@ 
   	  @ public instance model Producer[] producers; //所經銷的生產廠家
   	  @ public instance model int[] products;//所經銷的產品號
   	  @*/
    
    // ensures \result == (\exists int i; 0 <= i && i < producers.length(); producers[i].getId() == id);
   	public /*@ pure @*/ boolean containsProducer(int id);
    
    // ensures \result == (\exists int i; 0 <= i && i< products.length(); products[i] == id);
    public /*@ pure @*/ boolean containsProduct(int id);
    
}
public interface Producer extends Person{
    /*@
      @ public instance model Advertiser[] advertisers;  //經銷商
      @ public instance model int[] products;//所生產的產品號
      @*/
    // ensures \result == (\exists int i; 0 <=i && i < advertisers.length(); advertisers[i].getId() == id);
    public /*@ pure @*/ boolean containsAdvertiser(int id);
    
    // ensures \result == (\exists int i; 0 <= u && i< products.length(); products[i] == id);
    public /*@ pure @*/ boolean containsProduct(int id);
}
putlic interface Customer extends Person{
}

然后在Network中新增四個方法

發送廣告：考慮Advertiser也屬于普通用戶（繼承自Person），而并非微店，所以實際微信中更類似于“朋友圈營銷”的廣告方式，因此這里限定TA只能向有好友(isLinked)的Customer和吃瓜群眾發送廣告，
發送訂單
查詢某種商品的銷售額
查詢某種商品的銷售路徑：輸出為一個四元組的串列，每一個四元組為（生產者、經銷商、消費者、數量）

//四元組,這里就不用JML了
public class Item{
    private Person producer;
    private Person advertiser;
    private Person customer;
    private int quantity;
    private int productId;
    public Item(Person producer, Person advertiser, Person customer, int quantity, int productId)
    {
        this.producer = producer;
        this.advertiser = advertiser;
        this.customer = customer;
        this.quantity = quantity;
        hits.productId = productId;
    }
    public int getId()
    {
        return productId;
    }
}

方法的JML

public interface Network
{
    //省略已有的public instance model
    
    /*@ public instance model non_null Item[] paths;
        public instance model non_null int[] productSoldout;
      @*/
    
   //省略已有的方法
    
    /*@ public normal_behavior
      @ requires containsMessage(id) && (getMessage(id) instanceof AdMessage）&&(getMessage(id).getType==2) && (getMessage(id).getPerson1() instanceof Advertiser)
      @ assignable getMessage(id).getPerson1().socialValue
      @ assignable people[*].socialValue, people[*].messages
      @ ensures \old(getMessage(id)).getPerson1().getSocialValue() ==
      @ \old(getMessage(id).getPerson1().getSocialValue()) + \old(getMessage(id)).getSocialValue()
      @ ensures (\forall int i; 0 <= i && i < \old(people).length() && \old(people[i]).isLinked(getMessage(id).getPerson1()) && !(\old(people[i]) instanceof Advertiser) && !(\old(people[i]) instanceof Producer); \old(people[i]).getSocialValue() == \old(people[i].getSocialValue()) + \old(getMessage(id)).getSocialValue();
      @ ensures (\forall int i; 0 <=i && i < \old(people).length() && \old(people[i]).isLinked(getMessage(id).getPerson1()) && !(\old(people[i]) instanceof Advertiser) && !(\old(people[i]) instanceof Producer); 
      (\forall int j; 0 <= j && j < \old(people[i].getMessages().size()); \old(people[i]).getMessages().get(i+1) = \old(people[i].getMessages().get(i))));
      @ ensures (\forall int i; 0 <=i && i < \old(people).length() && \old(people[i]).isLinked(getMessage(id).getPerson1()) && !(\old(people[i]) instanceof Advertiser) && !(\old(people[i]) instanceof Producer); \old(people[i]).getMessages().get(0).equals(\old(getMessage(id)));
      @ also
      @ public exceptional_behavior
      @ signals (MessageIdNotFoundException e) !containsMessage(id);
      @ signals (InvalidMessageTypeException e) containsMessage(id) && (!(getMessage(id) instanceof AdMessage) || ((getMessage(id) instanceof AdMessage) && getMessage(id).getType!=2));
      @ signals (InvalidPersonTypeException e) containsMessage(id) && (getMessage(id) instanceof AdMessage) && (getMessage(id).getType==2) && !(getMessage(id).getPerson1() instanceof Advertiser)
      @*/
    public void sendAdMessage(int id) throws MessageIdNotFoundException, InvalidMessageTypeException, InvalidPersonTypeException;
    
    /*@ public normal_behavior
      @ requires containsMessage(id) && (getMessage(id) instanceof AdMessage) && (getMessage(id).getType==3) && ((getMessage(id).getPerson1() instanceof Customer) && (getMessage(id).getPerson2() instanceof Advertiser) && (getPerson(getMessage(id).getProducerId()) instanceof Producer)) && (((Advertiser)getMessage(id).getPerson2()).containsProduct(getMessage(id).getProductId()));
      @ assignable getMessage(id).getPerson2().messages, paths, productSoldout;
      @ 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(getMessage(id));
      @ ensures \old(getMessage(id).getPerson2()).getMessages().size() == \old(getMessage(id).getPerson2().getMessages().size()) + 1;
      @ ensures productSoldout[((PurchaseMessage)getMessage(id)).getProductId()] == \old(productSoldout[((PurchaseMessage)getMessage(id)).getProductId()]) + ((PurchaseMessage)getMessage(id)).getQuantity();
      @ ensures (\exist int i; 0 <= i && i < paths.length(); paths[i].equals(new Item(getPerson(((PurchaseMessage)getMessage(id)).getProducerId(), getMessage().getPerson2(), getMessage().getPerson1(), ((PurchaseMessage)getMessage(id)).getQuantity(), ((PurchaseMessage)getMessage(id)).getProductId());
      @ also
      @ public exceptional_behavior
      @ signals (MessageIdNotFoundException e) !containsMessage(id);
      @ signals (InvalidMessageTypeException e) containsMessage(id) && (!(getMessage(id) instanceof PurchaseMessage) || ((getMessage(id) instanceof PurchaseMessage) && getMessage(id).getType!=2));
      @ signals (InvalidPersonTypeException e) containsMessage(id) && (getMessage(id) instanceof AdMessage) && (getMessage(id).getType==3) && (!(getMessage(id).getPerson1() instanceof Customer) || !(getMessage(id).getPerson2() instanceof Advertiser) || (!getPerson(getMessage(id).getProducerId()) instanceof Producer));
      @ signals (ProductIdNotFoundException e) containsMessage(id) && (getMessage(id) instanceof AdMessage) && (getMessage(id).getType==3) && ((getMessage(id).getPerson1() instanceof Customer) && (getMessage(id).getPerson2() instanceof Advertiser) && (getPerson(getMessage(id).getProducerId()) instanceof Producer)) && !(((Advertiser)getMessage(id).getPerson2()).containsProduct(getMessage(id).getProductId()));
      @*/
    public void sendPurchaseMessage(int id) throws MessageIdNotFoundException, InvalidMessageTypeException, InvalidPersonTypeException, ProductIdNotFoundException;

    /*@ public normal_behavior
	  @ ensures \result == productSoldout[id];
      @*/
    public /*@ pure @*/ int getSaledata(int id);
    
    /*@ public normal_behavior
      @ ensures (\forall int i; 0 <=i && i < paths.length() && paths[i].getId() == id;
      	\result.contains(paths[i]));
      @*/
    public List<Item> getSalePath(int id);
}

五、本單元學習體會

? 這個單元相比于前兩個單元的設計和編碼作業量確實小了不少，不過初次接觸JML規格的時候，會有一種“帶著鐐銬跳舞”的感覺——首先JML給出的各種約束和限制是必須要滿足的，在滿足的基礎上，還要去思考如何提高效率，比如選擇怎么樣的容器，選擇怎么樣的演算法，

? 最為重要的是，這個單元的測驗與前面兩個單元的很大不同在于所謂的“題目資料限制”可謂是“無處不在”，因為任何一處JML陳述句都不能忽視，一方面可以用Junit工具來顯式地驗證一些前置后置條件的滿足情況，另一方面對于撰寫資料生成器進行大量測驗而言，能不能擊中缺陷其實是很大的問題，典型的例子就是上面提到了，即便做了大量的普遍測驗（比如上萬組），但是因為普遍資料生成器構造的不足，觸發不了bug，那么某種程度上自測就白測了，

? 因此，我覺得黑盒白盒測驗（包括代碼通讀）都要認真做，不可偏廢，尤其是現在還沒有自動根據JML生成Junit測驗的情況下，即便是撰寫資料生成器，也還是基于人工對JML的語意理解，如果對JML語意理解有偏差，那么就談不上測驗的有效性，

轉載請註明出處，本文鏈接：https://www.uj5u.com/houduan/485584.html

標籤：Java

上一篇：IOS – OpenGL ES 影像漩渦 GPUImageSwirlFilter

下一篇：Java 執行緒創建與常用方法