一、JML的理论基础应用工具链
JML是用于对Java程序进行规格化设计的一种表示语言。基于Larch方法构建。
(1)注释
JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。其中行注释的表示方式
为//@annotation ，块注释的方式为/* @ annotation @*/ 。
(2）原子表达式
\result表达式：表示一个非void 类型的方法执行所获得的结果，即方法执行后的返回值。\result表达式的类型就是
方法声明中定义的返回值类型。如针对方法： public boolean equals (Object o) ，\result的类型是boolean ，
任意传递一个Object 类型的对象来调用该方法，可以使用\result来表示equals 的执行结果（ true 表示this 和o
相等； false 表示不相等）。
(3)量化表达式
\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。(\forall int
i,j; 0 <= i && i < j && j < 10; a[i] < a[j]) ，意思是针对任意0<=i<j<10，a[i]<a[j] 。这个表达式如果
为真( true )，则表明数组a实际是升序排列的数组。
(4）方法规格
前置条件(pre-condition)
前置条件通过requires子句来表示： requires P; 。其中requires是JML关键词，表达的意思是“要求调用者确保P为
真”。注意，方法规格中可以有多个requires子句，是并列关系，即调用者必须同时满足所有的并列子句要求。如果
设计者想要表达或的逻辑，则应该使用一个requires子句，在其中的谓词P中使用逻辑或操作符来表示相应的约束场
景： requires P1||P2; 。
后置条件(post-condition)
后置条件通过ensures子句来表示： ensures P; 。其中ensures是JML关键词，表达的意思是“方法实现者确保方法执
行返回结果一定满足谓词P的要求，即确保P为真”。同样，方法规格中可以有多个ensures子句，是并列关系，即方
法实现者必须同时满足有所并列ensures子句的要求。如果设计者想要表达或的逻辑，这应该在在一个ensures子句
中使用逻辑或( || )操作符来表示相应的约束场景： ensures P1||P2; 。
副作用范围限定(side-effects)
副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。从方法
规格的角度，必须要明确给出副作用范围。JML提供了副作用约束子句，使用关键词assignable 或者
modifiable 。
(5)应用工具
Openjml,junit,SMT Solver都能从不同方面对于所写代码的规格以及类方法等进行测试正确性。
二、架构设计与重构分析
(1)第一次作业
度量图
类图
第一次作业主要就是按照所给规格进行代码的书写，比较简单，类方法也比较好理解，关键是对查询增删等数据结构存储的优化。
(2)第二次作业
度量图
类图
本次作业主要是增加了计算最短路径和连通性，比第一作业难度还是增加了不少，主要是考虑路径删减与边的删减联系起来的快速方法，采用hashmap等数据结构存储边，便于快速增删还有就是对最短路径的算法的选择以及对最短路径结果的存储管理，主要是如何快速查找以及计算的问题。
(3)第三次作业
度量图
类图
本次作业增加了连续换乘，票价，不满意度等的计算，所以导致前面所写的方法大量重构，本次作业所写的算法也是一个难点之一，如何寻找一个快速的算法尽快求出结果，又如何存储图的数据而避免来回的轮询是一个非常困难的问题。对于类的继承、重写的要求也非常高。
三、bug修复
第一次作业
在比较字典序路径时对规格方法理解出现错误，当一条路径比一条路径的节点多时就误认为这条路径比较长。还有就是使用的是ArrayList结构，在大量的查询命令情况下容易超时。
第二次作业
这次作业问题主要是超时，主要是程序中采用的dfs算法计算最短路径结果存储的遍历有大量的偏高的复杂度，需要对查询的算法进行优化。
四、心得和体会
JML在描述相对不是很复杂的类方法时可以清晰的描述方法需求，前置条件，计算结果等，便于对方法功能特性的理解。使用JML也使得代码能够更加便于封装和继承，在工程上使用也是具有很大的优势。
JML的描述也是十分严谨的，对于自己正确书写JML规格的要求也比较高，此外虽然JML语言描述出了方法具体的需求，但具体的实现过程以及如何使用相应的算法却也是更重要的，只有二者在解决实际工程问题上很好的结合起来才能达到更好的效果，JML配备的各种测试工具也能较快的让我们对于自己程序的错误进行精准的打击然后改正。JML是非常有实用价值的。