1、JML简介
1.1 JML与契约式设计
提及JML，就不得不提到契约式设计（Design by Contract）。这种设计模式的始祖是1986年的Eiffel语言。它是一种限定了软件中每一个元素所必需的责任与义务的开发模式，程序设计中的每一个元素都须要用规范的语言精准地限定其前置条件（Preconditions）、后置条件（Postconditions）和不变式（Invariants）。经过这三项限定，咱们能够清晰地得到对一个函数功能的刻画，从而达成设计与实现的分离，便于优化、测试和生成文档。html
契约式设计的理论基础是形式验证、形式规约和霍尔逻辑。在我看来，契约式设计正是形式规约的工程化实现方式，也正是由于有了规范的契约，形式验证才可能得以成立。相比于测试驱动编程（Test-Driven Development），契约式设计能经过定理证实器经过形式验证的方式证实程序的正确性，从而更加可靠。java
契约式设计在不少语言中都有自带支持，例如Fortress、Perl和Java的新近亲Kotlin，其中不少语言都是经过相似于assert断言的方法进行契约限定的。Java并无自带的契约式设计模块，JML做为仍处于活跃开发中的第三方Java契约式设计模块能够填补这一方面的空白。node
JML是一种行为接口规格语言，能够借由一套标准化的带注解的注释实现对Java代码语法接口（即函数名、返回类型、可抛出异常等）和行为的规范。JML将Eiffel等契约式设计语言的操做性和Java等现代语言的可读性相结合，利用Java表达式进行规格书写，并对其进行了必定的扩展，增长了量词方便规格书写。git
1.2 JML工具链
JML的一大优点就在于其丰富的外围工具，它们都被罗列在了http://www.eecs.ucf.edu/~leavens/JML//download.shtml上。其中比较重要的几个以下：程序员
- OpenJML：首选的JML相关工具，以提供全面且支持最新Java标准的JML相关支持为目标，可以进行静态规格检查（ESC，Extended Static Cheking）、运行时规格检查（RAC，Runtime Assertion Checking）和形式化验证等一系列功能。OpenJML提供了自带的命令行版本和Eclipse插件版本。
- JML Editing：官方的Eclipse插件，提供了JML规格的代码高亮及代码补全。
- JMLUnitNG：JMLUnit的替代工具，可以根据JML规格自动生成基于测试库TestNG的单元测试集。
- jmldoc：可以经过JML生成javadoc的工具。现已合并入OpenJML中。
JML还有一系列其余工具，可是这些工具大都是从不一样角度根据规格进行代码测试的，这些功能已被OpenJML所涵盖。github
2、SMT Solver的使用
利用SMT Solver进行形式化验证是OpenJML提供的功能之一。该工具备两种使用方式：使用命令行版本（或经过IDEA的OpenJML/ESC插件间接调用该工具）或使用OpenJML的Eclipse插件。算法
在个人前一篇博客中，我介绍了如何利用Maven项目在IDEA和Eclipse间进行项目互通以方便地使用Eclipse插件进行形式化验证，所以在此省略操做部分。编程
然而，OpenJML存在一些谜同样的问题，会致使代码被错误地判为invalid。许多人遇到的size在形式验证中返回值为真实值-1的错误至今依然让我感到疑惑，甚至MyPath一样的代码和规格，在第9次做业中所有为valid，然而复制粘贴到第10次做业中就出现了错判。这也许和OpenJML对JML语法的支持尚不彻底有关，不过我在写上一篇博客时意外地留下了一张运行无误的截图，在此能够对它进行一下粗略的分析。windows
这是对个人第9次做业全部文件的形式验证结果，验证配置为OpenJML 0.8.42 + z3 Prover 4.7.1。从左下角一片绿色的验证结果能够看出，此次做业中MyPath和MyPathContainer两个类中除了个别方法被判为invalid外（实际上这些错误大部分是由于整数自增溢出），其他方法都可以完美地经过形式化验证。在这其中，出现错误最多也最典型的一个函数是MyPathContainer.addPath()。从代码中的高亮能够看到，该函数中存在4处错误。这四处错误分别为：设计模式
- 54行：
++currentPid中，因为currentPid为int型，故自增可能致使溢出。 - 55行、56行：我在
MyPathContainer的实现中为了提升id和Path互查的效率，采用了双HashMap的结构，所以在addPath()中须要对pathToId和idToPath两个HashMap均进行put()操做。此处报出的两个错均为InvariantLeaveCaller，代表调用一个外部函数时不知足不变式。这一结果出乎意料地正确，由于在调用单个put()操做的中间，因为已经调用了外部函数，故属于可见状态，而在此期间两个HashMap并未完成统一，因此不变式未达成。不过HashMap.put()做为jdk自带方法，这样的报错也许是多余的。 - 58行：在这里虽然采用了java 8的双冒号写法，但内涵依然是
int递增，仍然可能致使溢出。
因而可知，利用SMT Solver在不出现没法解释的所有判错现象时是很是可靠的，能够认为一旦经过了该测试就彻底符合了规格要求，是保险性最高的测试。
3、JMLUnitNG的使用
此处首先感谢讨论区伦dalao的分享。
JMLUnitNG虽然是JMLUnit的替代版，但它的功能还没有开发彻底，使用起来很是复杂，稍有不慎就会让人完全崩溃。我在使用过程当中遇到了许多难题：
- 该工具的最后一次更新是在2014年，甚至在java 1.8更新前。因为JMLUnitNG包中自带了其所有依赖库，因此其自带的过旧的OpenJML库依赖使得其没法正常分析使用了java 1.8及以后版本的语法，这给测试形成了第一道困难。为此，我将其依赖的OpenJML工具替换成了截至2019年5月的最新版本0.8.42并从新打了包，感兴趣的能够从个人github上下载：https://github.com/sheryc/JMLUnitNG/releases/tag/v1_5
- 该工具分四步操做：生成测试→编译→执行rac→测试。在第一步生成测试中，须要添加-cp参数添加库依赖。根据JMLUnitNG的官方doc，classpath参数的写法遵循javac写法，然而实际上在添加多个依赖目录时，JMLUnitNG采用了对windows系统极为不友好的冒号分隔方式。这致使以盘符加冒号（如D:\）开头的绝对路径没法做为JMLUnitNG的-cp参数被传入。为了解决这个问题，须要将依赖库所有放入项目文件夹中。
- JMLUnitNG不容许所分析的文件中带有GBK字符，而官方接口中每一个函数都有用中文写的javadoc，删除注释的工做量巨大。最终无可奈何转成了对并不依赖过多官方文件的
MyPath类进行测试。 - 当依赖.jar文件包时，JMLUnitNG没法检测到JML规格。为此我将JML规格复制到了本身的文件中。
- 因为对OpenJML的依赖，因此OpenJML存在的对一部份量词没法验证的问题天然也继承到了JMLUnitNG中。为此须要对规格进行改写。须要删去model，在本身的实现中添加
spec_public标识，并改写或删除会报错的\exists和\forall规格。 - 即便解决了以上问题，还会存在JMLUnitNG对于一部分写法不能识别的问题。在一开始，我在进行rac步骤时会报出一个其余人都不会报出的错误：A catastrophic JML internal error occurred. Please report the bug with as much information as you can. Reason: Mismatch in number of arguments in accumulateTypeInstantiations。通过一段时间控制变量式的探索后，我发现错误根源竟在于
Path.equals()中采用的以下for-each循环：
Iterator<Integer> objIter = ((MyPath) obj).iterator();
for (Integer integer : this) {
if (!objIter.next().equals(integer)) {
return false;
}
}
该循环自己写法并无错，而且支持了java 1.8语法后应该对for-each循环的判别没有问题。然而这样的循环居然会致使OpenJML的内部错误，这很是不可理喻。这样一个错误花费了我很长的时间，从第9次做业贯穿到本次总结的写做，甚至我拜托了几名同窗帮我进行测试，却怎么也没想到错误是因为OpenJML自己的bug致使的所谓“Catastrophic internal error”。最终我将for-each循环改成了hasNext()循环，解决了这个问题。
最终的测试结果以下：
鼓捣了半天，最后竟然报了构造方法出错，并且彷佛由于构造器没法经过测试而跳过了后续的测试？可是MyPath的构造器实际上构造很是简单，因为时间紧迫，我也没有进一步探寻如何修复报出的莫须有的错误。不过从后续的测试数据中能够发现，JMLUnitNG即便在检测到了JML规格的状况下，所作的也只有边界测试，测试覆盖性极其有限，而且其生成单元测试的依据彷佛不是JML规格，而是函数签名。
虽然自动生成单元测试的功能很方便，但对于JMLUnitNG这一款工具而言着实鸡肋：其高昂的学习代价，漏洞百出的执行过程，毫无体验感的使用流程，对JML规格并不够好的支持，以及最终生成的覆盖度差的测试用例，都不值得让用户使用这样一款半成品工具，也难怪早在5年前这一项目就中止了活跃开发。相比之下，阅读规格并本身设计单元测试会更加可靠且更加方便。在自行设计单元测试时，咱们能够仿照JMLUnitNG的测试思路，在覆盖全部运行分支的基础上，多设计一些边界测试和无效测试，而这些在SMT Prover的形式验证中也经常成为测试的反例。
4、JUnit的使用
在这几回做业中，JUnit若是使用到位是能够对程序验证起到很是大的帮助的。在此以本身第9次做业的单元测试为例。经过对测试执行“Run with Coverage”指令，能够得到单元测试对代码中全部执行路径的覆盖程度：
从右边的Coverage能够看出，个人测试对于MyPath和MyPathContainer的代码覆盖度分别达到了81%和100%，已经能够几乎覆盖到全部执行分支。而实际上，个人单元测试是在写代码前就已经写好的（很有一种Test-Driven Develop的感受），因此能够作到测试和代码的分离。
在设计测试时，须要将不一样运行分支分在不一样的方法中进行测试，这也是为什么个人函数后面会带有Normal、Exceptional和编号，这样能够在一次执行中最大化发现的问题数量。
单元测试是最底层的测试，在个人理解中，它的做用与方法规格是相辅相成的，都是为了测试一个函数是否可以知足对该函数的全部要求。恰好在这次做业中每一个函数的功能几乎是分离的，因此一个覆盖性好的单元测试对正确性的保证是仅次于形式验证的。
5、三次做业总结
5.1 第九次做业
5.1.1 实现方案
本次做业须要实现的是Path和PathContainer。
对于Path类，其存在的操做仅为查询。对根据下标查询的操做，选用基于数组的ArrayList能够达到O(1)复杂度；对查询节点是否存在/不重复节点个数的操做，选用HashSet能够达到一次生成后每次查询都为O(1)复杂度的目标。
对于外部函数能够经过iterator()返回的迭代器修改Path的问题，在这里我记录了每一次ArrayList的hash码，当进行HashSet相关查询操做时，首先比较当前ArrayList的hash码是否与先前保存的hash码，若相等则能够认为很大几率该Path未通过修改，不然从新构建HashSet。
我在其中使用了一些提升效率的小trick，好比HashSet的构建只有在进行相关查操做时才开始，这样能够省去一些进行无用且耗时的HashMap构建操做的时间。
对于PathContainer类，进行的是少许的增删操做和大量的查操做。为此，须要将查操做尽量优化到O(1)复杂度。我采用了idToPath，pathToId双HashMap以优化两者之间的双向查找；与此同时，使用一个单独的HashMap记录每一个节点的出现次数，这样在查询不重复节点时只需返回该HashMap的size便可。
本次做业的UML类图以下：
5.1.2 出错分析
本次做业强测满分。高工不参加互测。
5.2 第十次做业
5.2.1 实现方案
本次做业中将PathContainer升级为了须要计算节点间路径长度的Graph。本来Path和PathContainer的操做依然保持不变。
在本次做业中我本应让MyGraph继承上次的MyPathContainer的，但当时我对于继承时private字段的处理方式理解不到位，因此没有用这种方式，而是直接将MyPathContainer的代码复制了过来。如今想来实在是很是不该该。
新增的操做所有是基于两点间最短距离的，因此计算最短路径成为了本次做业的核心。为此我新建了两个辅助类：用于压缩记录每两个节点间距离的DistMap和应用图算法的GraphUtils。
在DistMap中，我将每对节点的距离记录在了一个HashMap<AbstractMap.SimpleEntry<Node, Node> Integer>的数据结构中（此处Node其实是Integer，这样写是为了理解方便；此外AbstractMap.SimpleEntry是java.util中自带的Pair类型）。因为须要存储的图是无向图，其距离矩阵应为对称阵，故为了节约存储空间 ，存入和查询时的SimpleEntry都应保证其key<=value，这样能够将距离矩阵压缩一半。
在GraphUtils中，采用基于优先队列的堆优化的Dijkstra算法。为此须要在该类中维护一个邻接矩阵HashMap<Node, HashMap<Node, Integer>>（此处Node其实是Integer，这样写是为了理解方便），其中内层的Integer为这两个Node的邻接次数，这样能够在一些删除重复边的状况下忽略其影响。
在使用优先队列时，实际上能够用一种更简单的方式进行初始化。个人优先队列中存储的均为AbstractMap.SimpleEntry<Node, Distance>的形式，故堆的比较依据为该SimpleEntry的value。此处可使用Java 1.8中新增的双冒号写法以简化代码：
PriorityQueue<SimpleEntry<Integer, Integer>> remainDist = new PriorityQueue<>(Comparator.comparingInt(SimpleEntry::getValue));
计算全部的距离后，全部新增的查操做均可以经过判断两点之间距离的方式达成。须要注意的一点是，有些结点可能存在自环，因此对这样的结点判断本身和本身间是否存在边时应返回true。所以，须要维护一个记录存在自环的结点的数据结构。
本次做业的UML类图以下：
5.2.2 出错分析
本次做业强测满分。高工不参加互测。
值得一提的是，因为做业中须要进行n次SSSP计算全图距离，因此本来的想法是创建一个线程池，多线程运行这些Dijkstra算法。然而，线程池所有线程运行结束的判断比较复杂，再加上须要优化的并不是实际运行时间而是CPU时间，因此在发现错误以后果断地回归了单线程模式。
5.3 第十一次做业
5.3.1 实现方案
本次做业中将Graph升级为了须要计算换乘距离/连通份量个数的RailwaySystem。本来``Path和Graph`的操做依然保持不变。本次做业我依然错误地没有使用继承，反省反省。
本次做业新增了三种须要考虑线路换乘的距离计算问题，这三种问题实质上使用的是同一种算法，不同的只有边权和换乘权重。所以，我将先前的图计算类GraphUtils改造为了一个抽象类，保留了Dijkstra算法，而边权和换乘权重变为了两个抽象方法normalCost()和transferCost()，而不一样的距离计算只须要新建不一样的图计算子类override这两个方法便可。
为了解决线路换乘的判断问题，我采用了拆点法，将不一样线路上的相同节点视为不一样结点，这样每一个点的邻接点被分为两类：在同一条Path上的相邻点和在不一样Path上的相同点。为此，须要：
- 对点进行扩展编号，在其中保存点编号和线路号两重信息；
- 对每一个点记录其所在的Path集合方便遍历；
- 邻接表中存储的均为点的扩展编号，只有在同一Path上相邻的点才在邻接表中进行记录。
对于扩展编号，我采用了一些小trick。因为增删Path的指令最多只有50个，所以，不须要创建复杂的数据结构，只须要经过一个最低三位记录线路号，高位记录节点号的long类型数便可。我创建了静态类ExtendedNode，经过(long) nodeId * 100 + pathId的方法得到扩展编号；从扩展编号逆推原来的点编号和路径号时，只需进行除100或模100操做便可，省去了不少IO时间。
相比于上一次做业每作一次增删路径操做都从新计算全图的全部距离，本次我采用了查一个算一个的策略，发现所查询距离没有时则跑一次对应图的SSSP，也能够节省一些时间。
对于连通份量个数，采用带路径压缩的并查集完成。在删除结点后，须要从新对并查集进行计算。
本次做业的UML类图以下：
5.3.2 出错分析
本次做业强测满分。高工不参加互测。出乎意料的是此次做业竟然是弱测带强测一次过，或许是这种清晰的继承结构带来的方便吧。
6、感想
在第一单元时，我就听闻单元测试对于程序验证的重要性，然而单元测试从何开始设计一直都是个人困惑。在接触了规格以后，这一问题获得了解决：单元测试应该是面向一个模块应该完成的全部工做的，而规格恰好为测试的设计提供了依据。有了规格以后，不管是单元测试仍是场景测试都能很快地定位到出错位置。
此外，规格还能成为顶层设计与底层实现之间的桥梁。在开发大型项目时，设计架构事后须要将任务分摊到每一个不一样的模块中，撰写代码规格有助于理清每一个模块所需实现的功能，从而更好地耦合；而程序员则不须要考虑模块与模块之间的调用逻辑，只须要想办法完整实现规格便可。
同时，在我看来规格也是依赖反转的体现之一。实际上方法的调用者须要的是一个被调方法的功能，而不关心其背后的具体实现，这有点相似于接口的用处。有了规格以后，背后的实现方式的更新或是算法的优化都有了不出错的保证（其实是根据规格所撰写的完整的单元测试保证了这样的改写依然有效）。
在本次做业中，因为指导书的描述和函数名已经给予了足够清晰的函数功能定义，因此实际上并不须要彻底理解规格的内涵就能够完成任务，这样看来应该是程序文档对程序员的帮助更大一些，毕竟天然语言更贴合人的思惟。然而，规格的规范性可以让程序设计者明确一些边界状况应该如何处理，以及多数状况下规格自己就是一个方法功能的最简单实现，有了文档和规格的双重保证才能让程序设计者可以更快更好地实现功能。
规格的撰写的确是一大难事，有很大一部分缘由是JML规格并无提供代码高亮和自动补全，而JML Editing插件也是在写本次总结的时候才了解到的，因此每敲一下键盘都要怀疑本身写的对不对，甚至括号匹配都会成一个大问题。不过JML的优点在于其贴近Java的语法，因此抱着用最浅显的算法去实现功能的想法反而能很容易地写出规格。
最后须要吐槽一下JML的工具链：除了OpenJML依然在持续更新外，其余工具都已经彻底跟不上时代了，甚至还有JMLUnitNG这种历史悠久的半成品直接发布出来让人用，实在是体验极差。此次博客的撰写比以前任何一次代码做业都让人崩溃，其中数次想要放弃，但依然坚持住跑完了全部工具，实属不易。~~（在这里感谢湊あくあ等国际友人在这些天里提供的精神支持）~~或许这说明了契约式设计并非当前的主流设计模式，诸如利用assert进行契约规范或是TTD等模式要比撰写复杂而不易懂的规范来的简单直接的多。
最后感谢这次讨论区的各位算法dalao提供的算法思路，此次因为没对问题分析透彻的缘故，在讨论区提供了一个错误的算法，还好及时发现了错误。这样的探究在当下仍是有意义的，让我对SSSP问题有了更清晰的认识。同时也感谢这次提供了各类JML相关工具的dalao，没有大家这篇博客也就不会是这个样子了。