一、JML语言
1.理论基础
JML(Java Modeling language)是用于程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言(Behavior Interface Specification Language,BISL)，基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部课件的内容。近年来，JML持续受到关注，为严格的程序设计提供了一套行之有效的方法。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式来检查代码实现对规格的满 足情况。
一般而言，JML有两种主要的用法：
（1）开展规格化设计。这样交给代码人员的将不是可能带有内在模糊性的自然语言表述，而是逻辑严格的规格。
（2）针对已有的代码的实现，书写其对应的规格。从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
2.类规格的组成：
·数据规格：类所管理的数据内容，及其有效性条件
·方法规格：类所提供的操作，前置条件（权利），后置条件（义务）和副作用（注意事项）
3.工具链：OpenJML是一套以OpenJDK构建的依靠JML对Java程序进行规格化和验证的工具，在Java1.8环境下运行。它将JML规格翻译成SMT-LIB格式并依靠SMT Solver组件进行分析工作。JML的完整工具链可以从JML官网下载。此外，还可以通过JMLUnitG/JMLUnit针对类自动生成样例并进行测试。
4.基本语法：
·前置条件(pre-condition)·
通过requires子句表示，方法中可以有多个requires子句，表示并列关系，就调用者必须同时满足所有的并列子句要求，示例：
requires P;
·后置条件(post-condition)：
后置条件通过ensures子句来表示。eusures是JML关键词，表达的意思是“方法实现者确保方法执行返回结果一定满足谓词P的需求，即确保P为真。示例：
ensures P;
·副作用范围限定(side-effects)
副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而为后续方法的执行带来影响。JML提供了副作用约束子句，使用关键词assignable或者modifiable。举例几种经常出现的副作用约束子句形态：
/*@ @ ... @ assignable \nothing; @ assignable \everything; @ modifiable \everything; @ assignable elements; @ modifiable elements; @ assignable elements,max,min; @ modifiable elements,max,min; @*/
·有时候，前置条件或后置条件需要不止一个变量进行约束，往往是对一个容器中的所有元素进行约束，这时就需要使用\forall或者\exists表达式：
/* @requires size < limit && !contains(elem); @ ensures \result == true; @ ensures contains(elem); @ ensures (\forall int e; @ e != elem; @ contains(e) <==> \old(contains(e))); @ ensures size == \old(size) + 1; @*/
·为了明确地区分异常，会针对输入参数的取值范围抛出不同的异常，这时可以使用exceptional_behavior:
//@ public model non_null int[] credits; /*@ normal_behavior @ requires z>=0 && z<=100; @ assignable \nothing; @ ensures \result == credits.length; @ also @ exceptional_behavior @ requires z < 0; @ assignable \nothing; @ signals_only IllegalArgumentException; @ also @ exceptional_behavior @ requires z > 100; @ assignable \nothing; @ signals_only OverFlowException; @ */
二、部署JMLUnitNG/JMLUnit并测试MyGroup类
三、作业架构设计
第一次作业：
类图：
分析：
第一次作业内容相对来说比较简单。由于是利用静态数组完成的，在用于关系和成员数目计数的数组中，我使用了表示人数的计数变量。在iscircle类中，我使用了比较传统的遍历方式，循环次数比较多，因而导致效率较低。
第二次作业：
类图：
分析：
第二次作业相当于在第一次作业的基础上加入了四个查询方法，同时一些基本的类的定义没有太大变化，因此可以在第一次作业的基础上迭代开发。
在计算组的AgeVar时利用了方差公式化简了表达式，提高了计算的精度。
第三次作业：
类图：
分析：
第三次作业在两个方法的设计过程中遇到了很大的问题，因此功能没有完善，（但是由于测试样例相对比较宽松），通过了样例的中弱测试。
由于只是添加了一部分功能，这次作业依然可以通过第二次作业的迭代开发实现。
四、代码实现的bug以及修复情况：
第一次作业：
第一次作业出现了一个很低级的错误。在实现添加关系的类时，我没有仔细解读jml的含义，在涉及添加关系的两个对象id相同时，没有做出对应的处理。导致没有输出，实际上对于两个id相同的人添加关系的情况，应该不做处理但是需要正常输出提示信息。因为这个问题，强测的大部分样例都没有通过，因而没有进入互测。
第二次作业：
第二次作业在第一次作业的基础上做了修复，并且由于对添加的功能类进行了仔细的分析，因而进入了互测。在互测过程中发现了两处bug，互测过程没有被发现bug。
第三次作业：
第三次作业由于有一个功能没有实现，因此强测过程中关于这个类的输出有很大问题，因此没有进入互测。
五、规格撰写和理解上的心得体会
这三次作业并没有涉及规格的撰写，但是个人认为在代码的开发过程中，作为团队开发过程中不可缺少的一种方式，我们撰写jml规格的能力需要得到锻炼。
JML规格在团队合作中的作用是减少不同人在代码开发过程中的耦合度，并且规划明确的分工。在软件开发的层面上也更应该侧重于将软件功能层次化，细分化。
我觉得规格的使用相当有必要，因为在完成了代码的规格，即通过形如伪代码的规格限制了代码的功能以及编写方式后，代码的开发会更加的精确，有效率。虽然我们目前接触的代码量还不是很大，但是在未来的开发过程中，我们可能会遇到规格庞大功能复杂的软件代码，系统代码等等。届时一个合理周到的规格或者响应的说明文档就不可少了。
原文：https://www.cnblogs.com/daleida/p/12944197.html