其他分享
首页 > 其他分享> > OO Unit3 单元总结

OO Unit3 单元总结

作者：互联网

第三单元OO作业总结

​ 本单元的作业主要针对JML建模语言进行训练，建立对于方法规格和数据规格的认识，学习了契约式编程(Design by Contract)的编程方法与规格化设计理念。现对这一单元做一个小结。

JML语言理论基础

​ JML以Javadoc的注释形式表示规格，每个方法的规格均在该方法的前部，类的数据规格则在类代码的开头，JML语句每行以@开始。由方法规格、数据规格和异常处理组成，在使用了Java大多数语法的同时，也引入了独特的表达式以方便对规格进行描述。现对JML相关知识做一个简单总结。

基本组成

方法规格

​ 由于JML语言的思想来自于契约式编程，其三个核心部分包括

数据规格

异常处理

​ 用户输入是无法预测的，当用户给出一些不正常的输入的时候，我们不希望程序崩溃。这时候可以将这些不希望的输入放入异常部分进行统一处理，JML也提供了异常处理相关语句。

/*@ public normal_behavoir
@ ensures ...
@ ...
@ also
@ public normal_behavior
@ ...
@ also
@ public exceptional_behavior
@ ensures ...
@ signals SomeException b_expr
// 当b_expr满足时，抛出某异常
@ also
@ public exceptional_behavior
@ ensures ...
@ signals_only SomeException
// 无条件地抛出某异常
*/

表达式

原子表达式

量化表达式

集合表达式

操作符

​ 除了Java自带的操作符外，JML还提供了一些逻辑操作符，这里对其进行介绍。

操作符 示例说明
O1 <: O2 子类型操作符，如果O1是O2的子类型或者相同类型，则返回真
b_expr1<==>b_expr2 等价关系操作符，expr1成立当且仅当expr2成立（本质上是布尔类型 == 运算）
b_expr1<=!=>b_expr2 expr1成立当且仅当expr2不成立（本质为布尔类型 != 运算）
b_expr1==>b_expr2 蕴含操作符，当b_expr1为假，或者b_expr1为真且b_expr2为真时，表达式为真
\nothing ; \everything 变量指示操作符，分别表示空集和全集

OpenJML检查

​ OpenJML有多种检查方式，本测试中采用如下三种进行测试

语法检查

​ 使用语法检查对第11次作业的JML代码进行检查，将源文件全部包含在<source>中，得到结果如图

4

​ 错误来源是使用了三目运算符

    /*@ ensures \result == (people.length == 0? 0 : 
      @ ((\sum int i; 0 <= i && i < people.length; people[i].getAge()) / people.length));
      @*/
    public /*@pure@*/ int getAgeMean();
    
    /*@ ensures \result == (people.length == 0? 0 : ((\sum int i; 0 <= i && i < people.length; 
      @ (people[i].getAge() - getAgeMean()) * (people[i].getAge() - getAgeMean())) / 
      @           people.length));
      @*/
    public /*@pure@*/ int getAgeVar();

​ 进行修改后，通过了检查

    /*@ public normal_behavior
      @ requires people.length == 0;
      @ ensures \result == 0;
      @ public normal_behavior
      @ requires people.length != 0;
      @ ensures \result ==
      @          ((\sum int i; 0 <= i && i < people.length; people[i].getAge()) / people.length);
      @*/
    public /*@pure@*/ int getAgeMean();
    
    /*@ public normal_behavior
      @ requires people.length == 0;
      @ ensures \result == 0;
      @ public normal_behavior
      @ requires people.length != 0;
      @ ensures \result == (\sum int i; 0 <= i && i < people.length;
      @          (people[i].getAge() - getAgeMean()) * (people[i].getAge() - getAgeMean())) / 
      @           people.length;
      @*/
    public /*@pure@*/ int getAgeVar();

静态检查

​ 修改后，代码也通过了静态检查，出现了警告 ，由于几个方法包含了\not_assigned，对这些方法的检查被跳过

com\oocourse\spec3\main\Network.java:58: 注: Not implemented for static checking: ensures clause containing \not_assigned
      @     \old(people[i].getId()) != id2; \not_assigned(people[i]));

运行时检查

​ 运行时检查结果报错，但代码中并没有关于Object的自增运算符，此处把错误信息贴出。

The operation symbol ++ for type java.lang.Object could not be resolved

JMLUnitNG与自动测试

​ 使用JMLUnitNG产生自动化测试样例，首先将MyGroup.java和MyPerson.java进行修改，取消接口实现关系，并修改其所在包位置。

​ 分别执行以下指令，指令执行步骤参考了讨论区J哥的博客。

java -jar jmlunitng.jar test/Group.java

​ 这一步产生了测试文件

javac -cp jmlunitng.jar test/*.java

​ 这一步将产生的测试文件编译为了.class文件

java -cp jmlunitng.jar test.Group_JML_Test

​ 这一步执行了之前生成的测试文件

​ 最后一条指令的输出如下图所示

5

​ 其生成的测试用例主要针对每个函数的输入参数进行生成，可以看到其对构造方法在内的所有带输入的函数进行了输入测试。测试的情况也是一些边界数据，针对int类型变量来说就是最大整数、最小整数和0。针对对象则测试了null类型对象。可以看出，确实测出了一些边界问题，但由于官方给出的数据均有范围，没有在官方测试中引发错误。

​ 这样的测试可以覆盖性地检查一些特殊输入可能会引发的问题，但无法测试方法之间的协作关系。如对于没有输入参数的getValueSum()方法，其只检查了能否正常输出而无法生成与其配合的addPerson方法。这些方法之间的组合测试，以我目前的了解，只能使用JUnit针对每个方法写测试用例来实现。

架构设计梳理

第一次作业

​ 本次作业给出的规格较为完善，且初次接触JML对数据规格了解不足。本次对算法没有什么特殊要求，于是只按照JML提供的规格要求对程序完成构建。扩展设计仅在两处：MyPerson额外增加了addRelation()和getAcquaintance()方法。其中前者满足了将操作聚合在类内部的特点，避免外部的修改；而后者的设计有缺陷之处，其直接返回Acquaintance的ArrayList，将内部保护的数据暴露在外。在学过Iterators章节之后，可以对此处进行优化。给出UML类图。

1

第二次作业

​ 本次设计时，仍然没有注意算法上的要求，受到JML描述的局限性，Group中的大量计算密集型方法完全按照JML提供时的方法进行设计。尽管在数据规格上进行了优化，将大量ArrayList容器更换为HashMap以提升查找速度，但由于算法的局限性，导致测试点超时。由于功能没有出现明显分化，整体架构仍然按照官方接口提供的架构进行设计。给出最初设计时的UML类图，debug阶段对部分方法进行了调整，在之后会提到。

2

第三次作业

​ 本次作业对性能设计的要求更高，针对连通块的特点，同时总结第二次作业的经验，使用了类似并查集的手段进行缓存，但由于采用列表方式效率实际没有并查集高。为实现本方法，增加了Block类，提供大量静态方法，专门处理图相关的内容，减小了MyNetwork的工作负担。其他的类仍然保持之前的设计模式。

​ 方法是：

​ 通过这种方式，isCircle这种耗时的方法可以通过离线的方式进行查询，提升了查询速度。

3

​ Block类通过公共方法修改其内部状态，并且通过公共方法向外提供数据，类似一个记录者记录并更改图相关的数据。

Bug修复

第二次作业

​ 由于被JML方法规格限制，采用了大量循环进行查询。如下方的方法，实现方式与规格提供的方法完全相同。

    /*@ ensures \result == (\sum int i; 0 <= i && i < people.length; 
      @          (\sum int j; 0 <= j && j < people.length && 
      @           people[i].isLinked(people[j]); people[i].queryValue(people[j])));
      @*/
    public /*@pure@*/ int getValueSum();

​ JML只规定了方法执行后产生的结果，而对其具体实现并不关心，并且可以在数据规格规定范围之外额外规定数据。这些数据对外界是不可见的，只要实现者维护好这些变量并保证RepOK即可。于是修复时采用了缓存的方式，当有新关系或者新加入的组员的时候，更新这些缓存，通过这种方法成功修复了CTLE漏洞。

第三次作业

​ 本次作业有两个漏洞，其中一个是在进行类似并查集操作时，忘记检查两者是否本来就在一个小组(Block)内。另一个是对JML规格理解有误，没有注意到queryStrongLinked方法要求两条路径之间只有起点和终点可以重复，导致错误。

​ 修复时，正确理解规格之后，由于qsl指令条数较少，使用了循环删点 + DFS判断是否连通的方式修复了本问题。同时，增加了addRelation的两个人是否本来就在一个Block中，修复了之前的问题。

心得体会

​ 通过本次作业，从官方规格和模块的设计角度我进一步理解了构建良好框架对可扩展性的提升。学习和理解了JML在设计时的思维，将设计与实现分离。同时理解了自动化测试对软件质量保障，学习自动化测试的一些方法。这些思想和方法也一定会在以后的学习工作中让我事半功倍。

标签：OO,java,int,规格,表达式,JML,Unit3,方法,单元
来源： https://www.cnblogs.com/stevezzy/p/12941886.html