首页 > 其他分享> > 【2022春-面向对象】第三单元总结

【2022春-面向对象】第三单元总结

2022-06-06 15:31:35 作者：互联网

【2022春-面向对象】第三单元总结

【2022春-面向对象】第三单元总结

写在前面

本单元的主题是JML。

JML是一种形式化的语言，用来对类和方法进行规格化的描述。初见JML时可能需要花一定时间去理解其语法，而且会发现这样的语言理解起来十分费劲。例如一个“求图的最短路径”的方法可能需要几十行的JML描述。

这就是诸如JML这类形式化语言的特点：用一种规范的语法，去严谨的定义一个类的规格，及其各种方法。相比于人们交流时所使用的自然语言，形式化语言更为“规范”，避免了歧义的产生。当然任何事物都有两面性，如此“规范”的语言的代价就是理解难度高。

在初学JML时也许会感觉用JML描述规格是多此一举：例如，为了定义一种类的“求最短路径”方法，设计者需要把“求最短路径”这样的自然语言翻译成JML，然后实现者又需要把JML语言翻译成更易于理解的“求最短路径”这样的理解方式，然后再套用求最短路径的算法。试想一下如果设计者直接告诉实现者：“这个方法需要传入两个节点的编号，返回最短路径长度。”这样不是更方便吗？没错这显然更方便，减少了理解的难度，但是有产生歧义的风险。如果实现者的实现有问题，他可以说“是设计者没说清楚”。但如果设计者给出的是JML，实现有问题的话，实现者就没法找借口了。

其实实际的工程中，JML的应用不是很广泛，也许原因就在于太晦涩难懂了。但JML确实能在一定程度上帮助设计者明确规格，并不是一无是处。从学习的角度来说，学习JML也能更好学习面向对象的思想。设计者只关心需求，不关心具体实现，所以需要JML提出“需求”。而实现者要确保需求得以实现。

一.本单元架构

本单元聚焦于社交网络的建模及处理。

社交网络可以抽象为图论中的图结构：每个人是图中的节点，人与人的关系是图中的边。而作业中的需求涉及到许多对图结构的询问：例如连通块个数，最小生成树等等。如果从JML本身出发也许可以不用维护图结构，但显然复杂度过高，作为实现者，有必要引入图的数据结构，并维护之，以解决问题。

第一次作业

首先观察需求：最基本的addPerson, addRelation等方法，表示增加节点，增加关系等等。大部分这样的方法都可以直接根据JML来一板一眼的写代码即可。（当然查询操作不适用JML中数组那样的方式，而是采用HashMap增加效率。）

需求：连通性相关查询

要格外关注的是isCircle queryBlockSum：查询两个节点是否联通；查询连通块个数。如果看这两个方法给出的JML会很有意思，似乎不是很好理解：

isCircle:

/*
      @ ensures \result == (\exists Person[] array; array.length >= 2;
      @                     array[0].equals(getPerson(id1)) &&
      @                     array[array.length - 1].equals(getPerson(id2)) &&
      @                      (\forall int i; 0 <= i && i < array.length - 1;
      @                      array[i].isLinked(array[i + 1]) == true));
      @*/
public /*@ pure @*/ boolean isCircle(int id1, int id2) throws PersonIdNotFoundException;

JML的意思是“存在一个Person序列，使得第一个Person的id是id1，且最后一个Person的id是id2，且相邻两个Person邻接”，也就是存在一条连接两点的路径。

queryBlockSum:

/*@ ensures \result ==
      @         (\sum int i; 0 <= i && i < people.length &&
      @         (\forall int j; 0 <= j && j < i; !isCircle(people[i].getId(), people[j].getId()));
      @         1);
      @*/
public /*@ pure @*/ int queryBlockSum();

JML的意思是统计所有person中“id小于它的person都不与它联通”的person的个数。再翻译一下，每个连通块中只有id最小的person被计数。也就是统计了连通块个数。

通过观察这两个方法的JML也能发现JML的一大特点：确实相对不利于理解。

实现：并查集

理解上述方法后，两个方法具体该如何实现？答案是并查集。并查集可以很好的维护连通性相关的信息。

我们可以引入新的类:DisjointSetUnion，提供的public方法：

void add(int):增加节点编号为id
void merge(int, int):使两个节点联通
boolean check(int, int) :查询两节点是否连通
int qbs()：查询连通块个数

并查集具体的实现方法网上的资料已经很多了，这里不再赘述。我们只关心架构设计。

在Network中增加了并查集对象，在addPerson以及addRelation中对并查集维护即可。

第二次作业

我们关心新增的方法。

需求

message相关：新增message，发送message等等。照着JML一点一点实现即可。

group相关：新增qgas,qgav等方法，查询一个Group内的信息。这里需要注意下复杂度的控制，如果按照JML实现的复杂度为\(O(n^2)\),\(n\)为group中person个数。这里恰好能说明：JML只是给出了设计者所期望的需求，具体实现以及性能的控制由实现者自行考虑。

qlc：查询最小生成树边权和。

/*    @ 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])));
      @*/
    public /*@ pure @*/ int queryLeastConnection(int id) throws PersonIdNotFoundException;

这里的JML为了定义最小生成树，给出了一个边集subgroup,其需要满足条件：

相邻两个person邻接（因为是边集）
所有与查询的id联通的点都出现在subgroup里
所有与查询的id联通的点都可以用subgroup里面的边组成一条路径

如此便定义了最小生成树。

实现

引入MstSolver类，提供方法：

int solve(List<MyPerson> people);

传入person的集合（保证输入参数是连通图），给出最小生成树边权和。对于具体的算法，本次使用了Kruscal算法，方法内部还可以借助上次作业的并查集对象进行维护。

第三次作业

我们关心新增的方法。

需求

此次涉及到新的三种不同的message类型。以及需要查询最短路径的sendIndirectMessage方法。

/*@ ensures (\exists Person[] pathM;
      @         pathM.length >= 2 &&
      @         pathM[0].equals(\old(getMessage(id)).getPerson1()) &&
      @         pathM[pathM.length - 1].equals(\old(getMessage(id)).getPerson2()) &&
      @         (\forall int i; 1 <= i && i < pathM.length; pathM[i - 1].isLinked(pathM[i]));
      @         (\forall Person[] path;
      @         path.length >= 2 &&
      @         path[0].equals(\old(getMessage(id)).getPerson1()) &&
      @         path[path.length - 1].equals(\old(getMessage(id)).getPerson2()) &&
      @         (\forall int i; 1 <= i && i < path.length; path[i - 1].isLinked(path[i]));
      @         (\sum int i; 1 <= i && i < path.length; path[i - 1].queryValue(path[i])) >=
      @         (\sum int i; 1 <= i && i < pathM.length; pathM[i - 1].queryValue(pathM[i]))) &&
      @         \result==(\sum int i; 1 <= i && i < pathM.length; pathM[i - 1].queryValue(pathM[i])));
      */

这里给出了sendIndirectMessage方法的部分JML，此部分JML定义了最短路径。翻译过来的意思是：存在一个Person数组，使得相邻两个person邻接，并且相邻Person的边权和是所有这样的数组之中最小的。返回最小的边权和。

实现

新建graph类，维护图的信息。方法int getShortestPath(int start, int end);提供查询最短路径的服务。

总结

实际上本次的三次作业实现都有图相关的修改或者查询等操作。并查集，最小生成树，最短路径，都属于图相关的询问。但是在这三次作业的迭代中，这三种询问用了三个不同的类来实现，显得有些复杂。如果考虑重构的话，将这些图相关的操作封装到一个统一的类中会更好。

二.测试数据构造（利用JUnit）

众所周知JUnit是一种用来测试的工具。它提供了一个方便进行测试的环境，利于用户构造数据开展测试，并快速找到bug的来源。

但是归根到底它只是一个工具，真正的测试数据的构造还需要人类的主观能动性。

测试可以采取逐步递进的策略：对单一类单一方法的功能性测试，和对单一类多方法间协同的测试，和对多个类的综合性测试。

单一方法测试

对单一方法测试相对简单。需要改变的有两个地方：一是对象本身的状态；二是传入的参数。而验证正确性则要编写对应的对象状态检查函数repOk()以及每个方法的返回值检查函数，来检查对象本身和返回值的正确性。因为涉及到对象状态的改变，所以测试时要优先保证一些改变对象状态，且较为重要的方法优先测试。

（这里的“重要”比较泛，这样的方法的特点一般有：实现不是很复杂，使用很频繁，等等。例如本次的addPerson addRelation等等）

对于一般的方法，其测试方式便是：尽可能利用测试好的方法改变对象状态，在不同的状态下传入不同的参数进行测试。

单一类测试

对于一个类来说，测试的一个重要的事情是各方法调用的次序。就像学习计组时做测试，常常需要通过随机构造指令序列，制造各种数据冲突。对于类的测试可能也需要随机构造调用方法的次序。

除了随机，也可以尝试手造一些极限数据，往往是为了弥补随机测试不够全面的地方。

综合性测试

对多个类的协同工作进行测试。对于随机的测试策略而言，可以将随机的范围扩大：每个类的新建，所有类的所有方法，都需要随机其顺序。这样的数据构造往往相对困难，因为需要保证调用方法的顺序是合理的，因此需要斟酌随机产生的次序。当然对于这次作业而言，可以仅仅随机输入的指令，这也是最为方便的方法之一，但是缺点在于容易有测试不到的地方。

总结

上述三种测试方法的范围从小到大。在测试时间一定的情况下，范围越大，相对来讲对每一个类或方法而言的测试强度则会减弱。至于优先做哪种测试还要具体问题具体分析，如果规模不大可以直接做综合性测试，如果规模较大最好先对单一类或方法进行测试。此外对于一些容易出问题的类或方法，复杂程度很高的类或方法，最好要进行额外的单一的针对性测试。

三.代码修复及性能分析

bug修复

本单元的作业相对而言难度不大，bug仅在第一次测试中出现过，原因是没有实现“异常中的两个传入的id相同时，只统计一次异常”。这说明测试是基于需求的。如果需求有所遗漏，那么测试时自然不会考虑到这样的需求，从而导致检测不出这样的错误。也就是说，无论是代码实现还是测试，明确需求总是第一位的。

性能分析

本单元作业涉及到的各个查询需要进行复杂度的控制。需要尽可能保证每个输入的指令，运行的最坏复杂度不能到达\(O(n^2)\)量级，否则不能在规定时间内运行完毕。

int queryGroupValueSum(int id)：查询一组person之间的所有边权和。解决方案：在Group类中新建成员变量valueSum，每次增加组内成员时，以及每次增加边时，更新valueSum，在查询时直接输出此变量值。复杂度变为\(O(1)\).
int queryGroupAgeVar(int id)：查询组内年龄方差。若完全按JML实现复杂度为\(O(n^2)\).解决方案：只调用一次getAgeMean()获取平均值再计算。复杂度\(O(n)\).
boolean isCircle(int id1, int id2):查询是否联通。通过维护并查集即可。采取路径压缩的并查集优化后，复杂度约为常数级别。
int queryBlockSum()：查询连通块个数。在并查集对象中维护此值即可：每次新增节点，连通块个数+1；每次合并两个不连通的节点，连通块个数-1。复杂度为\(O(1)\)。
int queryLeastConnection(int id)：查询最小生成树。采用Kruscal算法加并查集维护。复杂度\(O(E\times logE)\),\(E\)为边的个数。
int sendIndirectMessage(int id) :查询最短路径。采用堆优化的Dijkstra算法的复杂度为\(O(n\times logn)\)。

四.对Network进行扩展

假设出现了几种不同的Person

Advertiser：持续向外发送产品广告

Producer：产品生产商，通过Advertiser来销售产品

Customer：消费者，会关注广告并选择和自己偏好匹配的产品来购买
-- 所谓购买，就是直接通过Advertiser给相应Producer发一个购买消息

Person：吃瓜群众，不发广告，不买东西，不卖东西

如此Network可以支持市场营销，并能查询某种商品的销售额和销售路径等

需求分析

我们先从需求的角度出发，对于一个需要支持市场营销的NetWork来说，可能会存在哪些需求。

对消费者：查询收到的所有广告列表；从某个Advertiser购买某件商品。
对生产商：新建某个商品；查询某商品的销售额，库存等；
对Advertiser：新建和发送某个广告（借助addMessage，sendMessage）；查询某个广告有多少消费者通过此广告购买了产品（通过这种查询了解广告的效果）；

接口设计

新建Item类，表示商品。属性有ID号与价格。支持ID查询，价格的查询与修改。

public interface Item {

    /*@ public instance model int id;
      @ public instance model int price;
      @*/
    
    public void setPrice();

    public /*@ pure @*/ int getPrice();
    
    public /*@ pure @*/ int getId();
}

新建消息类，继承自Message。Advertisement类是Advertiser发送给Customer的消息。作为Customer可以查询所有收到的广告，可以依据某个广告购买。

public interface Advertisement extends Message {
    //@ public instance non_null Item item;
    
    //@ public invariant socialValue == item.getPrice();
}

新建各种不同类别的Person：Customer，Advertisor，Producer
新增异常InvalidPersonTypeException：只有特定类型的person能使用特定的方法。
其他：在Person中新增相应查询方法，等等。

方法设计

关于Network，新增模型Item[] items.

public interface Network {

    /*@ public instance model non_null Person[] people;
      @ public instance model non_null Group[] groups;
      @ public instance model non_null Message[] messages;
      @ public instance model non_null int[] emojiIdList;
      @ public instance model non_null int[] emojiHeatList;
      @ public instance model non_null Item[] items;
      @*/
}

查询Customer的所有广告

	
   /*@ public normal_behavior
      @ requires contains(id) && (getPerson(id) instance of Customer);
      @ ensures \result == ((Customer) getPerson(id)).getReceivedAdvertisements();
      @ also
      @ public exceptional_behavior
      @ signals (PersonIdNotFoundException e) !contains(id);
      @ public exceptional_behavior
      @ signals (InvalidPersonTypeException e) contains(id) && !(getPerson(id) instance of Customer);
      @*/
    public /*@ pure @*/ List<Advertisement> queryReceivedAdvertisements(int id) throws PersonIdNotFoundException, InvalidPersonTypeException;

购买某件商品,个数为count（通过某条广告）

前置条件：对应person存在，且为Customer类型,且存在此Message。

/*@ public normal_behavior
      @ requires contains(personId) && (getPerson(id) instance of Customer) && !(((Customer) getPerson(id)).haveAdvertisement(advertisementId));
      @ assinable people;
      @ ensures getPerson(id).getMoney() == \old(getPerson(id).getMoney) - getMessage(advertisementId).getItem().getPrice();
      @ ensures people.length == \old(people.length);
      @ ensures (\forall int i; 0 <= i && i < \old(people.length);
      @          (\exists int j; 0 <= j && j < people.length; people[j] == \old(people[i])));
      @ ensures (\forall int i; 0 <= i && i < people.length && \old(people[i].getId()) != personId; \not_assigned(people[i]));
      @ also
      @ public exceptional_behavior
      @ signals (PersonIdNotFoundException e) !contains(personId);
      @ public exceptional_behavior
      @ signals (InvalidPersonTypeException e) contains(personId) && !(getPerson(id) instance of Customer);
      @ public exceptional_behavior
      @ signals (MessageNotFoundException e) contains(personId) && (getPerson(id) instance of Customer) && !(((Customer) getPerson(id)).haveAdvertisement(advertisementId));
      @*/
public void buy(int personId, int advertisementId， int count) throws PersonIdNotFoundException, InvalidPersonTypeException, MessageNotFoundException;

新建某个商品（在对应生产商处注册商品）

/*@ public normal_behavior
      @ requires contains(personId) && (getPerson(id) instance of Producer) 
      @ assinable people;
      @ ensures ((Producer) getPerson(producerId)).containsItem(item.getId());
      @ ensures ((Producer) getPerson(producerId)).getItemCount(item.getId()) == 0;
      @ ensures \forall(int i = 0; 0 <= i && i < items.length; \old(((Producer)getPerson(producerId)).containsItem(item.getId())) ==>((Producer)getPerson(producerId)).containsItem(item.getId()));
	  @ ensures ((Producer)getPerson(producerId)).itemCount()) == \old(((Producer)getPerson(producerId)).itemCount())) + 1;
      @ ensures people.length == \old(people.length);
      @ ensures (\forall int i; 0 <= i && i < \old(people.length);
      @          (\exists int j; 0 <= j && j < people.length; people[j] == \old(people[i])));
      @ ensures (\forall int i; 0 <= i && i < people.length && \old(people[i].getId()) != personId; \not_assigned(people[i]));
      @ also
      @ public exceptional_behavior
      @ signals (PersonIdNotFoundException e) !contains(personId);
      @ public exceptional_behavior
      @ signals (InvalidPersonTypeException e) contains(personId) && !(getPerson(id) instance of Producer);
     
      @*/
public void addNewItem(int producerId, Item item) throws PersonNotFoundException,InvalidPersonTypeException;

生产某件商品,个数为count。

public void produceItem(int itemId, int count) throws ItemNotFoundException,InvalidPersonTypeException;

查询商品销售额

public int queryItemValue(int itemId) throws ItemNotFoundException,InvalidPersonTypeException;

查询库存

public int queryItemCount(int itemId) throws ItemNotFoundException,InvalidPersonTypeException;

查询某个广告有多少消费者通过此广告购买了产品

public int queryAdvertisementValue(int messageId) throws MessageIdNotFoundException, InvalidPersonTypeException;

五.学习体会

JML因其形式化的特点，可以对需求进行规范化设计，但因此复杂程度有所增高。尽管工程上可能用不上JML，但是利用此方法有利于进行面向对象思想的学习。这单元的难度在于对这种语言以及面向对象思想的理解，并不在于代码实现。在以后的学习中不管用不用JML，都要时刻记住要明确需求，严格在满足需求的情况下给出相应实现。

最后衷心感谢老师助教同学在学习之路上的帮助。

标签：JML,int,测试,public,面向对象,2022,查询,id,单元
来源： https://www.cnblogs.com/infinity0/p/16348336.html