其他分享
首页 > 其他分享> > 面向对象第三单元总结

面向对象第三单元总结

作者：互联网

面向对象第三单元总结

目录

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

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

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

对Network进行扩展——JML规格

假设出现了几种不同的Person

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

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

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

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

 /*@ 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规格角度出发多思考，进一步加深对其的认识。

标签：总结,Advertiser,Customer,Producer,Person,面向对象,规格,JML,单元
来源： https://www.cnblogs.com/zhaixing771/p/16341459.html