【作业3.0】OO第三单元作业总结

OO第三单元总结

目录

• OO第三单元总结
  • 1. JML理论基础和应用情况
    • JML简介
    • JML语法
      • 方法规格
      • 类型规格
      • 表达式语法
      • JML应用工具链
  • 2. 部署SMT Solver
  • 3. 部署JMLUnitNG进行测试
  • 4. 第三单元架构设计
    • 第一次作业
      • 测试结果
      • 设计架构
    • 第二次作业
      • 测试结果
      • 设计架构
    • 第三次作业
      • 测试结果
      • 设计架构
  • 5. 代码实现的bug和修复情况
    • 第一次作业
    • 第二次作业
    • 第三次作业
  • 6. 规格撰写和理解的心得体会
  • 7. 总结

1. JML理论基础和应用情况

JML简介

JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言(Behavior Interface Specification Language，BISL)，基于Larch方法构建。BISL提供了对 方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。JML主要由Leavens教授在Larch上的工作，并融入了Betrand Meyer， John Guttag等人关于Design by Contract的研究成果。近年来，JML持续受到关注，为严格的程序设计提供了一套行之有效的方法。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式来检查代码实现对规格的满足情况。——来自OO课程组JML指导书

互联网上关于JML的资料介绍很少，很多都是参与OO课程的往届学长学姐留下的资料。可能说明了JML在工业界的应用没有同类规格语言那么广泛，但作为面向初学面向对象课程的我们，JML语法接近JAVA原生语法、易于上手的特点比较适合我们对基于规格的编程进行学习。

经过本单元的学习，我认为行为接口规格语言的用处主要有以下几点：

1. 为编程人员提供统一、无二义的规格和需求。
2. 便于对各个模块的功能进行解释，不必阅读代码即可理解其功能，从而便于展开测试和修改。
3. 提供了底层实现的抽象，便于检查整个工程项目的功能是否健全。

JML语法

JML行为接口规格语言使用Java注释进行编写，具体的内容写在//@ annotation或/*@ annotation @*/注释块中。JML语言一般以一个方法或一个成员变量为表示单元。JML注释写在和对应的方法或属性紧邻的上方。下面分方法规格、数据规格分别对JML语法进行介绍。

方法规格

方法规格由以下几部分组成：

• 行为说明：public normal_behavior用来表示满足后续条件的行为为正常行为，无异常抛出；public exceptional_behavior表示满足后续条件的行为为异常行为，可能有异常抛出。满足各个行为说明的条件之间不可有交叉；各个行为说明之间使用also字句相连接；若只处理一种行为，则public normal_behavior可以省略。不满足任何行为说明的输入，其返回值和造成的结果是未定义的。以下内容均是单个行为说明中的组成部分。

• 前置条件：使用requires P语句表示，即方法的调用者应当保证谓词P为真，否则对于该输入，方法不按照对应的规格进行输出。

• 后置条件：使用ensure P语句表示，当输入满足前置条件时，方法应当保证谓词P为真。

• 副作用范围限定：使用assignable V或modifiable V语句表示，表示变量V在执行后可能被改变。若方法不修改任何变量，则该方法为pure方法，可在方法名之前用/*@ pure @*/加以表示。

• 异常说明：signals (***Exception e) b_expr;表示满足当前异常行为使得b_expr为真时，抛出对应的异常。另一种表示为signals_only直接抛出对应的异常。

类型规格

类型规格由以下几部分组成：

• 不变式：invariant P表示在所有可见条件下均需要满足的特性。
• 状态变化约束：constraint P之中的P对当前状态和前序状态之间的关系进行约束。

表达式语法

JML的语法和Java语法有很多互通之处，下面主要对JML中新增的一些表达式语法进行说明。

• JML的语句以分号;作为结束标志，一个注释块由若干语句组成。
• 原子表达式：
  • esult：非void方法的返回值
  • old(expr)：表达式在方法执行前的值。对于引用类型，只判断引用本身有没有发生变化，所指向的实体内容则无法判断。
  • ot_assigned(x, y, ...)或 ot_modified(x, y, ...)：限制括号中的变量在方法执行过程中未被赋值/未被改变。
  • onnullelement(container)：限制container容器对象中不含null元素。
  • ype(type)或 ypeof(expr)：分别返回对应的Class和expr的准确类型。
• 量化表达式：
  • forall(type elem; P; Q)：全称表达式，对于所有满足谓词P的elem，都有谓词Q成立。
  • exists(type elem; P; Q)：特称表达式，存在一个满足谓词P的elem，使得谓词Q成立。
  • sum(type elem; P; f(elem))：返回所有满足谓词P的f(elem)的和。
  • product(type elem; P; f(elem))：返回所有满足谓词P的f(elem)的连乘。
  • max(type elem; P; f(elem))或min(type elem; P; f(elem))：返回所有满足P的f(elem)中的最值。
  • um_of(type elem; P; Q)：返回满足条件的变量个数
• 操作符：
  • E1<:E2：子类型关系操作符，E1是E2的子类型
  • EXP1<==>EXP2：等价关系操作符，EXP1与EXP2等价
  • EXP1==>EXP2：推理操作符，EXP1可推出EXP2
  • othing、everything：空集、全集

JML应用工具链

基于JML规格语言的工具有很多，Iowa State JML提供了JML的断言检查和编译器jmlc，可将JML转化为运行环境。文档生成器jmldoc可生成提供了更加丰富信息的JML文档。另外，还有JMLUnit，它可以根据JML生成对应的JUnit测试代码。

很多独立的组织都发布了基于JML规格语言的工具，包括以下内容：

• ESC/Java2 [链接]：一个JML静态检查的扩展程序，可以根据JML规格执行更严格的静态检查。
• OpenJML ：自称为ESC/Java2的继承者。
• Daikon：动态不变式生成器。
• KeY：提供了一个动态开源的，基于JML的定理证明工具。同时在Eclipse中有内置高亮扩展工具。
• Krakatoa：一个基于Why平台，运用Coq作为检查辅助的静态检查工具。
• JMLEclipse：一个面向Eclipse的JML集成开发环境，对JML语法进行检查。
• Sireum/Kiasan：一个具有代表性的、执行式的JML语言的静态分析工具。
• JMLUnit：一个根据JML规格语言生成JML测试代码的工具。
• TACO：一个开源的静态检查工具，检查Java程序是否符合其对应的JML规格。
• VerCors verifier：不详。

2. 部署SMT Solver

上述的OpenJML的官方包中含有了SMT Solver工具，笔者利用这一工具对课程组提供的Person.java和Group.java两个接口中的JML规格进行静态检查，检查结果如下：

• Person.java没有问题出现。
• Group.java提示找不到Person对象，参考了往届OO同学和本届其他同学的博客，仍未发现解决方案。

（检查结果如图所示）

3. 部署JMLUnitNG进行测试

JMLUnitNG可以根据JML规格自动生成测试数据进行测试，由于本单元作业要求提交的代码中不包含规格本身，因此我对做测试的代码进行了修改，即将代码和规格都放在Group.java和Person.java文件中（将MyGroup、MyPerson中的相关声明做修改）。然后使用JMLUnitNG官方包进行测试。

• 文件放置：源代码放置在JMLUnit文件夹中，测试包在本次作业的根目录（如图）

• 执行代码：

   java -jar jmlunitng.jar JMLUnit/*.java # 生成测试源文件
   javac -cp jmlunitng.jar JMLUnit/*.java # 编译测试源文件和待测文件
   java -jar openjml.jar -rac JMLUnit/*.java # 生成测试程序
   java -cp jmlunitng.jar JMLUnit/Group_JML_Test # 执行测试程序
  

• 执行结果：我将Group中的所有方法检测了一遍，全部结果较多，不便全部展开，每个方法只放几个样例。可以看出，出错的样例大多是超过了int上界，或者是对null对象、0等边界值没有进行适当的处理（因为为了简化操作，对应的异常直接抛给了JVM）。

4. 第三单元架构设计

第一次作业

测试结果

我轻松通过了中测，以为万事大吉，然而发现自己没有进入互测的时候，内心是崩溃的；强测只有10分。

原因非常简单而值得反思：isCircle方法没有进行基本的判断，陷入了死循环。

设计架构

我第一单元的作业完全将JML规格“直译”为代码，除了isCircle方法使用了BFS进行搜索，其他没有任何架构创新（然而这个方法还写出了bug。。。丢死个人）。

值得注意的是，本次作业由于直译JML为Java代码，给后续的迭代造成了诸多隐患：

• getPerson方法使用遍历的方式进行搜索（直到第三次作业debug阶段才改过来。。。）
• 所有查询方法每次都做遍历，没有缓存结构。
• 使用了很多contains+getPerson组合。事实上这样将进行两次遍历，contains遍历中得到的结果没有被很好的利用。因此，我认为这也是盲目“直译”JML的一个巨大坑点。contains方法应该只适用于需要判断person是否存在而不需要得到person对象的时候，这样的场景及其特殊，在本单元目前的所有方法中，都没有这样的场景存在，直接使用getPerson+判断是否为null的方法才是正解。

唯一对架构进行的扩展，是在MyPerson中添加了Person getAcquainance(int index)方法，用来获得第index个熟人。这样即可避免NetWork在寻找熟人时需要反复遍历的问题，MyPerson将acquaintance成员变量以提供下标的方式部分公开给MyNetWork，简化了代码而不带来破坏数据的危险。

UML类图如下：

第二次作业

测试结果

吸取上一次作业的教训，我对这次作业的代码进行了充分的黑箱测试，也对contains+getPerson这个做无用功的设计缺陷进行了修改。但是，测试结果再次让我失望，只有20分。出现了两个大问题：

• getAgeVar计算方差需要得到组内的人数，我没有对人数为零的特殊情况进行判断，这是严重的问题，说明我当时没有认真研读JML规格。值得深刻反省！但这同时也暴露出另一个问题：我在写完代码后使用自己编写的评测机，和其他同学的代码作比对，互相检查错误，在数据量很大的情况下，也没有检查出这一错误。正是因为数据生成器生成的样例都是数据量很大，才没有能够检测出组内人数为0的时候，可能会出现除零错误的问题。这一次作业我也进行了JUnit白箱测试，但很显然，覆盖仍然不够全面。
• 修改了上述错误之后出现CTLE的问题。在我对我的代码进行黑箱测试的时候，我注意到我的qnl方法的时间消耗比其他方法高出20倍左右，因此，即使限制qnl指令的数目，对这个方法进行优化，也是这次作业算法优化的重中之重。因此，我将全部精力都放在了这个方法上，而没有想到应当在各个方法中尽可能多地使用缓存解决问题。在很多我最初看来耗时很少的方法，我都使用了直接查询的方法。

设计架构

尽管还是出了很多问题，这次作业我也进行了很多架构上的改变：

• 完全放弃contains方法的使用，改为getPerson+检查是否为null的方法。
• qnl建立一个姓名排序的链表，每当有人加入的时候，使用按序插入的方法直接给定其在链表中的位置。查询name_rank的时候，遍历这个姓名顺序表即可。这个方法既避免了直接遍历所有成员进行查询所造成的O(person_num * name_avg)时间复杂度，又避免了直接给每个人建立排名缓存的方式，在加入新人的时候需要全部重新计算排名的麻烦。
• 对于需要getPerson两个人的情况，在getPerson第一个人之后先判断其是否为null，如果为null则直接抛出异常，然后再进行第二个人的检索。在人数很多的情况下，出现异常ID为小概率事件，从概率的角度分析，这样可以省去一整个人的查询时间。

UML类图如下：

第三次作业

测试结果

本单元作业没有再次出现重大错误，但强测的14-16个点出现了略微超时的问题。互测中被同学找到了两个bug，是qsl方法中对于割点判断出错的bug。

设计架构

这次作业和前两次不同，NetWork中最后几个方法完全无法用JML直译的方法进行判断了，需要另外构建算法进行代码的实现。

• queryMinPath方法，即两点最短路径问题。这一方法可直接采用单元最短路径求解的经典方法——Dijkstra算法进行求解。算法的主要思想是：1. 将所有的点标记为三种状态：未遍历到、已遍历到但未确定最短路径、已确定最短路径。2. 从当前点（是已确定最短路径的点）出发，将所有邻接点的“临时最短路径”更新为当前点的最短路径长度+当前点到邻接点的距离（若这个值大于已有的临时最短路径，则不更新）。3. 从所有已经有“临时最短路径”的点中选取值最小的点，这个点的最短路径已经确定，将其作为当前点，重复1-3。
• queryBlockSum方法，这个方法需要求NetWork中连通分量的数目。其他很多同学都使用了并查集的方法进行解决，我直接使用一次BFS遍历+缓存的方式实现。每次调用addPerson方法时，缓存值+1（因为直接多了一个连通分量），每次调用addRelation方法时，再进行一次BFS遍历。这样的实现，在addPerson和addRelation和查询方法分开的时候很高效，但若各种指令均匀分布时，可能效率没有并查集那么高。
• queryStrongLinked方法，这是求点双联通分量的方法，也是这次作业最令我费神的地方。高工的数据结构理论讲得很浅，我的基础也很不扎实，关于双连通分量的内容事先完全不知道。最初我想到了两次BFS/DFS的方法，第二次遍历时不经过第一次遍历过的节点。但这种方法存在着巨大问题，没有抓住问题的实质，当以第一次遍历恰好遍历到所有关键节点时，第二次无论如何也不可能找到另一条路径。解决问题的关键在于排除路径上的割点。Tarjan算法提供了计算割点的算法，但我一直没有理解算法中使用的三个数组的意义。因此，我最终采用了遍历第一条路径上的所有点，检查是否有割点的方法。

UML类图如下：

5. 代码实现的bug和修复情况

第一次作业

1. isCircle方法死循环：由于BFS遍历对于结束时刻的判断和常规BFS有出入（优化考虑），当存在多个联通分量时，BFS遍历无法终止，陷入死循环。debug时将出现CTLE的样例进行测试，可立即发现死循环的问题，定位到错误点时，将终止条件修改，即可解决这一bug。

第二次作业

1. 除零错误：由于我初次代码实现时没有认真阅读JML的规格，getAgeVar方法没有判断组内人数为0的情况，导致了大范围的错误。这一错误在强测后显得十分明显，但由于我在本地进行黑箱测试时完全陷入了另一个极端，没有考虑可能出现类似的问题。
2. CTLE：第二次作业由于没有对时间进行全面的优化，导致强测数据几乎全部超时。在注意到题目对空间的要求及其松散，而时间要求相对严格，我采用了将所有非点对点查询方法均设置缓存的方法来提高时间效率（但这是空间换时间的行为）。

第三次作业

第三次作业没有严重问题，14-16三个点略微超时。对比其他同学的代码，发现我的getPerson方法仍然使用了遍历查找的方式，改为使用HashMap<id, Person>的方法可以明显提高时间效率。

6. 规格撰写和理解的心得体会

首先说一下自己对于规格的主观感受，我认为JML规格的作用介乎代码和自然语言之间，和代码相比可读性提高了很多，和自然语言相比，不存在二义性，逻辑紧密严谨。以JML为代表的规格语言将是程序开发中的一件利器。

然而，成事在人。我认识到了JML的优势，可不幸的是对这种语言产生了过分的依赖，没有分清规格和代码的关系。经过这一单元的作业，我甚至发现规格和代码是相互分离的两种存在。规格只是作为一种理解程序职责的一种“接口”，是和算法、架构、代码实现相互独立的。

JML作为一种表达程序功能的语言，在这单元作业中代替了指导书的部分作用，这是我经历的编程方式的一个重大转变，基于规格进行代码实现更加严谨高效。我认为这样基于规格的代码实现能够在多人协作方面发挥更多的左右，或许在下一届的OO课程中可以加入利用规格进行分工协作的任务。

在JML规格的书写方面，我觉得自己需要进行更多的训练才能熟练掌握，和程序实现不同，编写规格的时候更需要对于工程的各方面功能有总体性的把握，对于逻辑的严谨性、闭环性的掌握要更多，而对于算法、实现细节这些要少考虑甚至需要刻意地排除这些考虑对于规格编写的干扰。

7. 总结

这一单元的作业有很多的遗憾，但是也有特别多的收获，我相信这样的经历能够在今后发挥更多的作用。基于规格进行总体功能的思考，按照规格进行程序实现，是工程架构和实现细节相统一的桥梁。我将利用这一利器在今后的编程中攻克更大更复杂的项目。