OO Unit3 Blog

測試資料準備

首先是對相關jml的理解和解讀，這一部分首先自己通讀jml規格然後根據自己的理解寫出程式碼。對於一些較為複雜的jml規格，與同學交流具體對應實現內容。

對於jml中的規格測試主要是對函式特殊邊界情況的測試以及對大量資料的時間複雜度測試。

第三單元設計分析

第一次作業

第一次作業中主要的實現難點是並查集以及qbs指令的複雜度問題。其中並查集的相關實現較為簡單，而對於qbs指令複雜度的問題，若使用傳統的雙重迴圈就會超時，較為巧妙的設計也是評論區中提到的設計方法就是使用一個常量times來儲存這個值，找到引起times變化的兩個條件並相應的變化就可正確得到相應值。

第二次作業

第二次作業中主要需要解決的是最小生成樹演算法問題。我使用的是kruskal演算法，每次新增一條邊對應的節點後迴圈找到需要新增的person，並新增到對應的set中，具體實現如下：

        while (peoples.size() != totalPeople.size()) {
            for (Person per : ((MyPerson)nowPer).getAcquaintances().keySet()) {
                if (!peoples.contains(per)) {
                    RelationSet relat = new RelationSet(nowPer.queryValue(per), per, nowPer);
                    relats.add(relat);
                }
            }
            relats.sort(new Comparator<RelationSet>() {
                @Override
                public int compare(RelationSet o1, RelationSet o2) {
                    if (o1.getValues() > o2.getValues()) {
                        return 1;
                    }
                    else if (o1.getValues() == o2.getValues()) {
                        return 0;
                    }
                    return -1;
                }
            });
            for (RelationSet relat : relats) {
                if (peoples.contains(relat.getPer1()) && peoples.contains(relat.getPer2())) {
                    continue;
                }
                if (peoples.contains(relat.getPer1())) {
                    peoples.add(relat.getPer2());
                    nowPer = relat.getPer2();
                    totalCount += relat.getValues();
                    break;
                }
                else {
                    peoples.add(relat.getPer1());
                    nowPer = relat.getPer1();
                    totalCount += relat.getValues();
                    break;
                }
            }
        }
 

需要注意的還是要保證實現的正確性。

第三次作業

這次主要實現的是最短路徑演算法，我採用dijkstra演算法，但是在實現時只使用小資料測試程式沒用使用大資料測試，導致一個地方少寫了一個字母沒有發現，在大資料測試時讀取到NULL資料(悲)，還是課下要多做測試。。對於堆優化部分可使用Java自帶的優先佇列實現對堆頂元素的讀取，但是在刪除堆頂元素後需要注意這個堆不會自動進行更新，這需要手動破壞當前狀態使其更新堆頂元素。具體實現如下：

        PriorityQueue<Person> perPriQue = new PriorityQueue<>(new Comparator<Person>() {
            @Override
            public int compare(Person o1, Person o2) {
                return Integer.compare(((MyPerson) o1).getLeastLength(),
                        ((MyPerson) o2).getLeastLength());
            }
        });
        for (Person person : people.values()) {
            ((MyPerson)person).setLeastLength(maxNum);
        }
        ((MyPerson)per1).setLeastLength(0);
        perPriQue.addAll(people.values());
        MyPerson peekPerson = (MyPerson) perPriQue.poll(); // 彈出堆頂
​
        while (!peekPerson.equals(per2)) {
            okSets.put(peekPerson, peekPerson.getLeastLength());
            HashMap<Person, Integer> acqs = peekPerson.getAcquaintances();
            for (Person per : acqs.keySet()) {
                if (!okSets.containsKey(per) && (((MyPerson) per).getLeastLength() >
                        (peekPerson.getLeastLength() + acqs.get(per)))) {
                    perPriQue.remove(per);
                    ((MyPerson) per).setLeastLength(
                            peekPerson.getLeastLength() + acqs.get(per));
                    perPriQue.add(per);
                }
            }
            peekPerson = (MyPerson) perPriQue.poll();
        }
        if (peekPerson.equals(per2)) {
            return peekPerson.getLeastLength();
        }
        else {
            return 0;
        }
 

總體bug分析

這一單元總體bug體現為對實現方法的理解以及對方法複雜度的降低。前者需要能夠熟練閱讀jml程式碼從而獲得相應實現內容，後者則需要自己探索較好的解決策略。都是可以避免的但還是犯下了錯。

Network拓展

Network在拓展之後可以實現 購買商品、生產商品、傳送廣告、查詢銷售額、查詢銷售路徑等方法。

需要新增 Advertiser、Producer、Customer這幾個類

購買商品：

/*@ public normal_behavior
 * @ requires getCustomer(customerId) != null && getAdvertiser(advertiserId) != null && (message instanceof PurchaseMessage);
 * @ assignable getAdvertiser(advertiserId).getProducer(message.getProductId(productId));
 * @ 
 * @ ensures (\forall int i; 0 <= i && i < \old(getAdvertiser(advertiserId).getProducer(message.getProductId()).getMessageSize()); 
 * @            getAdvertiser(advertiserId).getProducer(message.getProductId(productId)).getMessage(i + 1) == 
 * @            \old(getAdvertiser(advertiserId).getProducer(message.getProductId(productId)).getMessage(i)));
 * @ ensures getAdvertiser(advertiserId).getProducer(message.getProductId(productId)).getMessage(0) == message;
 * @ ensures getAdvertiser(advertiserId).getProducer(message.getProductId(productId)).getMessageSize == 
 * @         \old(getAdvertiser(advertiserId).getProducer(message.getProductId(productId)).getMessageSize) + 1;
 * @ also
 * @ public exceptional_behavior
 * @ signals (CustomerIdNotFoundException e) !containsCustomer(customerId);
 * @ signals (MessageTypeErrorException e) !(message instanceof PurchaseMessage);
 * @ signals (AdvertiserIdNotFoundException e) !containsAdvertiser(advertiserId);
 */
public void purchaseItem(Message message, int customerId, int advertiserId, int productId);

廣告資訊傳送：

/* @ public normal_behavior
 * @ requires message instanceof AdvertiseMessage ;
 * @ assignable customers.getAdvertisements, messages;
 * @ ensures messages.length = \old(messages.length) - 1;
 * @ ensures (\forall int i; 0 <= i && i < \old(messages.length) && messages.get(i) != message; 
 * @           (\exists int j; 0 <= j && j < messages.length; \old(messages.get(i)) == messages.get(j)));
 * @ ensures (\forall int i; 0 <= i && i < customers.length; customers.getAdvertisements.get(\old(customers.getAdvertisements.size)) = message);
 * @ ensures (\forall int i; 0 <= i && i < customers.length; customers.getAdvertisements.size == \old(customers.getAdvertisements.size) + 1);
 * @ also 
 * @ puclic exceptional_behavior
 * @ signal (MessageTypeErrorException e) !(message instanceof AdvertiseMessage);
*/
public void sendAdvertisement(Message message);

得到銷售額：

/* @ public normal_behavior
 * @ requires getAdvertiser(advertiseId) != null;
 * @ ensures \result == getAdvertiser(advertiseId).getSalesMoney();
 * @ also
 * @ public exceptoinal_behavior
 * @ signal (AdvertiserIdNotFoundException e) getAdvertiser(advertiseId) == null;
*/
public int getSalesMoney(int advertiserId);

學習體會

JML單元的學習讓我瞭解到了契約式程式設計的準確和嚴謹，這對於方法的編寫有著十分重要的指導作用，可做到精準。但是對於一些用數學語言表述十分簡單的方法，用這種表述方式則十分繁瑣，閱讀理解的阻礙較大。當然jml只是給出了規範，需要自己整合優化相關實現。