BUAA_OO_2020_Unit3_Summary

2024-03-20 16:51:40

BUAA_OO_2020_Unit3_Summary

写在开头：在本单元的学习中，对于JML相关工具链的使用我一直处于一头雾水的状态，在撰写自己的总结之前，学习了18373109同学的博客，按照他的测试方法进行了本地测试，习得了使用OpenJML及JMLUnitNG工具的方法。

目录

  • BUAA_OO_2020_Unit3_Summary
    • JML语言梳理
      • 理论基础（level 0）
        • 注释结构
        • 规格变量声明
        • JML表达式
        • 方法规格
        • 类型规格
      • 应用工具链
    • OpenJML验证情况
      • Parsing and Type-checking
      • Extended Static Checking
      • Runtime Assertion Checking
    • JMLUnitNG测试（针对MyGroup类）
    • 作业架构设计梳理
    • 作业BUG分析
    • 规格撰写与理解的心得体会

 

JML语言梳理

 

理论基础

JML是用于对Java程序进行规格化设计的一种行为接口规格语言语言，提供了对方法和类型的规格定义手段。

经一个单元的学习使用，个人感觉JML对于代码开发主要优势有以下三点：

（1）开展规格化设计。

（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。

（3）根据规格测试实现，以使测试自动化、系统化、覆盖率可视化。

JML的设计考虑到了未来扩展需要，把语言分成了几个层次。下面对最核心的语言特征level 0进行整理总结。

 

注释结构

JML以javadoc注释的方式来表示规格，每行都以@起头。

有两种注释方式，行注释和块注释。其中行注释的表示方式为 //@annotation，块注释的方式为/* @ annotation @*/。

按照Javadoc习惯，JML注释一般放在被注释成分的紧邻上部。

 

规格变量声明

静态规格变量：//@public static model (non_null) type name;

实力规格变量：//@public instance model (non_null) type name;

 

JML表达式

原子表达式：

关键字 含义
\result 表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值
\old(expr) 表示一个表达式 expr 在相应方法执行前的取值，该表达式涉及到评估 expr 中的对象是否发生变化
\not_assigned(x,y,...) 用来表示括号中的变量是否在方法执行过程中被赋值。如果没有被赋值，返回为true ，否则返回 false ，用于后置条件的约束
\not_modified(x,y,...) 该表达式限制括号中的变量在方法执行期间的取值未发生变化
\nonnullelements(container) 表示container对象中存储的对象不会有null
\type(type) 返回类型type对应的类型(Class)
\typeof(expr) 该表达式返回 expr 对应的准确类型

 

量化表达式：

关键字 含义
\forall 全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束
\exists 存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束
\sum 返回给定范围内的表达式的和
\product 返回给定范围内的表达式的连乘结果
\max 返回给定范围内的表达式的最大值
\min 返回给定范围内的表达式的最小值
\num_of 返回指定变量中满足相应条件的取值个数

 

操作符：

关键字 含义
<: 子类型关系操作符
<==> / <=!=> 等价操作符
==> / <== 蕴含操作符
\nothing / \everything 变量引用操作符
Java定义的所有操作符 同Java

 

方法规格

  • 前置条件

　　　　通过requires子句表示，要求确保其表达式为真才可进行正常行为操作。

  • 后置条件

　　　　通过ensures子句表示，要求确保方法执行后其表达式为真。

  • 副作用限定

　　　　通过assignable或modifiable表示，限定方法能够修改的对象

  • 正常行为与异常行为

　　　　方法规格分为正常行为规格和异常行为规格两种，分别对应`normal_behavior`和`exceptional_behavior`。多种行为间通过`also`子句连接，前置条件不可重叠。在异常行为规格中通过signals子句抛出异常。

 

类型规格

关键字 含义
invariant 不变式，在可见状态下必须满足的条件
constraint 状态变化约束，前序和当前状态之间关系的约束

 

应用工具链

  • OpenJML

　　　　对JML注释的语法及完整性进行检查，包括类型、变量可见性与可写性等检查。（注意其不支持高版本jdk，建议配置JDK 8u102 + OpenJML 0.8.40）

  • JMLUnitNG

　　　　根据JML规格自动生成测试以检查实现。

  • Junit

　　　　单元测试，根据规格自己编写测试代码，提供覆盖率检查功能（但全部覆盖不意味没有bug）。

 

OpenJML验证情况

配置环境为JDK 8u102 + OpenJML 0.8.40

工作区如下图所示：

 BUAA_OO_2020_Unit3_Summary

Parsing and Type-checking

该检查为JML静态语法检查

在cmd中进入工作区，运行如下命令：java -jar openjml.jar -check "$FilePath$" -cp "$Classpath$" -sourcepath "$Sourcepath$" -encoding utf-8

  • -check参数指定检查类型为Parsing and Type-checking
  • -cp参数指定Classpath
  • -sourcepath参数指定源文件目录（可缺省）
  • -encoding参数指定文件编码

据本地测试，课程组提供的规格某些可通过检查，某些则会出现如下图所示的奇奇怪怪的bug：

BUAA_OO_2020_Unit3_Summary

Extended Static Checking

该检查利用Solver对按照JML编写的程序进行简单的静态检查

在cmd中进入工作区，运行如下命令：java -jar openjml.jar -prover z3_4_7 -exec ".\Solvers-windows\z3-4.7.1.exe" -esc "$FilePath$" -cp "$Classpath$" -sourcepath "$Sourcepath$" -encoding utf-8

  • -prover参数指定Solver类型
  • -exec参数指定Solver可执行程序
  • -esc参数指定检查类型为Extended Static Checking
  • 其余参数见上

在对第三次作业中的实现进行该检查时，虽没有出现错误，但是出现了许多Solver无法解析某些运算符、不支持检查某些表达式的错误。由此可见，此功能的开发与目前的开发环境出现脱节，有待更新。

 

Runtime Assertion Checking

该检查对按照JML编写的程序进行简单的运行时检查

在cmd中进入工作区，运行如下命令：java -jar openjml.jar -rac "$FilePath$" -cp "$Classpath$" -sourcepath "$Sourcepath$" -encoding utf-8

  • -rac参数指定检查类型为Runtime Assertion Checking
  • 其余参数见上

对于课程组所书写的规格，openjml的运行检查抛出了各种各样的错误，未能跑通：

 BUAA_OO_2020_Unit3_Summary

BUAA_OO_2020_Unit3_Summary

 

JMLUnitNG测试（针对MyGroup类）

工作区同openjml测试部分，在cmd中进入工作区，依次运行以下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

所得部分测试结果如下：

BUAA_OO_2020_Unit3_Summary

分析测试结果，可见该测试工具存在以下问题：

  • 测试针对单个方法进行，无法联合测试，而本单元作业中为了优化性能设置的cache机制就无法使用该工具测试了，而此部分又为bug的高发区
  • 生成的测试数据情况较为简单，集中于对简单边界数据和空引用的测试，范围有限（一些不符合指导书要求的边界数据可忽略）

对于本单元作业的黑箱测试，以上两种方法显然不如找同学对拍有效，更不必说复杂的工业开发环境了。

 

作业架构设计梳理

 

第一次作业

UML类图如下：

 BUAA_OO_2020_Unit3_Summary

第一次作业架构比较简单，需要设计的部分其实只有某一节点的邻接节点存储方式、与各节点间可达性判断算法。

对于某一节点的邻接节点存储方式，我采用了Hashmap<id,value>的方式进行存储，节省空间而又便于查询。而Hashmap结构也成为了后续作业实现中的高效容器。

而对于各节点间可达性判断算法，由于第一次作业只涉及两点间是否可达判断，并不涉及复杂的图论知识，于是我采用了较之dfs算法面对大多数情况性能更优的bfs算法实现。

复杂度分析如下：

 BUAA_OO_2020_Unit3_Summary

由于第一次作业限制较为宽松，各不同算法间性能差异并不大，都能较好满足要求。

 

第二次作业与第三次作业

第三次作业与第二次作业架构基本一致，只是增添了两个考察算法的函数，故一并分析。

第三次作业UML类图如下:

BUAA_OO_2020_Unit3_Summary

从第一次作业到第二次作业，从主体设计需求来看，拓展了与图的联通分量相关的诸多功能要求，于是我在MyNetwork层次加入了并查集记录联通信息，在MyPerson层次加入了所在群组记录属性inGroup。

另外由于第二次作业中增添了许多基于遍历图节点实现的查询算法，维护查询cache成为了保证性能的必须之策。而维护cache时，最关键的步骤便是判断更新cache的时间节点，以relationSum和valueSum为例，在Group中增减成员或者内部成员加好友的时候都要进行正确的维护操作。

第三次作业则主要考查了连通分量数量计算、最短路径查找、极大点双连通分量求解三个算法。在并查集的基础上维护连通分量数量属性成为了轻而易举的事，而对于最短路径查找我则使用了数据结构课上学习的迪杰斯特拉算法。

最为困难的算法是极大点双连通分量求解，为了保证性能，我学习使用了tarjan算法，并在tarjan算法执行前通过并查集检查两者是否相连以节省时间。

复杂度分析如下：

 BUAA_OO_2020_Unit3_Summary

BUAA_OO_2020_Unit3_Summary

BUAA_OO_2020_Unit3_Summary

总的来说，就架构设计及算法实现层面，我在本单元中做的还算优异，性能表现比较出色。

 

作业BUG分析

第一次作业的实现较为简单，算法的限制程度也比较宽松，未出现bug，互测屋内其他成员除个别看错规格外也没出现什么错误。

第二次作业中测试的重要性突显，相较于各种JML工具，对于通过课上测试最有效的方法其实是找高水平同学对拍。在课下我与多名同学进行了对拍以验证自己的程序，最终顺利通过了强测与互测。而在互测的过程中也依赖对拍器hack到了不少课下测试不充分的同学。

第三次作业的测试策略与第二次作业没有区别，依旧是对拍，不过由于自动生成数据的针对性不够强，我在本次强测过程中出现了本单元唯一的一个bug，便是age总和较大时炸int。其实这一点我在编写程序时考虑到了，但由于对于java类型转换的机制理解出现了偏差导致错误。分析其原因还是因为自己经过前两次作业的顺利通过后掉以轻心，没有进行充足的边界情况测试。

 

规格撰写与理解的心得体会

本单元的学习为我们带来了一种全新的程序设计模式——规格化设计，这一设计模式使我受用最深的地方有两点。

第一点在于设计与实现分离，经历了前两单元作业的“无中生有”、“暗度陈仓”、“凭空想象”，这一单元作业照规格写实现的设计过程显得无比幸福，规格化设计对于开发过程的高效优化对我产生了巨大的冲击，让我不仅渴望以后都能在这样的条件下进行开发工作。

另一点在于形式化的规格所带来的严格的形式化验证，基于规格写实现，不仅使我们的开发设计行之有方，亦使设计完成后的测试工作有迹可循。不再像前两单元作业测试时集思广益、同学们你想一个我想一个来测试隐藏bug，规格化设计下测试的边界情况似乎变得明朗直观起来。虽然由于JML相关工具链的开发还不够完善便捷，最终我仍然选择了对拍的方式进行测试。但是在我的脑海中，已经有了对于规格化设计下高覆盖、高自动化、高压力测试方法的可行判断。

上一篇：BUAA-OO Unit3 JML规格


下一篇：OO Unit3 单元总结