前言
第三单元是我们学习oo以来第一次接触JML。这一单元的三次作业和以前一样，采用了难度递进的方式，而且前一次作业的设计思路在下一次作业都多多少少有些体现（或者说是在其基础上做出的改进）。而且本单元作业在理解了JML的基础上来做，实现起来并不困难，难点在于如何提高自己代码的性能。本文分为四个部分：首先是JML语法基础；我的设计架构以及性能优化；debug以及测试样例的自动生成；心得体会。
JML语法基础
首先简要介绍一下JML语法基础。
JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。其中行注释的表示方式 为 //@annotation ，块注释的方式为 /* @ annotation @*/。JML的表达式是对Java表达式的扩展，新增了一些操作符和表达式。其中，新增的一些表达式分为原子表达式和量化表达式。原子表达式有： esult表达式，表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值；old( expr )表达式，用来表示一个表达式 expr 在相应方法执行前的取值，以及 ot_assigned(x,y,...)表达式等。量化表达式有forall表达式、exists表达式、sum表达式、product表达式、max表达式、min表达式等。新增的操作符有：子类型关系操作符，等价关系操作符和变量引用操作符。除此之外，方法规格是JML的重要内容。方法规格的核心内容包括 三个方面，前置条件、后置条件和副作用约定。其中前置条件是对方法输入参数的限制，如果不满足前置条件，方法 执行结果不可预测，或者说不保证方法执行结果的正确性；后置条件是对方法执行结果的限制，如果执行结果满足后 置条件，则表示方法执行正确，否则执行错误。副作用指方法在执行过程中对输入对象或 this 对象进行了修改（对 其成员变量进行了赋值，或者调用其修改方法）。
设计架构以及性能优化
第一次作业内容比较简单，主要目的是为了让我们熟悉JML语法，在此不做过多分析。这里分析一下第二第三次作业。
第二次作业在第一次作业的基础上，引入了一些图论的知识。在实现时，由于指导书给出了明确的指示——PATH_ADD和PATH_REMOVE不超过20条。出于这一点考虑，我把第二次作业涉及的最短路径的运算分散到了每一个PATH_ADD和REMOVE，就是每一次增删路径，都会对任意两点之间的最短路径进行重新运算并保存（听起来似乎很浪费，但是有20条指令限制的保护，起码可以保证不超时）。这样，在要用最短路径的时候，直接取用就好了。第三次作业就是在第二次作业的基础上加入了换乘的概念。但就是加入这一简单的概念，让整个问题复杂了许多。在解决这一问题时，我没有找到太好的解决办法，采用了拆点的方式来解决换乘。基本思路就是，不同path上的相同点在计算最低票价和最低不满意度时视为不同的点。（最低票价和最低不满意度都用迪杰特斯拉算法，当作最短路径来算，权值不同而已）
总体架构上，我除了题目要讲求的两个类之外，还单独加入了一个类，用来封装关于图的操作，比如每次加入新的path，都要存储和更新之前存储的任意两点之间的最短路径，最低票价，最低不满意度，最少换乘次数等。这些量各自都用一个图来存储，我把这些图，以及对这些图的操作都放在这个类里（全部都用静态变量和静态方法），每次要用到，或者要更新时，就访问这个类。
心得体会
这一单元让我感触最大的，是hash表的神奇之处——他能够将一段时间复杂度为o(n)甚至更多的遍历，改变成时间复杂度为o(1)的遍历。因为在这次作业之前，我没怎么遇到过程序运行时间上限的要求，所以在这之前，我一般都是选用ARRILIST来解决这一类的问题，但是ARRILIST只要是需要遍历一次，就有o(n)的时间复杂度，一旦出现嵌套遍历的情况，就会出现o(n)以上的时间复杂度。然而，hashmap就不存在这种问题了，因为它是通过hash值作为key值，用所在类的hashcode方法来计算相应的value值存储位置，时间复杂度为o（1）。而且，hashmap还有一个好处就是，他存储的不止是一个值，而是一对键值对，这样一对相互关联的值实际上都存储在了hashmap，比如path和pathid，就可以用pathid作为键值来存储path（整型类的hashcode是已经写好的不用重写，比较方便），这样一来，path和pathid都被存储了。
bug分析以及测试数据的自动生成
dubug
本单元作业还有一个难点，那就是debug，尤其是强测互测之后，那些强侧和互测的数据你根本看不出来什么（太多了），所以我以往面向评测机debug的方法已经不再实用，因为每个bug都相当于一个前两单元中测没有返回信息的点！
JMLUnit
package demo;public class Demo { /*@ public normal_behaviour @ ensures
esult >= num1; @ ensures
esult >= num2; @ ensures
esult >= num3; */ public static int compare(int num1, int num2, int num3) { int max; if (num1 > num2) { max = num1; } else { max = num2; } if (max < num3) { max = num3; } return max; } public static void main(String[] args) { compare(114,1919, 1111); }} 执行javac -cp jmlunitng-1_4.jar运行测试文件得到的结果是：
[TestNG] Running: Command line suiteFailed: racEnabled()Passed: constructor Demo()Passed: static compare(-2147483648, -2147483648, -2147483648)Passed: static compare(0, -2147483648, -2147483648)Passed: static compare(2147483647, -2147483648, -2147483648)Passed: static compare(-2147483648, 0, -2147483648)Passed: static compare(0, 0, -2147483648)Passed: static compare(2147483647, 0, -2147483648)Passed: static compare(-2147483648, 2147483647, -2147483648)Passed: static compare(0, 2147483647, -2147483648)Passed: static compare(2147483647, 2147483647, -2147483648)Passed: static compare(-2147483648, -2147483648, 0)Passed: static compare(0, -2147483648, 0)Passed: static compare(2147483647, -2147483648, 0)Passed: static compare(-2147483648, 0, 0)Passed: static compare(0, 0, 0)Passed: static compare(2147483647, 0, 0)Passed: static compare(-2147483648, 2147483647, 0)Passed: static compare(0, 2147483647, 0)Passed: static compare(2147483647, 2147483647, 0)Passed: static compare(-2147483648, -2147483648, 2147483647)Passed: static compare(0, -2147483648, 2147483647)Passed: static compare(2147483647, -2147483648, 2147483647)Passed: static compare(-2147483648, 0, 2147483647)Passed: static compare(0, 0, 2147483647)Passed: static compare(2147483647, 0, 2147483647)Passed: static compare(-2147483648, 2147483647, 2147483647)Passed: static compare(0, 2147483647, 2147483647)Passed: static compare(2147483647, 2147483647, 2147483647)Passed: static main(null)Passed: static main({})===============================================Command line suiteTotal tests run: 31, Failures: 1, Skips: 0===============================================