一、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表达式如：

　　　　\result ：表示一个非void类型的方法执行所获得的结果，即方法执行后的返回值。

　　　　\old(expr) ：表示一个表达式expr在相应方法执行前的取值。

　　　　\not_assigned(x,y,...) ：表示括号中的变量是否在方法执行过程中被赋值。如果没有被赋值，返回为true，否则返回false。

　　　　\not_modified(x,y,...) ：表示该表达式限制括号中的变量在方法执行期间的取值未发生变化。

　　　　\forall ：全称量词，表示对于给定范围内的元素，每个元素都满足相应的约束。

　　　　\exists ：存在量词，表示对于给定范围内的元素，存在某个元素满足相应的约束。

　　　　\sum ：表示给定范围内的表达式的和。

　　　　\product ：表示给定范围内的表达式的积。

　　　　\max ：表示给定范围内的表达式的最大值。

　　　　\min ：表示给定范围内的表达式的最小值。

　　　　\nothing ：空集。

　　　　\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。

　　

五、心得体会

　　理解和撰写规格对于程序设计和测试都有很大的帮助，也利于以测试驱动开发。