一. JML语言
1. 理论基础
首先，JML不是JAVA的一部分，它是一群研究者为JAVA设计的扩展部分，但还没有得到官方的支持。因此，JAVA编译器并不支持JML，所以要想JML起作用，只能采用类似openJML这样的第三方来编译，将JML 规格编译为运行时检查的语句，即RAC code(runtime assertion checking)。如果代码实现与其JML规格不一致，将引发运行时JML exception。
JML遵从契约式设计范式(DBC)，Design by contract是软件开发的一种方法，核心是类与其客户之间达成契约。JML是一种形式化的、 面向 JAVA的行为接口规格语言。
推荐一篇step by step以一个比较复杂的例子来讲解JML语法和设计的教程：https://www.ibm.com/developerworks/library/j-jml/
2. 应用工具链
- jmlrac: test for violations of assertions during execution
- ESC/Java2: static verification; compile-time proving that contracts are never violated
- jmldoc: javadoc-style documentation
- jmlc: assertion-checking compiler
- jml4c: a new JML compiler built upon the Eclipse JDT open-source platform
上述工具很多都已经不再维护（跟不上java的升级，大多支持到java 1.5）, 看大家抱怨openJML坑，就想找找有没有更好用的JML工具，结果发现openJML竟然是最好用的。
- openJML：目前对JML支持最好，维护最积极的JML编译器了
- jmlunit/jmlunitNG: unit testing tool
二. JMLUnitNG
三. 架构设计
1. 第一次作业
直接继承接口，简单地实现了两个类。
2. 第二次作业
为了更改方便，直接ctrl+v把MyPathContiner的代码复制到MyGraph。
3. 第三次作业
由于第二次作业比较复杂，再去动很可能出bug，于是在写第三次作业的时候对于第二次作业已有的代码我一行都没动，只是在MyGraph类里加了求连通块个数的Public的函数。这样一来bug少了，但新加的架构和已有的架构看起来很不协调。
看了std码之后，惊呼：我之前竟将所有代码都直接放在src文件夹下。好的分层设计应该像标程一样，起码得有多个文件夹吧，比如base,core,util,grpha等。
四. bug和修复情况
三次作业均无bug。
五. 心得体会
撰写：规格的撰写用到了很多离散数学的知识，掌握常见的几种模式后，就能够比较容易地写出一些简单函数的规格。以我目前的水平看，写代码还是要比写规格来得容易。
理解：实操中，我实际上是先看的指导书，对于含混的地方，（比如起点和终点相同的情况下，算不算换乘，最小费用算多少？同一路径中如果有环该怎么算？）我会去详细阅读规格，因为规格严谨的描述了某一个方法该干什么。（但这次直觉上的理解实际上更靠谱，比如同一路径中有环的情况，直觉上的理解是不用非得绕着环走一圈多余的路，但死扣规格，确实得绕，事后证明是老师或助教的规格写错了）。
原文地址：https://www.cnblogs.com/yifan-liu/p/10898286.html