JML梳理
1. JM语法一般结构
public instance //jml中操作数据，并不要求实现public invariant //不变式public constraint //约束 normal_behaviour //描述该方法正常行为requires; //对输入的要求assignable; //该方法可以改变的东西ensures; //对方法返回结构约束alsoexceptional_behaviour //描述异常行为signals; //抛出异常public methods() {} 几个常用关键词：
- \forall
- \exist
- \result
- \old
其中，有几点注意：
- jml中描述的数据结构，仅仅作为jml的描述，作用，并不限制具体过程中所使用的数据结构。
- 不变式和约束是在全局应该保持为真的。
- 更具体的jml语法和关键词的作用可以在官网手册中查看。
2. JML检查工具
目前我们使用的JML检查的工具是openJML。
openJML使用要求：
- jdk
- openJML software itself
- a SMT solver
openJML的基本使用
java -jar $OJ/openjml.jar
其中$OJ是openjml安装路径。
常用options选项
- -check //typecheck only
- -esc //static checking
- -rac //runtime assertions checks
- -prover //指定使用的prover
- -trace //输出错误栈
windows下openjml基本配置。linux下参照讨论区。新建一个.bat脚本，bat中脚本内容
java -jar $OJ/openjml.jar %*
然后将脚本路径加入到环境变量Path中。然后我们就可以使用openjml命令了。但是在windows下我没有找到类似/**/*.java的语法，所以使用的时候我用了-cp来添加包路径。希望大佬能提供更好的方法。
3.jmlunitng生成测试样例工具
基本使用
java -jar $JUN/jmlunitng.jar
其中$JUN是jmlunitng的安装路径
常用options选项。可以通过-help查看。这里列出几个常用的。
- -d //指定测试class输出路径，避免测试class与源码混在一起
- -cp //指定查找包路径，与java的-cp相同
- -inherited //为集成方法生成测试
- -public //为public方法生成测试
windows中配置，与上面相同。
java -jar $JUN/jmlunitng.jar %*
openjml的使用
由于我在使用openjml运行整个作业文件时会出各种蜜汁问题。所以就写了一个简单函数试一试。
public class Demo { /*@ requires lhs < 0 && rhs < 0; @ ensures \result == lhs - rhs; */ public static int sub(int lhs, int rhs) { return lhs - rhs; } public static void main(String[] args) { sub(-45, -3); sub(32, 2); }} -check 它是可以检查出我们jml的语法错误的。
-esc 我出现了一个错误，不清楚是它检查除了减法的溢出，还是它本身的报错。
-rac 在运行时检查出了sub(32, 2)；这里不满足规格要求。
jmlUnitNg使用
对上面代码使用结果如下。
大致我在使用以上工具时如果有多个文件相互依赖的话，不使用-cp就会找不到依赖，使用的话就会报错，（希望大佬能指导一下。
架构设计
1.第一次作业
第一次作业实现功能较为简单，各个功能之间也没有什么耦合，所以就按照接口给出的两个类进行了填补。
2.第二次作业
类图结构
架构思路
第二次作业的整个架构思路，仿照抽象层次由高到低来重新思考一遍。
首先是功能的架构设计：
- 首先一定会有三个类，Path，PathContainer，Graph。这三个类至少应该分别实现接口所定义的功能。其中Graph应该是对PathContainer的继承。
- 三个类宏观上的功能：Path是path点的集合，PathContainer是path的容器，提供一些查询功能，Graph是由path中的点构成的图，实现一些关于图的计算，提供一些关于图的查询。
- 接下来就可以具体思考每部分的功能怎样实现。对于Path，和PathContainer已经在上一次作业中已经完成，此处不再赘述。对于Graph的功能实现，首先是要一个图一定要维护一个保存图的数据结构，无论是用邻接表还是邻接矩阵，抑或是其他一些数据结构。为了实现查询最短路径和是否连通，我们还要实现相应算法，其中最短路径可以选择Dij或者Floyd等，同理是否连接也选择一个适合的算法。那么为了查询，我们还需要一定的数据结构来保存查询的结果，最后通过这些结果实现相关的查询函数。
- 接下来就可以具体决定使用那些数据结构，使用哪些算法。首先保存图，我采用了邻接表，所以最短路径算法采用Dij，对于是否连通我同样也采用了计算路径来判断，同时为了在添加path的时候更新邻接表，所以我们需要在Graph里实现addPath的操作，但是这个操作已经在PathContainer中实现了，基于尽量少修改原代码，和继承的思想，我在Graph里重写了addPath，先调用父类addPath，再添加自己的功能。这个思路也是理所当然的，PathContainer和Graph都是path的容器，那么都应该有addPath的方法，只是子类的addPath是父类功能的扩展。之后把查询的方法完成，这次作业基本就完成了。
到这里，我们的基本功能就完成了。但是对于架构的设计，不只是功能，应该从多角度。对于每个架构，我们都应该充分的考虑扩展性。对于一个Graph，我们直接能想到的就是path加权，以及多种算法，如最短路径，最大流等。
- 对于加权问题，现在的邻接表完全可以处理，所以不用考虑。
- 对于多种算法，还像我们这样把所有算法挤在Graph类中，就显得臃肿并且扩展性不好。我们首先能想到的就是把这些算法封装起来。这也是我们都会想到的做法。但在写作业的时候，大部分就是把一些数据和一些函数新建一个类，如果发现缺了什么功能，在添加，没有一个明确的设计。所以我们再来反思一下，我们要封装什么，封装到什么程度。我们可以站在用户角度思考这个问题，如果有一个最短路径的库共我们使用，我们希望它提供给我们什么，首先是创建，我们创建一个最短路径的实例（那么我们会传一个储存图的数据进去，我们当然希望它能识别各种储存图的数据结构，无论是hashmap套hashmap或者最基本二维数组，或者它应该在提供一个标准的GraphMatric来保存储存图的数据结构，而我们在新建这个类的实例，每次添加都提供一条边，而我们不关心它内部是怎样储存图的，这样显得就统一了很多）。其次我们当然还希望要查两个点的最短路径。所以这样封装的设计也就完成了。
同时，我们还需要考虑效率。在这次作业中我们都认识到了这一点。我们不妨再来思考一下，应该怎样去考虑优化的过程。我们的整个功能大致可以看作添加，计算，查询。
- 添加我们都要遍历一遍path，似乎没有优化的空间。
- 计算来说，就是高效的数据结构和算法的结合，在这次作业中，比较容易想到的就是用堆来优化一下Dij算法。
- 查询，因为查询的次数远大于计算的次数，所以保存计算结果，使得每次查询可以是o（1），也同时减少计算的次数。这也是大家常规的做法。
- 虽然计算较少，但仍是占用时间的主要因素，而每次修改图就需要重新计算，所以我们在addPath和removePath时可以判断是否修改了图，所以我用了一个新建了一个类Edge表示边，维护了一个hashmap来记录Edge出现的次数，以此来判断图是否遭到了修改。
以上就是从功能，扩展，效率分别对这次作业的架构进行了设计。按照上次老师的分享，这三个方面并不是独立的，它是这一个完成作业的三个视图，我们应该把他们结合起来看。
虽然这次作业的功能并不复杂，大家真正在写代码时完全不用搞得这么复杂，但是对一个简单的问题来体会一下架构的设计，我觉得还是有一些收获的。并且我们可以看到如果我们在写作业之前有这样一份设计，那我们在书写代码时的思路就会非常的清晰。
代码迭代
由于第一次作业的功能较为简单，所以在第二次作业中没有出现重构，唯一的冲突就是Graph的addpath的问题，采用了重写方法，避免了对上次代码进行修改。基本都是对功能的添加。添加了一个Graph类，Edge类，计算最短路径类。
3.第三次作业
类图结构
架构设计
对于上一次的作业我们进行了一个比较详细的分析，这次作业的反思也可以按照上面的思考来进行。（或者大家有更好的方法）这里简单描述一下这次作业的大致结构。
- 在上次的基础上添加了一个node类，保存节点编号，和path编号，来区分不同path的相同的点。
- 添加一个并查集类。
- 修改GraphContain，使得在添加edge时能够实现拆点做法，并实例化4个实例。
- 对于最短路实例化四个实例分别实现四个要求。
- 实现Railway类。
代码迭代
随着我们功能变得越来越复杂，我们不可避免的对上一次的代码做出一些修改。这里我阐述一下我这两次作业之间的修改。拆点做法大家都非常熟悉，这里不再赘述。
- 首先是处理拆点，实际上就是建立一个映射，可以用hashmap很容易解决。我在Graph里建立一个hashmap用来维护这个映射。其次我们要区分不同path中编号相同的点。我新建了一个node类，来储存path编号，和节点编号。
- 由于这次需要查询联通快，所以不可避免的要新建一个并查集的类，按照第二次的设计，我们可以很容的扩展这个类。
- 相对第二次的一些删除部分，第二次中采用维护Edge出现的次数来判断是否修改图，但是这次由于拆点，即每次addPath或removePath都是对图的修改，这个功能就没有必要。但是这个hashmap可以用来判断是否需要重新计算并查集，所以对这一部分做出来修改。
- 总的来说，按照第二次的设计，这次作业需要修改的部分不多，四个功能全部转化为不同权值的最短路径问题。
jml的体会
形式化验证我认为是一个很大的难点。对于jml，我们确实可以用它来指导我们代码的书写。但是我们使用任何一个工具，都要考虑到它的代价，首先是书写jml的难度，如果书写jml的难度很大，那么其实使用它的意义就不大。其次是jml本身正确性的判断，如果我们不能容易的判断书写的jml的正确性，那么也减小了使用它的意义。那么我对jml的感受，我感觉它是有一定优势的，他只规定了我们代码的输入，结果，以及结果的可能性，而不涉及代码本身的逻辑。这就大大减少这个语言本身的难度，和正确性的判断难度。但是我们还是需要一个好用的工具来对我们的jml做出检查（似乎它的工具链有点不尽人意