一、理论基础
注释结构
JML以javadoc注释的方式来表示规格，每行都以@起头。
行注释：//@annotation
块注释：/* @ annotation @*/
JML表达式
JML的表达式是对Java表达式的扩展，新增了一些操作符和原子表达式。
原子表达式
（1） esult表达式：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。 esult表达式的类型就是方法声明中定义的返回值类型。
（2）old(expr)表达式：用来表示一个表达式expr在相应方法执行前的取值。针对一个对象引用而言，只能判断引用本身是否发生变化，而不能判断引用所指向的对象实体内容是否发生变化。
（3） ot_assigned(x, y, ...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。如果没有被赋值，返回为true，否则返回false。
（4） ot_modified(x, y, ...)表达式：该表达式限制括号中的变量在方法执行期间的取 值未发生变化。
（5） onnullelements(container)表达式：表示container对象中存储的对象不会有 null。
（6） ype(type)表达式：返回类型type对应的类型(Class)。
（7） ypeof(expr)表达式：该表达式返回expr对应的准确类型。
量化表达式
（1）forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
（2）exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
（3）sum表达式：返回给定范围内的表达式的和。
（4）product表达式：返回给定范围内的表达式的连乘结果。
（5）max表达式：返回给定范围内的表达式的最大值。
（6）min表达式：返回给定范围内的表达式的最小值。
（7） um_of表达式：返回指定变量中满足相应条件的取值个数。
集合表达式：可以在JML规格中构造一个局部的集合(容器)，明确集合中可以包含的元素。
操作符
（1）子类型关系操作符：E1<：E2，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。如果E1和E2是相同的类型，该表达式的结果也为真。
（2）等价关系操作符：b_expr1<==>b_expr2或者b_expr1<=!=>b_expr2，其中b_expr1和b_expr2都是布尔表达式，这两个表达式的意思是b_expr1==b_expr2或者b_expr1!=b_expr2。
（3）推理操作符：b_expr1==>b_expr2或者b_expr2<==b_expr1。对于表达式b_expr1==>b_expr2而言，当b_expr1==false，或者b_expr1==true且b_expr2==true时，整个表达式的值为true。
变量引用操作符
（1） othing指示一个空集。
（2）everything指示一个全集。
方法规格
（1）前置条件(pre-condition)：是对方法输入参数的限制，通过requires子句来表示。
（2）后置条件(post-condition)：是对方法执行结果的限制，通过ensures子句来表示。
（3）副作用范围限定(side-effects)：assignble表示可赋值。modifiable则表示可修改。
（4）signals子句
1、signals (Exception e) b_expr：当b_expr为true时，方法会抛出括号中给出 的相应异常e。
2、signals_only：后面跟着一个异常类型，不强调对象状态条件，强调满足前置条件时抛出相应的异常。
类型规格
（1）不变式(invariant)：要求在所有可见状态下都必须满足的特性，语法上定义invariant P，其中invariant为关键词， P 为谓词。
（2）状态变化约束(constraint)：对前序可见状态和当前可见状态的关系进行约束。
二、工具链
这里对jml第二次作业进行验证。为了测试方便，可以把官方包的源代码复制到工程的src文件夹下。
（1）部署OpenJML
真正得到官方支持的插件是OpenJML的Eclipse版插件，Eclipse上的OpenJML插件可以输出验证错误信息，提供问题代码高亮，提供全推导过程，甚至能够在代码中给出对有问题的代码的反例。因此我们可以用Eclipse打开项目，并在Eclipse上部署OpenJML和SMTSolvers。
在安装之前，需要设置Available Software Sites，在Window->Preferences->Install/Update->Available Software Sites中添加openjml的网址http://jmlspecs.sourceforge.net/openjml-updatesite/ ，如图
在Help->Install New Software中，在work with中输入openjml，把下面的OpenJML和SMTSolvers都选上，然后安装（如果安装好之后出现各种各样的报错，安装版本低的openjml就可以了）
安装好之后，Eclipse能检查jml规格中的语法错误并提供高亮，比如
当改正这个语法错误之后再保存，高亮消失。
（2）部署SMT Solvers
目前这个情况，直接进行JML->Static check貌似会报错，此时在Window->Preferences->OpenJML->OpenJML Solvers中，设置z3_4_3为external并设置路径为z3-4.7.1.exe的路径（应当可以在eclipse安装目录pluginsorg.jmlspecs.Solvers_1.4.0Solvers-windows中找到），此时再进行JML->Static check应该就可以了。
这里对jml第二次作业的MyGroup类进行测试，结果如下：
点开getAgeMean，getAgeVar，getRelationSum，可以发现这里举出了一些反例（以极端数据为主）说明了错误的情况，报错的原因可能是程序没有特别考虑极端数据的情况，或者规格中没有指明参数的取值范围，导致z3认为取值范围和int一样。
（2）部署JMLUnitNG
下载jmlunitng.jar之后，为了测试方便，可以把jmlunitng.jar复制到工程的src文件夹中，然后在cmd中依次执行以下命令
java -jar jmlunitng.jar MyGroup.java
javac -cp jmlunitng.jar *.java
java -cp jmlunitng.jar MyGroup_JML_Test
（最开始执行第一步的时候产生了报错，报错主要是说new HashMap<>()的尖括号中应当有数据类型，补上即可）
第一步产生了大量的测试代码，第二步对源代码和测试代码进行编译，第三步运行测试程序，输出结果如下：
这里只有hasPerson(null)这里出现了问题，主要是因为hasPerson没有考虑参数为null的情况。尝试进行改正，在传入参数为null时返回false，并再次进行验证，结果正确。
观察这个测试用例，可以发现JMLUnitNG只对极端数据（0，null，±2147483647这样的）进行测试，具有一定的局限性。
三、程序设计
第一次作业
第一次作业比较简单，要实现 person 类和简单社交关系的模拟和查询，仅需实现Person与Network类，重在理解清楚jml规格，并严格按照规格写出具体实现。唯一要注意的是把控好iscircle的复杂度，以免超时，我采用的是bfs算法，为O（nlogn）的复杂度。
MyPerson：
使用HashMap<Integer,Integer> id2value结构保存相识的人的id与具体对象，从而由id能迅速找到对应的人。
MyNetwork：
使用HashMap<Integer,MyPerson> id2person结构保存社交关系网中的id与对应的人，从而由id能迅速找到对应的人。
第二次作业
第二次作业在第一次的基础上新增了 Group接口，并且添加了一些与group内部属性相关的查询方法，由于标程复杂度瓶颈为O(n*group_sum)，若在此处不加以设计，在每次查询时重新进行计算，很容易使方法为O（n**2）复杂度，这样在多次查询时就会有超时风险。同时要注意平均值和方差的计算精确度，我原先使用了方差公式D（x）=E（x**2）-（E（x））**2，与规格不符使程序出现bug，所以要严格按照JML规格中的定义进行计算。
本次作业中，我使用relationSum、valueSum、conflictSum、ageSum、ageVar来保存Mygroup内部相关属性，同时在调用addPerson、addRelation、addtoGroup时分别对其进行更新，可以大大减小程序运行时间。
MyPerson：
使用HashMap<Integer,Integer> id2value结构保存相识的人的id与具体对象，从而由id能迅速找到对应的人。
MyNetwork：
使用HashMap<Integer,MyPerson> id2person结构保存社交关系网中的id与对应的人，从而由id能迅速找到对应的人。
MyGroup：
使用HashMap<Integer,MyPerson> id2person结构保存group中的id与对应的人，从而由id能迅速找到对应的人。
使用HashMap<Integer,MyGroup> id2group结构保存关系网中的id与对应的Group，从而由id能迅速找到对应的组。
第三次作业
第三次作业在第二次的基础上增加了从group中删除person操作、查询最短路径、连通块个数、强相关关系等有关图的操作以及关系网中的借钱操作。由第二次作业程序的可拓展性，我在delFromGroup中也同时更新MyGroup的相关属性，查询最短路径与强相关关系均使用了dfs，对于最短路径我用HashMap<Integer,HashMap<Integer,Integer>> mindis结构来保存目前已找到的最短路径，每次查询时先查看此结构中是否存在id1与id2的最短路径，若不存在，则使用dfs遍历并保存所有得到的最短路径，该结构在addRelation时需要清空，对所有最短路径进行重新计算。查询连通块操作则是用blockno属性保存块数，在addRelation时若id1与id2无通路，blockno减一，否则不变，而addPerson时需要对其加一。
MyPerson：
使用HashMap<Integer,Integer> id2value结构保存相识的人的id与具体对象，从而由id能迅速找到对应的人。
MyNetwork：
使用HashMap<Integer,MyPerson> id2person结构保存社交关系网中的id与对应的人，从而由id能迅速找到对应的人。
MyGroup：
使用HashMap<Integer,MyPerson> id2person结构保存group中的id与对应的人，从而由id能迅速找到对应的人。
使用HashMap<Integer,MyGroup> id2group结构保存关系网中的id与对应的Group，从而由id能迅速找到对应的组。
使用HashMap<Integer,HashMap<Integer,Integer>> mindis结构保存已找到的最短路径。blockno为连通口个数。
使用HashMap<Integer,Integer> id2money结构保存id及对应的money。
HashSet<Integer> dfsVisited结构dfs算法。
strongLinkedFlag标记强相关关系。
四、bug发现及修复
在第二次作业中易出现bug的地方为方差公式的变形以及除0错误，对于方差的计算我原本使用方差公式，还好在严格比对JML规格的时候发现了该错误，最后在公测和互测中均未被找到bug。
第三次作业有部分同学在判断qsl时出现失误，误用双dfs或者bfs，同时在实现minPath和strongLinked时，不考虑方法性能，最后出现超时。
五、体会与感想
本单元主要学习JML规格，具体来说包含两方面的内容：根据需求撰写规格，以及根据规格实现代码。JML是基于"契约式编程"的一种规格描述语言，通过查阅JML手册以及参考已有规格，为一个方法写一份简单的规格描述难度并不大，而想要针对某个特定项目写一份完整、严谨的规格却是十分困难的。但 JML 的好处在于，测试人员能够从设计层面直接判断方法的正确性，而不用花费大量时间阅读代码。相比于自然语言注释，JML更加严谨和清晰。只要能保证规格本身是满足需求的，并且编程时严格按照规格实现，理论上就程序就一定是正确的。正如指导书所言，”只要你确保满足了JML的需求，那么你的程序一定是正确的“。在这种情况下，即使出现了bug，也能通过OpenJML、JMLUnitNG等工具自动化地定位问题所在。
此外，通过对 JML 规格的阅读与撰写，我对每个方法的 Pre-Condition, Post-Condition, Side-Effect 有了更加深刻的理解，这是一个方法，或是一段程序正确性的根本保证，能更好地帮助我们判断一个架构设计的正确性与合理性。
JML 教给我们规格设计的思想以及这种规范编程的思维方式，对我们的程序员进化之路是大有裨益的。