一、梳理JML语言的理论基础、应用工具链情况
1.JML语言的理论基础
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言（Behavior Interface Specification Language，BISL），基于Larch方法构建。
JML有两种主要的用法：
（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
1.1JML表达式
1.1.1原子表达式
\result表达式：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。
\old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值。
\not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。
\not_modi?ed(x,y,...)表达式：与上面的\not_assigned表达式类似，该表达式限制括号中的变量在方法执行期间的取 值未发生变化。
\nonnullelements( container )表达式：表示 container 对象中存储的对象不会有 null 。
\type(type)表达式：返回类型type对应的类型(Class)。
\typeof(expr)表达式：该表达式返回expr对应的准确类型。
1.1.2量化表达式
\forall表达式：全称量词修饰的表达式。
\exists表达式：存在量词修饰的表达式。
\sum表达式：返回给定范围内的表达式的和。
\product表达式：返回给定范围内的表达式的连乘结果。
\max表达式：返回给定范围内的表达式的最大值。
\min表达式：返回给定范围内的表达式的最小值。
\num_of表达式：返回指定变量中满足相应条件的取值个数。
1.1.3集合表达式
集合构造表达式：可以在JML规格中构造一个局部的集合（容器），明确集合中可以包含的元素。
1.1.4操作符
JML表达式中可以正常使用Java语言所定义的操作符，包括算术操作符、逻辑预算操作符等。此外，JML专门又定义
了如下四类操作符。
子类型关系操作符： E1<:E2 ，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假
等价关系操作符： b_expr1<==>b_expr2 或者b_expr1<=!=>b_expr2 ，其中b_expr1和b_expr2都是布尔表达式，这两个表达式的意思是b_expr1==b_expr2 或者b_expr1!=b_expr2
推理操作符： b_expr1==>b_expr2 或者b_expr2<==b_expr1 。对于表达式b_expr1==>b_expr2 而言，当b_expr1==false ，或者b_expr1==true 且b_expr2==true 时，整个表达式的值为true 。
变量引用操作符：除了可以直接引用Java代码或者JML规格中定义的变量外，JML还提供了几个概括性的关键词来引用相关的变量。\nothing指示一个空集；\everything指示一个全集，即包括当前作用域下能够访问到的所有变量
1.2方法规格抽象
执行前对输入的要求----前置条件(requires)
执行后返回结果应该满足的约束----后置条件(ensures)
副作用范围限定，assignable列出这个方法能够修改的类成员属性
规格中专门说明exceptional_behavior
1.3数据(类型)规格抽象
数据状态应该满足的要求----不变式(invariant)
数据状态变化应该满足的要求----约束(constraint)
2.工具链
JML相应的工具链，可以自动识别和分析处理JML 规格。常用的有openjml，其使用SMT Solver来对检查程序实现是否满足所设计的规格(specification)。目前openjml封装了四个主流的solver：z3, cvc4, simplify, yices2。
二、部署SMT Solver
这个真不装不上。
三、部署JMLUnitNG/JMLUnit，针对Graph接口的实现自动生成测试用例， 并结合规格对生成的测试用例和数据进行简要分析
配置过程参见讨论区https://course.buaaoo.top/assignment/71/discussion/199
使用如下程序进行验证
import java.util.ArrayList; public class Demo { public ArrayList<Integer> nodes = new ArrayList<Integer>(); // @ public normal_behaviour // @ ensures \result = nodes.size(); public /*@pure@*/ int size() { return nodes.size(); } // @ public normal_behaviour // @ requires index >= 0 && index < size(); // @ assignable \nothing; // @ ensures \result == nodes.get(index); public /*@pure@*/ int getNode(int index) { if (index < 0 || index >= size()) { return -1; } return nodes.get(index); } //@ ensures \result == (nodes.size() >= 2); public /*@pure@*/ boolean isValid() { return nodes.size() >= 2; } public static void main(String[] args) { return; } }
最终文件结构如下
运行结果
成功运行
四、按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构
第一次作业：
理解规格，按照规格写就好了。需要注意的是，因为查询指令较多，更改状态的指令较少，这里采用双hashmap的方法，对pathId和path进行互相的索引，来降低查询时的复杂度。同时对于node的查询，采用缓存的思想，查询过的情况进行记录，跟新状态时，设立标志位，重新进行计算。
第二次作业：
增加了一个图的概念。当然，既然有图就少不了连通性和最短路径的查询。与第一次作业的不同也仅在这里。这里的图也与传统数据结构中的图一样。所有说普通的做法就是建立边集、点集，直接构建出图。同样，由于修改图的指令较少，所有这里采用floyd算法，一次性算出所有点对之间的连通性和最短路径。这样使得查询指令的时间复杂度为O(1)。当然，在修改图结构后不用马上进行计算，可以采用用时计算并缓存的策略。
第三次作业：
在图的基础上，具体化成了地铁轨道系统。这里采用继承的方式，原有的一些方法并不需要修改。这次的作业还是有很强的技巧性的，主要的原因是，这次的图并不是传统的图，这里的图是由一条条path构成，此外选哟实现的方法也与path与path之间的切换有着很强的相关性。所有在这里采用拆点的策略。具体而言，就是将每一站额外生成一个交换结点，该点连接所有nodeId相同的点。将nodeId相同，当所属path不同的点拆分出来。通过这样的处理，形成普通意义上的图，因为会额外生成许多点，且图大概率比较稀疏，所有采用Dijkstra算法进行计算并缓存。
还有一点要说的是，关于这次作业几个主要要实现的函数——最少票价、最少不满意度等等，可以建立起统一的求解方式。图结构可以采用同一个图结构，只是在获取权值时有所不同，这样的设计可以极大的减少代码量，同时易于管理，并且就上次作业中的连通性和最短路径也可以加入其中，进行统一管理。
五、按照作业分析代码实现的bug和修复情况
第十次作业：建立edge类，重写equals方法时。对于两个Integer对象的相等判定使用的“==”，未使用equals。这导致对于同一条边，不能够判断为相同。想想自己是真的菜，在我使用“==”时，idea都已经给我标注警告了。对于这个bug还想说的是，在数较小时，同一个值可能引用的Integer对象也相同，这也是我自己测试，使用较小的值没有测出bug的原因。
bug修改:把idea给我警告的“==”改为“.equals()”即可。
六、阐述对规格撰写和理解上的心得体会
关于jml的引入，由于每个人对于自然语言的理解不同，这导致大家实现的内容与预期出现偏差，由于需要对于保证规格没有二义性，这是jml就很自然的引入。这样不同的人理解规格不会出现偏差，至少规格本身的没有二义性。撰写规格是一件比较困难的事情，把抽象的语义转化为具象的jml规格确实有挑战，其中设计到大量逻辑上的问题，这一个部分是很难思考的。而且规格本身要保证其正确性和完备性，可以说规格的实现难度不亚于程序的实现难度。这里有一个问题，谁来保证jml规格的正确性呢？或许并不需要谁来保证吧，有了规格，在保证实现与规格之间没有偏差的情况下，规格上的错位是可追溯的，这样的bug，定位和修改都是比较容易的。那怎么保证实现与规格的一致性了?这不正是前面所提到的单元测试吗。
最后想说的是，不光撰写jml是技术活，理解jml也是技术活。通过层次化的方法可以使得规格更容易理解。这里我比较推崇的方法是，先通过自然语言进行理解(作业中通过函数名和指导进行理解)进行初步理解，对于具体细节，通过jml进行深入的理解。作业中关于Path中出现环的情况，就需要依靠jml才能找到答案。
原文：https://www.cnblogs.com/wudilailai/p/10903324.html