第三单元OO作业总结

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

JML语言理论基础

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

基本组成

方法规格

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

• requires：定义该方法的前置条件，即使用者（客户）需满足的义务。如果使用者没有遵守义务，可使用抛出异常或打印输出的方式提示用户。
• ensures：定义该方法的后置条件，即本方法需履行的义务。当满足前置条件的时候，本方法执行结束后一定满足后置条件。
• assignable：定义了副作用范围，列出了本方法可以修改的类成员属性。如果一个方法不对类成员属性进行修改，则是一个pure方法。

数据规格

• invariant不变式

  在所有可见状态下都必须满足的特性，总结一下就是在方法执行的过程中可以短暂地不满足不变式，而方法执行前和执行结束后都必须满足不变式。对于多线程程序而言，如果运行过程中会有短暂不满足不变式的情况，需要对该方法加锁避免其他线程访问到不满足不变式的对象。

• constraint不变式

  规定了前序可见状态与当前可见状态下不变式的关系，例如

  constraint size == \old(size) + 1

  说明执行完该方法之后，size变量需要自增1

异常处理

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

• public normal_behavior：以本语句开头之后的所有内容为对一个正常行为的JML描述
• public exceptional_behavior：以本语句开头之后的内容为对一个异常行为的JML描述
• signals：当满足一定条件时，抛出某个异常
• signals_only：无条件抛出某个异常

/*@ 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
// 无条件地抛出某异常
*/

表达式

原子表达式

• \result：非空方法执行后的返回值，类型与方法定义的相同
• \old(expr)：表示一个表达式在执行该方法之前的取值，由于其按照Java规范关注引用，当一个可变对象内部发生修改后，使用该表达式无法探测。即\old(expr) == expr，故需要规定其内部属性变化时，需要将其属性括在\old中，如\old(expr.getProp1())。
• \not_assigned() not_modified()：限制表达式在执行期间取值未改变
• \nonnullelements(container)：容器中不会有null对象存在
• \type(t)：返回t类型对应的Class
• \typeof(e)：返回e表达式的Class

量化表达式

• \forall：全称量词表达式，对于属于范围内的元素，保证其均满足约束。其格式如下

  (\forall int i; condition; requires)

• \exists：存在量词表达式，对于属于范围内的元素，保证其存在一个元素满足约束。其格式如下

  (\exists int i; condition; requires)

• \sum：条件求和表达式，对于属于范围内的元素，对其标识的变量add求和

  (\sum int i; condition; add)

• \product：条件连乘表达式，与求和类似，不过改成乘法

  (\product int i; condition; mult)

• \max：范围内最大值表达式，对于属于范围内的元素，返回某一属性的最大值

  (\max int i; condition; property)

  例如

  \max int i; -5 <= i && i <= 0; i*i，则获得25。

• \min：范围内最小值表达式，用法与\max类似，这里就略过

• \num_of：返回指定范围内变量满足条件的个数

  (\num_of int i; range condition; condition)

  其等价于

  (\sum int i; range condition && condition; 1)

集合表达式

• 在JML规格中构造一个局部容器，明确其中可包含的元素

  new JMLObjectSet {Integer i | s.contains(i) && 0 < i.intValue() } ，构造了一个JMLObjectSet对象，其中的元素均在s容器中存在，且整数值大于0。

操作符

​ 除了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有多种检查方式，本测试中采用如下三种进行测试

• 语法检查：可检查JML语法是否有错误

  java -jar openjml.jar -check <source>

• 静态检查：

  java -jar openjml.jar -esc <source>

• 动态检查：

  java -jar openjml.jar -rac <source>

语法检查

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

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

    /*@ 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

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

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

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

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

架构设计梳理

第一次作业

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

第二次作业

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

第三次作业

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

​ 方法是：

• 当有新的人加入的时候，他与任何人都没有联系，故为其创建一个Block

• 每当有新的relation的时候，检查两个人是否在一个Block中，如果不在一个Block中，则将后者Block删除，并将其元素全部放入前者的Block中。在实际操作时为减小时间开销，删除的Block为人数较少的那个。

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

​ 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规格只是提供了要求，而具体实现并未限制

  在初次接触JML的时候，一个很大的误区是认为数据和计算方式必须按照JML规格进行。随着学习的逐渐深入，特别是学习了数据规格抽象之后，了解了只要满足RepOK便可以设计自己的数据结构来代表规格中的数据。同时对于方法规格，JML也只限制了输出的结果，无论其中采用何种实现方式，只要使得输出结果满足\ensures语句即可。JML只是一个规格的传递者，而不是一个告诉你应当采用何种容器，使用何种算法。

• JUnit自动测试与回归测试为程序质量提供了保证

  每次修改程序或者重构的时候，总是担心本来功能正常的程序经过一番修改（魔改）之后出现异常。在使用了JUnit之后，这个问题就变得容易了。虽然编写测试用例需要花费一定的时间，但是随着迭代次数逐渐增多，才发现JUnit真香。

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