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

Posted shonnyx

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了OO第三单元总结规格JML和社交关系系统相关的知识,希望对你有一定的参考价值。

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

下载

使用方法

  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进行约束。写规格难度较大,而我对此的实践较少。
  • 全方面测试:在这系列作业的测试,由于不同功能的方法很多,需要使用单元测试,有较高的覆盖率,也要对边界情况充分地测试。毕竟一个方法没写好,可能就进不了互测了。
  • 性能的优化:如果不考虑总体,直接根据规格实现代码,那么性能将会很差。这几次作业中,容器的选择、缓存的设置、算法的优化,这些都对我们系统的整体性能有很大的影响,需要好好考虑。

以上是关于OO第三单元总结规格JML和社交关系系统的主要内容,如果未能解决你的问题,请参考以下文章

OO第三单元总结

OO-第三单元总结-2021

OO第三单元总结

oo第三单元总结

OO第三单元(JML)总结

OO第三单元总结