JML理论基础
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言（Behavior Interface Specifification Language，BISL），基于Larch方法构建。一般而言，jml有两种主要的用法（事实上在本单元的实验课中我们也都练习到了）：
（1）开展规格化设计。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。
JML以javadoc注释的方式来表示规格，每行都以@起头。主要的内容是由jml表达式来实现的。
原子表达式
\result表达式：表示一个非void类型的方法执行所获得的结果，即方法执行的返回值。\result表达式的类型就是方法声明中定义的返回值类型。
\old(expr)表达式：用来表示一个表达式expr在相应方法执行前的取值。
\not_assigned(x,y,...)表达式：表示括号中的变量在方法执行过程中是否被赋值。
\not_modified(x,y,...)表达式：与\not_assigned(x,y,...)类似，表示括号中的变量在方法执行期间取值是否发生变化。
\nonnullelements(container)表达式：表示container对象中存储的元素不会有null。
\type(type)表达式：返回type对应的类。
\typeof(expr)表达式：与\type(type)类似，返回expr对应的准确类型。
量化表达式
\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素都满足相应的约束。
\sum表达式：返回给定范围内的表达式的和。
\product表达式：返回给定范围内的表达式的连乘结果。
\max表达式：返回给定范围内的表达式的最大值。
\min表达式：返回给定范围内的表达式的最小值。
\num_of表达式：返回指定变量中满足相应条件的取值个数。
集合表达式
集合构造表达式：可以在jml中构造一个局部集合，类似于离散数学中的数学表达。
操作符
除去数学运算符和逻辑关系运算符，还有以下几种：
子类型关系操作符：E1<:E2，表示类型E1是E2的子类型。
等价关系操作符：b_expr1<==>b_expr2，表示两个表达式等价。
推理操作符：b_expr1==>b_expr2，表示第一个表达式可以推出第二个表达式。
变量引用操作符：\nothing表示空集，\everything表示全集。
方法规格
前置约束：使用requires语句描述，表示方法执行的一些要求约束。
后置条件：使用ensures语句描述，表示方法执行结果的一些约束。
作用范围：使用assignable语句描述，表示方法可以修改的变量。
对于前置条件与后置条件通常有两种类型，分别是正常执行\normal_behavior和异常\exception_behavior两种类型，对于异常行为的结果，通常使用\signal语句描述。
类型规格
不变式invariant：要求可见状态下都满足的约束，描述数据状态应该满足的要求。
约束constraint：描述状态变化的满足的约束。
工具链使用
SMT Solver
SMT Solver是一种验证理论，利用Openjml可以验证JML文档规格语法。但本人在配置使用的过程中发现报错不断，没能成功运行，遂放弃使用。
JMLUnitNG
JMLUnitNG可以基于JML规格来自动生成测试样例并自动进行测试的工具。本人在配置时出现这样的报错:
暂时原因还没有找到。但看同学使用的实际体验很差，只会对一些边界数据进行测试，如int的最大值，最小值，0，或是null等等，难以提供有效信息，并不能满足测试的需求。相比较而言不如junit单元测试自行构造测试用例。
作业分析
架构分析：
本次实验官方已经给出了基本的架构。下面以第三次作业为例：
具体方法分析：
在这里就讲一下经过第三次作业bug修复之后的最终版的一些方法（写作业的时候还是优化不力，希望以此为戒，学习一下其他同学的优化方法）：
1、实测用一种容器来存储数据具有局限性。hashmap在查找方面性能显著，但在遍历的时候由于需要使用迭代器故效率较差，arraylist遍历时效率较高，查找时效率较低，故可以使用两种容器来存储节点，取长补短可以提高效率。
2、有关缓存方面，可以针对group中一些变量做记录，设置dirty位，这样可以大大提高效率。诸如像agemean、agevar之类的。
3、本次作业中只有添加节点与边，固采用并查集可显著优化诸如iscircle（这方法的名字很有迷惑性，其实是判断两个点是否连通的）、queryblocksum（求连通块数目）等方法。
4、在queryminpath中使用堆优化的dij算法，java自身的PriortyQueue使的实现起来很方便。
5、querystronglink我直接采用了遍历删除点，判断是否连通来判断
测试分析：
BUG:本单元的作业说实话我有点凉凉，前两单元还比较顺利结果在这一单元翻车了。自己出现的bug除了第一次作业中对规格的理解有误意外其他的全是CPU超时了。优化的方法已经在上面的测试分析中写了，我自己的实现相较而言问题就的确很大了。可能自己心态比较好吧，毕竟这次单元也确实学到了很多东西（之前学的挺渣的关于图的数据结构又学了一遍感觉还不错）。
测试：自己本地的测试简单地使用了junit进行功能实现测试，很遗憾的是压力测试方面不过关。互测中针对像使用缓存但从组里删人之后未判断组中无人导致更新平均值时出现除以0的问题、优化方面的问题等进行hack。
心得体会：
本单元作业的负担确实小了很多，在规格的指引下我们只需要完成规格的要求即可满足正确性（但这是远远不够的，性能也很重要，所以一定要认真优化，不然就是满屏幕的CTLE让人头皮发麻），也确实认识到了自己对于性能优化、算法设计方面还有很长的路要走。我自己也对这种“契约式”设计的理解更加的深刻了，调用者与被调用者一起制定的规范保证了程序的完美运行。JML对于以后团队协作开发程序有很大的帮助，使得代码具有较好的可维护性。
原文：https://www.cnblogs.com/2020-cuaner/p/12925082.html