OO第三单元总结规格JML和社交关系系统

Posted 2021-02-18 shonnyx

OO第三单元总结 规格JML和社交关系系统

一、JML语言概况

1.1 理论基础

JML是一种形式化面向JAVA的行为接口规格语言

作用

1. 开展规格化设计与测试。将逻辑严格的规格交给代码实现人员。
2. 针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。

JML语法

• JML表达式
  • esult:表示一个非 void 类型的方法执行所获得的结果。
  • old(expr): 表示一个表达式expr在相应方法执行前的取值。遵从Java的引用规则，即针对一个对象引用而言，只能判断引用本身是否发生变化，而不能判断引用所指向的对象实体内容是否发生变化。
  • ot_assigned(x,y)表示括号中的变量是否在方法执行过程中被赋值。该表达式主要用于后置条件的约束表示上，即限制一个方法的实现不能对列表中的变量进行赋值。
  • ype(type)：返回类型type对应的类型(Class)。
  • forall全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
  • exist存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
  • sum返回给定范围内的表达式的和。
• 操作符
  • E1<:E2:如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。
  • b_expr1<==>b_expr2: 等价关系
  • b_expr1==>b_expr2:推理操作符
  • othing空集
• 方法规格
  • requires：前置条件，要求调用者确保P为 真。
  • ensures：后置条件，方法实现者确保方法执行返回结果一定满足谓词P的要求。
  • assignable、modifiable：副作用范围限定，指方法在执行过程中会修改对象的属性数据或者类的静态成员数据。
• Pure关键词
  • 设计中会出现某些纯粹访问性的方法，即不会对对象的状态进行任何改变，也不需要提供输入参数，这样的方法无需描述前置条件，也不会有任何副作用，且执行一定会正常结束。对于这类方法，可以使用简单的（轻量级）方式来描述其规格，即使用 pure 关键词。
  • 在方法规格中，前置条件可以引用 pure 方法返回的结果。
  • 不变式中可以直接引用pure形态的方法。
• 异常
  • 异常情况:public exceptional_behavior
  • signals子句的结构为 signals (***Exception e) b_expr ，意思是当 b_expr 为 true 时，方法会抛出括号中给出的相应异常e。
  • 简化的signals子句即signals_only子句：后面跟着一个异常类型。
• 类型规格
  • invariant：不变式，要求在所有可见状态下都必须满足的特性。（凡是会修改成员变量（包括静态成员变量和非静态成员变量）的方法执行期间，对象的状态都不是可见状态。）
  • constraint：状态变化约束，对前序可见状态和当前可见状态的关系进行约束。

1.2 应用工具链

1. OpenJML：检查JML规格的正确性，提供对程序的静态和动态检查。
2. SMT Solver：对代码进行形式化验证。
3. JMLUnitNG：根据JML自动生成测试数据来验证正确性。

二、JMLUnitNG

下载

• openjml：http://www.openjml.org/
• JMLUnitNG：http://insttech.secretninjaformalmethods.org/software/jmlunitng/

使用方法

1. 将JMLUnitNG和openjml的jar包放入同一个文件夹中

2. 将魔改后的测试文件也放入同一个文件夹中（注意package）

3. 运行以下指令

   java -jar jmlunitng.jar test/Group.java

   javac -cp jmlunitng.jar test/*.java

   java -jar openjml.jar -rac test/Group.java test/Person.java

   java -cp jmlunitng.jar test.Group_JML_Test

使用限制

• 不支持拥有全称量词和存在量词的关键词。
• 如果对一个以缓存机制实现的方法进行测试，测试效果不好，因为无法调用其他类中方法来更新缓存。

终于PASS的简单测试结果

测试范围

主要是用一些边界条件对方法进行测试，比如int的最大最小值、对象为null等情况等。窃以为这种测试方式对我们本次作业的帮助不是很大。

三、程序架构设计

可能是课程组提供了详细的JML与接口的原因，这三次作业自己对架构设计方面没有引起足够的重视，只是通过自己的类实现了三个接口，结构十分简单，也导致耦合性很高。而考虑架构的可扩展性，可以建立图的结点类、边类，以应对带权图的可能。将图的算法实现放到一个类中，可以降低耦合。

在模型构建过程中，主要选取增删查改很快的HashMap作为存储Person的容器。

通过缓存法来存储Group内age、value等信息。具体来说，每当有人加入Group时，更新character、age等信息，在查询方法调用时直接返回。但是这样还必须要考虑两个人先加进Group，后添加关系的情况。我在Person类中添加列表记录所在的Group，在add_relation时查找两个人是否有共同的Group，并更新Group内的value信息。

对于几个比较复杂的方法，我的实现算法是：

• isCircle：简单的bfs。
• queryMinPath：使用优先队列（堆排序）的dijkstra算法。其中优先队列直接使用JAVA类PriorityQueue。
• queryStrongLinked：首先对iscircle算法修改，找到并记录一条包含三个结点以上的id1到id2的路径。对路径中的每个点，如果删除它后（直接在bfs算法中设置此结点已经访问），仍然能够找到一条id1到id2的路径，则他们是点双连通的。
• queryBlockSum：多次bfs找连通分量。

四、代码BUG

第一次作业

强测互测都没有发现BUG。

但实质上iscircle缺少了对id1==id2情况的判断，这个BUG一直遗留到了第三次作业才解决。

第二次作业

未进互测，强测挂的点均为超时。

原因是Group中用ArrayList来存储person。Group中增加、查找次数很多，而用ArrayList遍历导致时间损耗很大。改成存储(id,person)的HashMap，它的增、删、查、改都是十分迅速的，修改后CPU使用时间减少很多。

第三次作业

发现三个BUG。

1. 在第一次作业中提到的iscircle缺少了对id1==id2情况的判断的问题。
2. 我在Person中增加一个列表来记录每个人所在的Group，但是在从Group中删除人后，并未在列表中删去这个Group，导致之后新增关系时可能，仍然判断两人在同一Group中，Group中缓存的valuesum增加。
3. 超时问题。在queryMinPath中我首先调用了iscircle方法来判断两点是否连通，再算最小路径。其实前者是完全没有必要的，如果无法用dijkstra算法求得最小路径，就说明了两者不连通。而多调用一个iscircle方法使得总体CPU使用时间增加了0.6秒上下，导致超时。

五、心得与体会

本单元作业看上去很简单，但是这只是一个烟雾弹。我认为，难点主要有一下：

• 自己写规格：读懂规格并不是一件难事，有的规格很长，但只要耐心地读几遍，是可以精确地理解含义的。但是写规格却是一件困难的事情。有时需要对 esult中数据的推导特性（max, min, sum, average）进行约束，而不是简单对每个数据进行约束；很多时候 esult是某个中间数据的统计结果，而这个中间数据往往必须使用构造性算法才能产生，这时就难以直接对 esult进行约束。写规格难度较大，而我对此的实践较少。
• 全方面测试：在这系列作业的测试，由于不同功能的方法很多，需要使用单元测试，有较高的覆盖率，也要对边界情况充分地测试。毕竟一个方法没写好，可能就进不了互测了。
• 性能的优化：如果不考虑总体，直接根据规格实现代码，那么性能将会很差。这几次作业中，容器的选择、缓存的设置、算法的优化，这些都对我们系统的整体性能有很大的影响，需要好好考虑。