一、梳理JML语言的理论基础、应用工具链情况
JML以javadoc注释的方式来表示规格，每行以@起头。其中行注释为“//@annotation”，块注释为“/*@ annotation... @*/”。
常用表达式有以下几种：
\public normal_behavior：表达方法在正常情况下应该做出的操作
\public exceptional_behavior：表达方法在异常情况下的操作
\signals：表达抛出的异常
\requires：表达本方法满足的前置条件
\ensures：表达本方法的后置条件
\old(expr)：表示表达式expr在该方法执行前的取值
\forall：全称量词修饰的表达式，表示对给定范围的元素，每个元素都满足相应约束
\exists：存在量词修饰的表达式，表示对给定范围的元素，存在某个元素满足相应的约束
\result：用来表示本方法返回的正确结果
\assignable：用来表示方法会改变哪些变量
应用工具链：
OpenJML：是一个相对完整的JML工具，提供了JML语法检查、基于SMT Solver的静态检查（ESC）和基于自动生成测试用例的运行时检查（RAC）。
JML UnitNG：根据规格自动化生成测试样例，进行单元测试。
三、部署JMLUnitNG/JMLUnit，针对Group接口的实现自动生成测试用例，并结合规格对生成的测试用例和数据进行简要分析
输入以下指令对MyGroup类进行测试
java -jar .\jmlunitng.jar .\jml\MyGroup.java javac -cp .\jmlunitng.jar .\jml\*.java java -jar .\openjml.jar -rac .\jml\MyGroup.java java -cp .\jmlunitng.jar jml.MyGroup_JML_Test
结果如下
Failed: racEnabled() Passed: constructor MyGroup(-2147483648) Passed: constructor MyGroup(0) Passed: constructor MyGroup(2147483647) Passed: <<MyGroup@60aca232>>.addPerson(null) Passed: <<MyGroup@1e234854>>.addPerson(null) Passed: <<MyGroup@534cb4a3>>.addPerson(null) Passed: <<MyGroup@34f6c241>>.delPerson(null) Passed: <<MyGroup@5b87e63>>.delPerson(null) Passed: <<MyGroup@235d7a8>>.delPerson(null) Passed: <<MyGroup@5c2d426>>.equals(null) Passed: <<MyGroup@452a069>>.equals(null) Passed: <<MyGroup@1244628>>.equals(null) Passed: <<MyGroup@13da4c58>>.equals(java.lang.Object@13c521e7) Passed: <<MyGroup@36f2ac63>>.equals(java.lang.Object@3a5820ac) Passed: <<MyGroup@5a7d408a>>.equals(java.lang.Object@3f61ca2d) Passed: <<MyGroup@5a7f4034>>.getAgeMean() Passed: <<MyGroup@534db40f>>.getAgeMean() Passed: <<MyGroup@6ac37982>>.getAgeMean() Passed: <<MyGroup@369dc9ab>>.getAgeVar() Passed: <<MyGroup@6a2a593a>>.getAgeVar() Passed: <<MyGroup@37c51a91>>.getAgeVar() Passed: <<MyGroup@5476ab3>>.getConflictSum() Passed: <<MyGroup@1683bd80>>.getConflictSum() Passed: <<MyGroup@5ce43960>>.getConflictSum() Passed: <<MyGroup@3a7820bc>>.getRelationSum() Passed: <<MyGroup@8b56ca4>>.getRelationSum() Passed: <<MyGroup@265a8d46>>.getRelationSum() Passed: <<MyGroup@45c60943>>.getValueSum() Passed: <<MyGroup@4a6c83045>>.getValueSum() Passed: <<MyGroup@83cf78>>.getValueSum() Passed: <<MyGroup@5487be60>>.hasPerson(null) Passed: <<MyGroup@659a7509>>.hasPerson(null) Passed: <<MyGroup@5adcd5c8>>.hasPerson(null) =============================================== Command line suite Total tests run: 34, Failures: 1, Skips: 0 ===============================================
四、按照作业梳理自己的架构设计，特别分析自己的模型构建策略
（1）第九次作业
第一次作业写了MyPerson和MyNetwork两个类，对继承的接口进行了实现，所有的代码内容就是简单地按照JML的规格来写的，在两个类中的person和value都使用ArrayList来保存。
这次的作业在中测和强测中均未发现bug。
（2）第十次作业
第十次作业依然是根据JML来写，MyPerson类沿用了第九次作业，在MyGroup中用一个ArrayList存储person。由于没有对算法、缓存等进行优化，这次过了中测之后在强测全线崩盘，出现了大量CTLE。isCircle、isLinked等方法因为多次遍历的原因导致导致复杂度过高，且没有将结果缓存，导致每一次调用都需要从头遍历，最终造成了大量的CTLE。
（3）第十一次作业
除按照JML规格增加了新的方法外，将MyNetwork中的people、groups、money、nameRank，MyPerson中的acquaintance、value，MyGroup中的people全都使用HashMap存储，将isCircle、queryMiniPath、queryStrongLinked、getAgeMean、getAgeVar等方法中得到的中间数据缓存，在people和link有改变时对其进行更新，减少复杂度。
五、按照作业分析代码实现的bug和修复情况
除开在写的过程中由于疏忽导致的肉眼可见的output错误的bug之外，最主要的问题就是在强测中程序超时，这边还是数据结构的问题，需要加强。
六、阐述对规格撰写和理解上的心得体会
规格的撰写是面向对象的一种很好的体现，我们要明确每个类的需求，然后要熟悉规格的语法，正确的规格有利于对程序进行更好的测试与维护。前两次作业主要按照规格来写，可以说逻辑上给了我非常大的帮助，测试的过程中也让我充分体会到规格的便利之处。对于规格的学习对我们未来的团队编程应该会有很大的帮助吧。
原文：https://www.cnblogs.com/ruby7/p/12942925.html