面向对象第三单元总结

来源：互联网收集：自由互联发布时间：2022-06-06

面向对象第三单元总结目录分析在本单元自测过程中如何利用JML规格来准备测试数据梳理本单元的架构设计，分析自己的图模型构建和维护策略按照作业分析代码实现出现的性能问题

面向对象第三单元总结目录

分析在本单元自测过程中如何利用JML规格来准备测试数据
梳理本单元的架构设计，分析自己的图模型构建和维护策略
按照作业分析代码实现出现的性能问题和修复情况
对Network进行扩展，以及相应的JML规格
本单元学习体会

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

前置条件
- 根据不同的前置条件情况构造数据，覆盖所有可能出现的数据类型，测试前置条件的判断是否全面覆盖且正确；
后置条件约束条件
- 判断结果的正确性

架构设计（+图模型构建+维护策略）

三次作业属性方法一览图
HW9
- MyCounter类用于异常计数，为每个异常类新增一个全局属性MyCounter记录异常出现的总次数，和单个Id出现该异常的次数；
- 其余类继承官方包类/实现官方包接口，按照JML完成相应功能即可完成一个简单的社交网络；
- qci——查询Person是否属于同一个连通图，qbs查询连通图的数量；使用并查集实现，findRoot-->判断Root_Person是否相同即可；
HW10
- qlr——求Person所在连通图的最小生成树-->Kruskal算法；
HW11
- sim——求连通图中两点间的最短路径-->Dijkstra算法；
图模型构建维护策略
- 维护一个parentMap<Integer,Integer>//<i,j>,id为i的结点对应根节点的id为j
- 在需要找到结点所在的连通图时将所有根节点id与该节点相同的结点作为连通图的点，边的权值是点与点之间的value值；
- 新建类Edge，包含属性——person1，person2，value；加入node集合后，根据person间社交关系添加对应的边即可生成该连通图；

代码实现出现的性能问题和修复情况

hw10中的qci，直接dfs实现——
- qci复杂度为O（n^2）
- qbs的复杂度为O（n^3）
hw10中求最小生成树一层层找父节点耗时长
hw10中qgvs二重循环可能导致超时
hw11中的最短路径算法常规会导致超时
解决：
- 采用并查集维护所有连通图，判断两个结点是否属于同一连通图只需要判断他们的根节点是否相同，qci复杂符降为O(1)，qbs复杂度降为O（n）；
- 在记录根节点时采用路径压缩，使一些结点直接指向根节点，减少查找根节点的时间；
- 为每一个group维护一个valueSum值，在atg，dfg，ar时该值可能发生变化；
- 采用Dijkstra堆优化算法进行优化；

对Network进行扩展——JML规格

假设出现了几种不同的Person

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

如何对Network扩展，给出相关接口方法，并选择3个核心业务功能的接口方法撰写JML规格

新建Advertiser、Producer和Customer类继承Person类
- Advertiser
  - 发送产品广告 sendAdvertiseMessage2（）
  - 接收Customer发送的BuyMessage并转发给Producer relyBuyMessage（）
- Producer
  - 包含一个或多个Product，保存当前产品生产商拥有的所有产品种类以及数量；当接受到购买信息时，将产品交给购买者；
  - 接收来自Advertiser的BugMessage并减少对应产品数量；
- Customer
  - 给Advertiser发送购买信息 sendBuyMessage1（）；
- Person
  - 新增一个Type属性，String类型存储Person的种类名称；
新建Product类
- 保存Product的相关信息，包括价格value，名称name，生产成本cost……
新建 AdvertiseMessage类和 BuyMessage类继承Message类，分别表示Advertiser对象发出的广告和Customer直接通过Advertiser给相应Producer发送的购买消息
- AdvertiseMessage
  - 包含一个Product
- BuyMessage
  - 包含一个Product
  - 包含购买数量
  - 包含购买者（消息的初始发送者） Person，为Person1
  - 包含一个Advertiser，为Person2
  - 包含生产厂商Producer ，为Person3
新增对应异常处理类
- 如CustomerNotFound，AdvertiseNotFound，ProducerNotFound……

选择三个核心业务并撰写JML规格

sendBuyMessage1(int advertiserId , BugMessage bug Message)
Customer send BuyMessage to Advertiser

    /*@ public normal_behavior
      @ requires containsMessage(bugMessageId) && getMessage(bugMessageId).getType() == 0
      @         && getMessage(bugMessageId).getPerson1().getType == "Customer"
      @         && getMessage(bugMessageId).getPerson2().getType == "Advertiser"
      @ assignable messages getMessage(id).getPerson1().money;
      @ ensures !containsMessage(bugMessageId) && messages.length == \old(messages.length) - 1 &&
      @         (\forall int i; 0 <= i && i < \old(messages.length) && \old(messages[i].getId()) != bugMessageId;
      @         (\exists int j; 0 <= j && j < messages.length; messages[j].equals(\old(messages[i]))));
      @ ensures (\old(getMessage(bugMessageId)).getPerson1().getMoney() ==
      @         \old(getMessage(bugMessageId).getPerson1().getMoney()) - getMessage(bugMessageId).getProduct.getValue();
      @ also
      @ public exceptional_behavior
      @ signals (MessageIdNotFoundException e) !containsMessage(bugMessageId);
      @ also
      @ public exceptional_behavior
      @ signals (CustomerNotFount id) !containsCustomer(getMessage(bugMessageId).getPerson1());
      @ also
      @ public exceptional_behavior
      @ signals (AdvertiserNotFount id) !containsCustomer(getMessage(bugMessageId).getPerson2());
      @*/
public void sendBuyMessage(int advertiserId , int bugMessageId) throw MessageIdNotFoundException ，CustomerNotFount ，AdvertiserNotFount ；

addProduct（Product product,Producer producer）
为一个生产厂商加入一个新产品，同时加入Network - Products[]中

 /*@ 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;

newProduct(String name,int void,int cost)
策划产品，加入preProduct中（等待现有产品队列）

 /*@ public normal_behavior
      @ requires !(\exists int i; 0 <= i && i < preProducts.length; preProducts[i].getName().equals(name));
      @ assignable preProducts;
      @ ensures preProducts.length == \old(preProducts.length) + 1;
      @ ensures (\forall int i; 0 <= i && i < \old(preProducts.length);
      @          (\exists int j; 0 <= j && j < people.length; preProducts[j] == (\old(preProducts[i]))));
      @ ensures (\exists int i; 0 <= i && i < preProducts.length; preProducts[i] == product) 
      @         && (product.getName().equals(name)) && (product.getValue() == value) && (product.getCost() == cost); 
      @ also 
      @ public exceptional_behavior
      @ signals (EqualProductException e) (\exists int i; 0 <= i && i < preProducts.length; preProducts[i].getName().equals(name));
      @ */
      public void newProduct(String name,int value,int cost) throws EqualProductException;

本单元学习体会

JML是本单元的学习重点；三次作业主要训练了我们阅读JML规格并根据JML规格完成具体实现的能力，并对数据结构知识进行了复习）；
阅读JML规格是一个简化提炼的过程，用所有的前置条件、后置条件等采取更为精简、易于理解的形式去构建一个实现的框架，在这过程中也要特别注意转化成更直观的效果时需要保证规格的全面概括；
在阅读实现的过程中，由于理解的偏差可能会出现一些情况的误处理，避免这类错误其一是不能想当然地按照固有思维进行处理；其二是可以构造将前置条件类型全覆盖的数据进行测试；
经过本单元的学习，我初步了解JML规格并认识到其在实际应用场景中的重要作用，这仅仅是一个开端，在今后的学习实践中，也应该有意识地从JML规格角度出发多思考，进一步加深对其的认识。

上一篇：组合计数 ☆ 概率期望 Solution Set
下一篇：没有了

面向对象第三单元总结

相关文章