标签：使用 open 地理 接口 等价 指令 参数 很多 可维护性
OO第三单元总结 规格JML和社交关系系统
一、JML语言概况
1.1 理论基础
JML是一种形式化面向JAVA的行为接口规格语言
作用
- 开展规格化设计与测试。将逻辑严格的规格交给代码实现人员。
- 针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。
JML语法
- JML表达式
- \result:表示一个非 void 类型的方法执行所获得的结果。
- \old(expr): 表示一个表达式expr在相应方法执行前的取值。遵从Java的引用规则，即针对一个对象引用而言，只能判断引用本身是否发生变化，而不能判断引用所指向的对象实体内容是否发生变化。
- \not_assigned(x,y)表示括号中的变量是否在方法执行过程中被赋值。该表达式主要用于后置条件的约束表示上，即限制一个方法的实现不能对列表中的变量进行赋值。
- \type(type)：返回类型type对应的类型(Class)。
- \forall全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
- \exist存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
- \sum返回给定范围内的表达式的和。
- 操作符
- E1<:E2:如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。
- b_expr1<==>b_expr2: 等价关系
- b_expr1==>b_expr2:推理操作符
- \nothing空集
- 方法规格
- 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 应用工具链
- OpenJML：检查JML规格的正确性，提供对程序的静态和动态检查。
- SMT Solver：对代码进行形式化验证。
- JMLUnitNG：根据JML自动生成测试数据来验证正确性。
二、JMLUnitNG
下载
使用方法
-
将JMLUnitNG和openjml的jar包放入同一个文件夹中
-
将魔改后的测试文件也放入同一个文件夹中（注意package）
-
运行以下指令
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。
- 在第一次作业中提到的iscircle缺少了对id1==id2情况的判断的问题。
- 我在Person中增加一个列表来记录每个人所在的Group，但是在从Group中删除人后，并未在列表中删去这个Group，导致之后新增关系时可能，仍然判断两人在同一Group中，Group中缓存的valuesum增加。
- 超时问题。在queryMinPath中我首先调用了iscircle方法来判断两点是否连通，再算最小路径。其实前者是完全没有必要的，如果无法用dijkstra算法求得最小路径，就说明了两者不连通。而多调用一个iscircle方法使得总体CPU使用时间增加了0.6秒上下，导致超时。
五、心得与体会
本单元作业看上去很简单，但是这只是一个烟雾弹。我认为，难点主要有一下：
- 自己写规格：读懂规格并不是一件难事，有的规格很长，但只要耐心地读几遍，是可以精确地理解含义的。但是写规格却是一件困难的事情。有时需要对\result中数据的推导特性（\max, \min, \sum, average）进行约束，而不是简单对每个数据进行约束；很多时候\result是某个中间数据的统计结果，而这个中间数据往往必须使用构造性算法才能产生，这时就难以直接对\result进行约束。写规格难度较大，而我对此的实践较少。
- 全方面测试：在这系列作业的测试，由于不同功能的方法很多，需要使用单元测试，有较高的覆盖率，也要对边界情况充分地测试。
毕竟一个方法没写好，可能就进不了互测了。
- 性能的优化：如果不考虑总体，直接根据规格实现代码，那么性能将会很差。这几次作业中，容器的选择、缓存的设置、算法的优化，这些都对我们系统的整体性能有很大的影响，需要好好考虑。
OO第三单元总结 规格JML和社交关系系统
标签：使用 open 地理 接口 等价 指令 参数 很多 可维护性
原文地址：https://www.cnblogs.com/shonnyx/p/12928253.html
