OO第三单元总结

自测过程中如何利用JML规格来准备测试数据

在整个第三单元的JML语言的学习下来，确实能够感觉到这真的是一门描述十分清晰的语言，从我们输入的数据的要求，数据中间变化的要求，再到输出数据的要求在JML中都是有较为严格的规定的，这也就为我们这个单元进行自测提供了不小的便利。具体如下：

• 前置条件：构造数据肯定是依照JML所给的要求来进行构造，再在保证符合前置条件的前提下覆盖可能出现的所有数据类型，我们也能通过前置条件判断我们是否全面覆盖。
• 可变式、不变式：提醒我在方法实现中是否超过副作用范围或破坏不变式。
• 后置条件：通过JML语言判定方法的正确性。

架构设计与图模型构建和维护策略

整个三个作业中主要的架构都在JML中给出来了，自我发挥空间很少，第一次作业中没有进行仍和其他类的实现，在第二次和第三次作业中因为涉及到了一些图的经典算法，所以我是在JML的基础上多实现了一个类——Edge类，实现代码如下：

package com.oocourse.spec3.main;

public class Edge implements Comparable<com.oocourse.spec3.main.Edge> {
    public MyPerson getPerson() {
        return person;
    }

    public MyPerson getPerson1() {
        return person1;
    }

    public int getValue() {
        return value;
    }

    private final MyPerson person;
    private final MyPerson person1;
    private final int value;

    Edge(MyPerson person, MyPerson person1, int value) {
        this.person = person;
        this.person1 = person1;
        this.value = value;
    }

    @Override
    public int compareTo(com.oocourse.spec3.main.Edge e) {
        if (value > e.value) {
            return 1;
        } else if (value < e.value) {
            return -1;
        } else {
            if (person.getId() > e.person.getId()) {
                return 1;
            } else {
                return -1;
            }

        }
    }
}

一个基础的“边”类，里面主要就是存储了两个MyPerson端点和它们之间的Value值，方便进行最短路径和最小连通图的计算。

构建

总的来说，这整个社交网络图就是用addPerson和addRelation构建起起来基本的框架，其他很多都是在这个基础上进行一些查询操作，除此之外就是对其中的person进行一些分组和message处理，然后是一些对于group和message的操作。

维护

图的维护，整体维护的框架也不太需要我们去设计，Person的点集我是使用一个ArrayList管理，然后其边集的信息开始都是在MyPerson这个类里面存储，没有在MyNetwork中特别的实现边集的存储。但是在我们第二次作业中进行最小生成树和最后一次作业中进行最短路径算法时我构建帮且维护了上面那个Edge类组成的List，存储了边集，方便操作。

性能问题与修复情况

容器选择问题

• 开始一直是多用ArrayList对我的所有person、group、message等等，后面我发现这样子自己程序跑的一直是比别人差的，意识到使HashMap进行管理可以将每次的查询复杂度由O（n）降到最优情况下是O（1）
• 用PriorityQueue容器降低了插入队首和取出队首的复杂度。

动态维护和来一次算一次

我们在第二次作业中的qgvs开始一直是来一次算一次，这样子我的复杂度就达到了可怕的O(n²)，在互测被干爆了，后面进行bug修复时候我在里面维护一个valueSum变量，直接返回这个变量就行，而我们只需要在addValue、dfg、atg更新值就行了，复杂度大大降低

并查集优化

这次很有幸的是在自己写最小生成树qlc方法之前就看到了讨论区有关并查集优化的分享，自己认真学习后在自己写的时候直接就使用了基于并查集的克鲁斯卡尔算法，性能很好，这部分没有需要我在进行优化。十分感谢那位在讨论区进行分享的同学。

Network的扩展

要求：

• Advertiser：持续向外发送产品广告
• Producer：产品生产商，通过Advertiser来销售产品
• Customer：消费者，会关注广告并选择和自己偏好匹配的产品来购买 -- 所谓购买，就是直接通过Advertiser给相应Producer发一个购买消息
• Person：吃瓜群众，不发广告，不买东西，不卖东西

如此Network可以支持市场营销，并能查询某种商品的销售额和销售路径等 请讨论如何对Network扩展，给出相关接口方法，并选择3个核心业务功能的接口方法撰写JML规格（借鉴所总结的JML规格模式）

如何实现：

• 新建Advertiser、Producer、Customer类继承Person类
• 新增Produce类来封装商品的各种属性和一些操作
• 新增AdvertiseMessage和PurchaseMessage类继承Message类
• 依照我们这个单元的异常类相应实现一些NotFound类等异常类

三个核心方法JML完成

//广告商发广告
/*@ public normal_behavior
      @ requires contains(personId) && getPerson(personId) instanceof Advertiser &&
      @          containsMessage(messageId) && getMessage(messageId) instanceof AdvertisementMessage;
      @ assignable people[*].messages;
      @ ensures (\forall int i; 0 <= i < people.length;
      @          \old(people[i].getMessages().size) + 1 == people[i].getMessages().size() &&
      @          (\forall int j; 0 <= j < \old(people[i].getMessages().size());
      @          \old(people[i].getMessages()).get(i) == people[i].getMessages().get(i+1)) &&
      @          people[i].getMessages().get(0).equals(getMessage(messageId)));
      @ also
      @ public exceptional_behavior
      @ signals (PersonIdNotFoundException e) !contains(personId) ||
      @          (contains(personId) && !(getPerson(personId) instanceof Advertiser));
      @ signals (ProductIdNotFoundException e) contains(personId) && getPerson(personId) instanceof Advertiser &&
      @          (!containsMessage(messageId) ||
      @          (containsMessage(messageId) && !(getMessage(messageId) instanceof AdvertisementMessage)));
      @*/
    public int sendAdvertisementMessage (int personId, int messageId)
            throws PersonIdNotFoundException, MessageIdNotFoundException;

//查询产品销售额
/*@ public normal_behavior
      @ requires containsProductId(ProductId);
      @ ensures \result == getProduct(ProductId).getSalesAmount();
      @ also
      @ public exceptional_behavior
      @ signals (ProductIdNotFoundException e) !containsProduct(ProductId);
      @*/
public int queryProductSales(int ProductId) throws ProductIdNotFoundException;

//添加商品
 /*@ public normal_behavior
     @ requires !(\exists int i; 0 <= i && i < products.length; products[i].equals(product)) && (\exists int i; 0 <= i && i < preProducts.length; preProducts[i].equals(product))
     @ assignable products,producer.getProducts()
     @ ensures products.length == \old(products.length) + 1;
     @ ensures (\forall int i; 0 <= i && i < \old(products.length);
     @          (\exists int j; 0 <= j && j < products.length; products[j].equals(\old(products[i]))));
     @ ensures (\exists int i; 0 <= i && i < products.length; products[i].equals(product));
     @ ensures producer.getProducts().length == \old(producer.getProducts().length) + 1;
     @ ensures (\forall int i; 0 <= i && i < \old(producer.getProducts().length);
     @          (\exists int j; 0 <= j && j < producer.getProducts().length; producer.getProducts()[j].equals(\old(producer.getProducts()          @            [i]))));
     @ ensures (\exists int i; 0 <= i && i < producer.getProducts().length; producer.getProducts()[i].equals(product));
     @ also
     @ public exceptional_behavior
     @ signals (EqualProductException e) (\exists int i; 0 <= i && i < products.length;
     @                                     products[i].equals(product));
     @*/
public void addProduct（Product product,Producer producer）throw EqualProductException

本单元学习体会

本单元学习了jml规格，还有契约化编程的思想，习得了JML撰写和代码实现的转化，虽说自己现在直接撰写JML能力还是十分有限，但也算是起步了吧。

我自己印象更深的可能要算是契约化编程，了解到了自己作为程序员在一个项目完成中可能要扮演着一个怎样的角色，并且基于契约化编程所能带来的好处，可能现在的感受还是太过于肤浅，希望自己可以在以后的应用中能更深刻地体会契约化的作用。

除此之外，本单元不得不说肯定是在作业的完成中复习了很多算法，之前很多算法学习的时候觉得也不是很复杂，但是真正在自己用代码实现并放到一个实际的问题中后才发现过程并不是这么轻松的，这也警示我之后在学习很多算法之后，不能只停留在理解上面，尽量多去自己用代码实现。

总而言之，本单元在不是那么累的状态下学习了基于规格化设计思想、契约化编程思维和一些算法实现等。

标签：OO,总结,return,MyPerson,value,person,JML,public,单元
来源： https://www.cnblogs.com/qiaoaiku44/p/16348087.html