一、JML语言理论基础及应用工具链情况
（1）JML的程序语言理论
JML（java建模语言）是一种行为接口规格语言（behavioral interface specification language），用于指定java模块的行为。JML结合了按契约设计的方法（design by contract approach, Eiffel）和Larch系列的基于模型的规格方法，Design by Contract with JML（Gary T. Leavens and Yoonsik Cheon, http://www.eecs.ucf.edu/~leavens/JML//jmldbc.pdf）阐述了JML的设计和用法。
（2）JML语法（JML level 0）
1. JML表达式：
JML表达式包括原子表达式、量化表达式和集合表达式，常用JML表达式如：
esult ：表示一个非void类型的方法执行所获得的结果，即方法执行后的返回值。
old(expr) ：表示一个表达式expr在相应方法执行前的取值。
ot_assigned(x,y,...) ：表示括号中的变量是否在方法执行过程中被赋值。如果没有被赋值，返回为true，否则返回false。
ot_modified(x,y,...) ：表示该表达式限制括号中的变量在方法执行期间的取值未发生变化。
forall ：全称量词，表示对于给定范围内的元素，每个元素都满足相应的约束。
exists ：存在量词，表示对于给定范围内的元素，存在某个元素满足相应的约束。
sum ：表示给定范围内的表达式的和。
product ：表示给定范围内的表达式的积。
max ：表示给定范围内的表达式的最大值。
min ：表示给定范围内的表达式的最小值。
othing ：空集。
everything ：全集。
2. 方法规格：
JML方法规格包括正常行为规格（normal_behavior）和异常行为规格（exceptional_behavior），核心内容是前置条件（requires）、后置条件（ensures）和影响范围（assignable）。
requires：对方法输入参数的限制，如果不满足前置条件，方法执行结果不可预测，不保证方法执行结果的正确性。
ensures：对方法执行结果的限制，执行结果应当满足后置条件，否则执行错误。
assignable：方法在执行过程中对输入对象或this对象所做的修改，如赋值。
3. 类型规格：
类型规格是对Java程序中定义的数据类型的限制规则，包括不变式限制(invariant)和约束限制(constraints)。
invariant ：要求在所有可见状态下都必须满足的特性。
constraint ：对状态的变化的约束，即对前序可见状态和当前可见状态的关系的约束。
（3）JML建模
JML用行为描述、前置条件、后置条件、影响范围对方法的行为建模，用不变式和状态变化约束对类的数据域建模，实现完整的对类的状态和行为的规格化。
（4）JML工具链
目前已有若干成熟的开源JML应用工具，包括jmlc（断言检查编译器），jmlunit（单元测试工具）及jmldoc（javadoc的增强版）。
二、部署JMLUnitNG并针对Group接口的实现自动生成测试用例
执行过程如下：
测试结果如下：
Passed: racEnabled() Passed: constructor MyGroup(-2147483648) Passed: constructor MyGroup(0) Passed: constructor MyGroup(2147483647) Passed: <<test.MyGroup@5000001f>>.addPerson(null) Passed: <<test.MyGroup@1f>>.addPerson(null) Passed: <<test.MyGroup@5000001e>>.addPerson(null) Passed: <<test.MyGroup@5000001f>>.addRelation(-2147483648) Passed: <<test.MyGroup@1f>>.addRelation(-2147483648) Passed: <<test.MyGroup@5000001e>>.addRelation(-2147483648) Passed: <<test.MyGroup@5000001f>>.addRelation(0) Passed: <<test.MyGroup@1f>>.addRelation(0) Passed: <<test.MyGroup@5000001e>>.addRelation(0) Passed: <<test.MyGroup@5000001f>>.addRelation(2147483647) Passed: <<test.MyGroup@1f>>.addRelation(2147483647) Passed: <<test.MyGroup@5000001e>>.addRelation(2147483647) Passed: <<test.MyGroup@5000001f>>.delPerson(null) Passed: <<test.MyGroup@1f>>.delPerson(null) Passed: <<test.MyGroup@5000001e>>.delPerson(null) Passed: <<test.MyGroup@5000001f>>.equals(null) Passed: <<test.MyGroup@1f>>.equals(null) Passed: <<test.MyGroup@5000001e>>.equals(null) Passed: <<test.MyGroup@5000001f>>.equals(java.lang.Object@51016012) Passed: <<test.MyGroup@1f>>.equals(java.lang.Object@29444d75) Passed: <<test.MyGroup@5000001e>>.getAgeMean() Passed: <<test.MyGroup@5000001f>>.getAgeMean() Passed: <<test.MyGroup@1f>>.getAgeMean() Passed: <<test.MyGroup@5000001e>>.getAgeVar() Passed: <<test.MyGroup@5000001f>>.getAgeVar() Passed: <<test.MyGroup@1f>>.getAgeVar() Passed: <<test.MyGroup@5000001e>>.getConflictSum() Passed: <<test.MyGroup@5000001f>>.getConflictSum() Passed: <<test.MyGroup@1f>>.getConflictSum() Passed: <<test.MyGroup@5000001e>>.getId() Passed: <<test.MyGroup@5000001f>>.getId() Passed: <<test.MyGroup@1f>>.getId() Passed: <<test.MyGroup@5000001e>>.getPeopleSum() Passed: <<test.MyGroup@5000001f>>.getPeopleSum() Passed: <<test.MyGroup@1f>>.getPeopleSum() Passed: <<test.MyGroup@5000001e>>.getRelationSum() Passed: <<test.MyGroup@5000001f>>.getRelationSum() Passed: <<test.MyGroup@1f>>.getRelationSum() Passed: <<test.MyGroup@5000001e>>.getValueSum() Passed: <<test.MyGroup@5000001f>>.getValueSum() Passed: <<test.MyGroup@1f>>.getValueSum() Failed: <<test.MyGroup@5000001f>>.hasPerson(null) Failed: <<test.MyGroup@1f>>.hasPerson(null) Failed: <<test.MyGroup@5000001e>>.hasPerson(null) =============================================== Command line suite Total tests run: 48, Failures: 3, Skips: 0 ===============================================
三、作业架构设计
三次作业的架构基本相同，按规格实现官方包的接口。建模策略是首先阅读JML规格，理解整体的需求，再做设计，比如money可以做成person的属性。
四、作业bug及修复
作业bug主要在于第二次作业时为了减少queryGroupRelationSum和queryGroupValueSum的运算次数在addRelation和addPerson中增加了很多判断，有一些考虑不周的漏洞，强测和互测时很多用例的执行结果都出现了错误。bug修复阶段在5行内修复了所有bug。
五、心得体会
理解和撰写规格对于程序设计和测试都有很大的帮助，也利于以测试驱动开发。