OO第三单元总结

一、JML理论基础与工具链梳理

使用：

jml有类型规格和方法规格。

类型规格指针对Java程序中定义的数据类型所设计的限制规则，一般而言，就是指针对类或接口所设计的约束规则。课程中的重点是不变式invariant和状态变化约束constraint。不变式invariant是要求在所有可见状态下都必须满足的特性，而状态变化约束constraint对对象状态的变化进行约束。

方法规格分为的正常功能行为和异常行为，即normal_behavior和exceptional_behavior。每一种行为，都有前置条件，副作用范围限定和后置条件三部分。

requires子句定义该方法的前置条件，表示要求调用者确定条件为真，对于方法中不同的表现可能有不同的前置条件。

assignable跟着副作用范围限定，会列出这个方法能够修改的类成员属性，除了自己定义的类成员之外，还有可能存在两种关键词，如/nothing，代表这个方法不对任何成员属性进行修改，以及/everthing，即作用域内可见的所有类成员变量和方法输入对象都可以赋值或者修改。

ensures子句表示后置条件，表示要求实现者确定此方法执行返回结果满足后置条件，同样的，多个条件可以用逻辑符号进行连接。

工具链：

常用的JML工具主要有OpenJML（对JML进行语法检查、配合Solver进行简单的静态验证、以及运行时验证）、JMLUnitNG 、JMLUnit（自动化单元测试生成工具）等等。http://www.eecs.ucf.edu/~leavens/JML//download.shtml

二、SMT Solver

报错不断，无法正常使用。

三、JMLUnit

jmlunit貌似不支持forall，exist等复杂指令，无法对Group接口生成测试用例。

四、架构设计

第一次作业：

完全按照课程组提供的jml来编写，isCircle部分使用并查集，简单好写效率高。

第二次作业：

大部分方法与第一次作业完全一样，但是对于容器进行了修改，所有的遍历查询都改成了HashMap查询，但是遍历统计部分仍旧使用Arraylist，因为hashmap遍历较慢，并且这次作业内存充足。

本次作业中新增了较多的查询方法，这些方法如果完全按照jml来写成双循环，强测不知道会怎么样，互测时是会被刀烂掉的，所以此处用动态维护的方式来实现query relationsum和query Valuesum。

第三次作业：

第三次主要麻烦的两个新增方法，查询最短路，查询点双联通。

点双联通我主要使用了tarjan算法，目测比暴搜还好写。

最短路我一开始写了spfa，后来怕助教顺手卡一手，就改成了堆优化dij。

五、bugs

第一次作业强测爆炸，出现了一个十分低级的错误，并且第一次作业的时候没有进行进一步测试。

第二次作业，搞了个数据生成和对拍器，强测无bug。互测的时候出现过有的同学忘了在查询平均和方方差的时候判断除数是否为0,导致异常。双循环也在互测中被卡，还有我用随机生成的数据发现了一些同学的WA。

第三次作业，互测时发现有同学在判断双联通时用tarjan算法忘了特判只有两个点的情况。还有同学qsl写错了，被随机数据刀了。

在强测中，我有个点TLE了，跑了2.1s，在bug修复中，再次提交相同的代码，结果只有1.4s。。。目测评测机在高压下速度慢了不少，由于本人完全不懂这种大规模评测机的部署方法，也不知道应该怎么优化比较好，希望还是能对每个任务保证一定的cpu使用量。同样的数据，在本地测试的时候只跑了0.75~0.95s，本地的cpu为i5-8300h@3.7GHz，我随后将频率压到了1.0GHz，结果运行时间到了2.5 ~ 3s。所以在进行本地测试的时候最好将频率压低到2.1Ghz左右，模拟和评测机相接近的性能环境。

六、心得体会

学习jml让我们体会到了规格化设计，形式化验证，和契约式编程的奥妙。但是实际上感觉本单元强推的一种基于junit的测试在这几次作业的情形下并不是很方便，老一套的随机数据生成+对拍依然最有效。并且jml的工具链很不完善，使用局限性很大，在搜索引擎中搜索jml蹦出来的大部分都是学长们的博客，让我不禁有些怀疑jml是否在开发中大规模应用，是否jml是个已经过时且不太完善的技术...