一、JML语言基础
原子表达式：
esult：表示方法执行后的返回值，类型为方法声明中所定义的返回值类型。
old(exp)：表示表达式exp在方法执行前的值。
ot_assigned(x)：判断括号中的变量在方法执行过程中是否没有被赋值、改变。
onnullelements(container)：约束container中存储的对象不含null。
type(type)、typeof(exp)：返回类型type、表达式exp对应的类型(Class)
量化表达式：
forall：类似于全程量词，表示范围内的每个元素都满足约束。
exists：类似于存在量词，表示范围内存在某个元素满足约束。
sum product max min等：返回给定范围内表达式的和、连乘结果、最大值、最小值。
um_of：返回指定范围内满足约束的变量取值个数。
操作符：
子类型关系<:，例如Integer. TYPE<Object .TYPE
等价关系<==>, <=!=>：表示左右两个表达式相等或不等
推理关系==>, <==：语义与离散数学中的蕴涵关系相同
变量引用：可直接引用java或规格中定义的变量。
数据规格：
/*@spec_public@*/：用来注释类的私有成员变量，表示在规格中是外部可见的
此外，规格中所定义的public变量都是表示规格中外部可见，实际实现代码时不需要按照public来实现
方法规格：
requires：表示前置条件，是对方法输入参数的限制。
ensures：表示后置条件，是对方法执行结果的约束。
assignable和modifiable：表示副作用，是对方法执行过程中对对象和类属性修改的限制。
pure：表示被修饰的方法为轻量级的纯访问性方法，没有副作用。
public normal_behavior ：表示接下来的部分为方法正常功能行为的规格描述
public exceptional_behavior ：表示接下来的部分为方法异常行为的规格描述
signals：在异常行为规格中声明抛出的异常。
also：分割多种行为(正常or异常)规格的关键词。
类型规格：
invariant：不变式，表示类和对象在所有可见状态下都应该满足的约束条件。
constraint：状态变化约束，表示有副作用的方法。
二、JML工具链
运行结果：
Passed: constructor MyGroup(2147483647)
Passed: <<MyGroup@6842775d>>.addRelation()
Passed: <<MyGroup@768debd>>.addPerson(java.lang.Object@490d6c15)
Passed: <<MyGroup@66133adc>>.delPerson(java.lang.Object@7bfcd12c)
Passed: <<MyGroup@18ef96>>.equals(java.lang.Object@6956de9)
Passed: <<MyGroup@6aceb1a5>>.getAgeMean()
Passed: <<MyGroup@12bc6874>>.getAgeVar()
Passed: <<MyGroup@67117f44>>.getConflictSum()
Passed: <<MyGroup@5d3411d>>.getId()
Passed: <<MyGroup@6979e8cb>>.getRelationSum()
Passed: <<MyGroup@2be94b0f>>.getValueSum()
Passed: <<MyGroup@47d384ee>>.hasPerson(java.lang.Object@2d6a9952)
Passed: <<MyGroup@224aed64>>.size()
三、作业架构
第一次作业
除了递归方面使用bfs，其他部分难度很低，大多使用Hashmap容器存放数据，便于数据的提取。
第二次作业
这次作业主要增加了Group类，此次作业中，考虑到容器的应用可大体抽象为遍历和查找两种，于是为了一些数据的存储实现了两个容器，一个是arraylist用于成员遍历，一个是hashmap用于成员查找，但每次增加一个对象可能要进行很多的增删，所以有点麻烦。
第三次作业
有两个难点，一是求最短路，二是求是否强连通。求最短路直接使用的迪杰特斯拉；连通块数只在addPerson方法调用的时候进行更新，调用getBlockSum方法时直接返还缓存变量，更新使用并查集；强连通算法为tarjan，递归的编写需要人进行很多的练习才能熟练掌握。
四、BUG的问题
第一次作业
Map的get方法需要的是key而不是索引，出现了很大的问题。
第三次作业
递归写的稀碎，都是re，虽然感觉自己写的没有什么问题也进行了很多测试，但真的写的问题太大了，而且写的时候特别艰难，只能说是ds没学好留下的坑。
五、心得体会
JML是一种面向规格的设计语言，他让我们依据规格，能够正确的使用方法和数据，能够写出完善的功能实现，并且在保证正确性的条件下，选择不同的实现方式，从它的语法来看，非常符合契约设计的理念：requires 描述先验条件，由调用者进行保证，即调用者的义务；ensures 描述后验条件，由开发者进行保证，这也是调用者享受的权利。
但对于我来说这次最大的问题在于递归的编写，数据结构学的不扎实导致我计组p2和这个单元特别痛苦，写的还不对，所以我认为最大的问题在于提高自己对于递归的掌握，期望在这个假期的空余时间可以进行提高。