一、JML语言理论基础及其工具链
1. JML语言理论基础
JML是用于对Java程序进行规格化设计的一种表示语言，是一种行为接口规格语言(Behavior Interface Specification Language，BISL),基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。JML主要由Leavens教授在Larch上的工作，并融入了BetrandMeyer， John Guttag等人关于Design by Contract的研究成果。近年来，JML持续受到关注，为严格的程序设计提供了一套行之有效的方法。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式来检查代码实现对规格的满足情况。一般而言，JML有两种主要的用法：
1) 开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。
2) 针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
2. JML工具链
JML是一种语言，那必然需要一些测试工具来检验我们用JML编写的规格的正确性。JML的测试可以使用开源的JML编译器来编译含有JML标记的代码，所生成的类文件会在运行时自动检查JML规格，若程序未实现规格中的要求，JML运行期断言检查编译器会抛出一个uncheckedException来说明程序违背了哪一条规格。JMLdoc工具与Javadoc工具类似，可在生成的HTML格式文档中包含JML规范。还有工具JMLUnitNG可以根据规格的实现自动生成TestNG测试样例。SMT在形式化方法、程序语言、软件工程、以及计算机安全、计算机系统等领域得到了广泛应用。SMT Solver工具可以以静态方式来检查代码实现对规格的满足情况。Openjml使用SMT Solver来对检查程序实现是否满足所设计的规格(specification)。目前openjml封装了四个主流的solver。z3由Microsoft开发的，并已在github上开源：https://github.com/Z3Prover/z3 其正式发布版可通过https://www.microsoft.com/en-us/download/details.aspx?id=52270获得。cvc4由Standford开发，可以通过http://cvc4.cs.stanford.edu/downloads/下载。
二、JMLUnitNG测试流程
1. 实现文件树
test --> test.java
执行 jmlunitng test/Test.java
生成新的文件树
test
├── Test_InstanceStrategy.java
├── Test.java
├── Test_JML_Data
│ ├── ClassStrategy_int.java
│ ├── ClassStrategy_java_lang_String1DArray.java
│ ├── ClassStrategy_java_lang_String.java
│ ├── compare__int_lhs__int_rhs__0__lhs.java
│ ├── compare__int_lhs__int_rhs__0__rhs.java
│ └── main__String1DArray_args__10__args.java
├── Test_JML_Test.java
├── PackageStrategy_int.java
├── PackageStrategy_java_lang_String1DArray.java
└── PackageStrategy_java_lang_String.java2
2. 编译
1）javac 编译 JMLUnitNG的生成文件 java -cp jmlunitng-1_4.jar test.java
2）jmlc 编译我们的java代码，生成class文件 openjml -rac test/Test.java
3. 测试
java -cp jmlunitng-1_4.jar test.Test_JML_Test 即可得到运行结果
三、三次作业架构设计与迭代
1. 第一次作业PathContainer
PathContainer主要是针对path的增删改查，指令都很简单也不涉及到算法，而又有运行时间的要求，因此主要为了锻炼我们对JML的理解和对java中的各种容器的认识。我在MyPath类中采用的arraylist+hashset的方式，arraylist来计算路径长度，判相等，hashset用于计算distinctNodes.而MyPathContainer中，我采用了双hashmap，这样能保证根据path查pathid和根据pathid查path都有相同的复杂度O(1)。
2. 第二次作业Graph
Graph最重要的是出现了图这个概念，最重要的方法便是判连通和最短路径。我用了三个类：Vertex类，Edge类和Graph类三个类来存储图，每个vertex有一个linkedlist的属性来储存邻接表，Graph中有一个hashmap来存储vertex和其对应的nodeId.算法上判连通我用的BFS，而最短路径由于边权值均为1因此也可以用BFS来做。由于图结构变化指令很少，因此distinctnodes是在每次加入删除path时计算，询问时直接返回即可。
3. 第三次作业RailwayStation
RailwayStation是一个实际应用的场景，包括这次作业实现的方法也是与实际生活息息相关的。这让我们体会到了从简单的底层抽象到复杂的实际问题的分析流程。查连通块个数可以用多个BFS或者冰茶几，另外三个最低票价，最短换乘，最少不满意度其实都是虽短路径问题的变体。最短路径算法我采用的是时间复杂度为O(n^2)的dijkstra算法。对于最短换乘，我把每个Path看作一个节点，如果两个Path中有相同的PathId则这两个Path有一条边相连，然后用BFS即可。而最低票价和最少不满意度，都是涉及到一个换乘的问题。我采用的是拆点的解决方案，权值赋值成换乘需要增加的即可。
四、Bug分析与修复
1. WA
第9次作业，也是我认为OO作业有史以来最简单的一次作业，然而我的强测却惨遭爆炸，原因就是我的偏序比较comparable接口的实现错误。我对字典序的理解出现了偏差，导致所有不是相同长度的路径的比较都会产生相反的结果。分析原因，一是我C语言功底的薄弱，更重要的是我没有进行充足的测试，没有用Junit进行单元测试或者与自动生成测试样例与人对拍。在之后两次作业我增强了自我的测试因而之后没有出现正确性的问题。
2. CTLE
第11次作业我的strong15发生了CPU超时的情况，原因是忘了写cache。在用dijkstra算法求解最短路径的过程中，其实不止可以算出要求的最短路径，还有包含好多的中间结果(比如起点到好多点的最短路径)。然后，我们需要做的，就是充分利用好这些本次暂时用不上的中间结果，使得以后的最短路运算被不断加速（准确的说，这样的架构下，求解次数越多，后期速度越快）。对于已经求出来的全部最短路结果(无论本次是否用得上)，都作为边加入到构建的图中(后续经过此段的时候，不再需要一步步算)，并做好标记(对于访问已有结果的情况，可以直接出解)，使得这张图不断滚雪球，运算速度越来越快,这样可以极大的提高程序性能，降低CPU时间。
五、心得体会
1. 规格撰写与理解
通过这一单元三次作业还有课上的两次实验写下来，对规格也算是有了更深的理解。规格是对开发人员的规范，为严格的程序设计提供了一套行之有效的方法。我们第三单元通过三节课的学习，了解了类规格，方法规格，数据规格的写法，最重要的是为什么要写规格。总结来说，类规格定义了与用户的契约，也定义了开发人员必须遵从的规约。方法规格则由前置条件，后置条件和副作用组成，这是一个方法对实现者的规约。而数据规格则是类有效性的控制条件，constraint和invariant分别定义了数据状态需要满足的条件和数据修改需要满足的条件。
规格化设计是一种致力于保证程序正确性的设计方法，它本质上是一种设计方法。我们可以利用WARRANTY方法来看待规格化设计。
Step1(Why): 为什么需要这个方法？
Step2(Acceptance criteria): 这个方法所提供结果正确的判定条件是什么？
Step3(cleaR Requirement): 这个方法是否需要对调用者做出一些要求，从而确保能够产生正确结果？
Step4(ANticipated changes): 这个方法执行期间是否需要修改输入数据或者所在对象数据？
Step5(TrustY): 无需代码即可确认其语义
契约式设计是一种基于信任机制+权利义务均衡机制的设计方法学，JML的诞生正是源自于契约式设计的需要。通过本单元的学习，我感受到了通过规格设计，可以更容易获得简洁和职责单一的设计和实现（复杂方法会导致直接写不清楚相应的规格）。另一方面，经过实验和作业训练会发现，在很多情况下设计和撰写规格要比编写代码难。一旦规格确定了，其实实现代码就变成了一个相对简单的事情，除非涉及复杂的算法要求。因此，多理解规格使用规格化设计，对我们今后的软件开发大有裨益。
2. 想说的话
随着第三单元的结果，12周OO生涯已经过去了。本学期的OO课程也接近尾声，本学期OO课程做了非常大的改革，目前看来都是非常成功的，再次感谢老师助教们的付出。最后一单元是UML相关，希望自己继续加油，给本学期的OO课程画上一个圆满的句号。