JML理论基础及应用工具链
理论基础
JML，Java 建模语言，可以规范 java 类和接口的设计。JML是一种行为接口语言，也就是说，其规范了java代码的行为和语义接口。java 类和接口的语义规范包括其方法签名，名字和域的类型等。这通常指的是 API 。java 类和接口的行为接口描述了编程者使用这个 API 的方式。就行为来说，JML 可以对方法的前置条件与后置条件细化，以及类的不变式等。这属于契约编程。
工具链
最基本的工具是 parsing 和 typechecking，这由 jml (developed at Iowa State University) 实现。
Runtime assertion checking，这样的运行时检查由JML编译器 jmlc 实现。
Static checking and verification，包括 ESC, LOOP, JACK 等一些工具。
Generating specifications，包括 Daikon, Houdini, jmlspec tool，可以帮助编写 JML 规范。
Documentation，jml-doc, 可以产生保护API和规范的 HTML 网页。
Unit Testing, jmlunit，可以根据 JML规范生成相应的单元测试。
JMLUnitNG
下面选取几个生成的测试函数。
可以看到，其主要是测试空对象，异常条件，以及边界数据。
架构设计
上图清晰地反映了自己的架构思路。每一次作业都是通过继承上一次作业实现的类并实现本次作业所需的接口完成。
bug和修复
第一次作业：
bug:自己实现整数列表的compareTo方法时直接将两个整数作差，没有考虑溢出。
fix:使用Integer.compareTo()方法。
lesson:不要重复造轮子；当涉及算术运算时，必须考虑溢出这个常见的bug。
第二次作业：
bug1:两个相同的点一定相连，其不一定有边连接。
fix1:对于特殊情况特殊判断。
lesson1:需要考虑清楚特殊情况，注意积累特殊情况。这次的特殊情况是点不存在、点相同无自环、点相同且有自环连接。（需要看清楚需求）
bug2:自己的floyd算法实现不够高效，使用了哈希查询，使得时间超出。
fix2:改用数组查询。
lesson2:虽然都是常数查询，但由于查询操作量很大，致使常数因子发挥了重要影响。自己以后需要考虑在哪些情况下需要考虑算法常数因子的影响。
第三次作业：
bug1:当某条边属于多个路径时无法正确处理。
fix1:对每条边维护一个路径集合。
lesson1:自己不应事先对图做出任何假设，即要考虑任意情况，测试时也是如此。
bug2:对floyd算法理解不够，导致自己没有意识到在查询边权时若换乘则修改的实现对于floyd算法并不可行，破坏了迭代条件。
fix2:使用dijkstra算法。
lesson2:对于某个算法应理解其原理，在条件变化后不应想当然地认为依然成立，而应证明。
规格撰写和理解的心得体会
对于一个编程任务，编写过程并不是最重要的，也不是最花时间的。其中设计是很重要的。通过契约编程的思想，将设计由自然语言变为JML规格，使得其更为清晰，并且可以由工具来检查规格与实现的不一致。这样进一步分离了设计与实现。
JML规格通过谓词逻辑与java自带的保证正确性的函数来描述自己程序的行为，从效果入手，这给了与实现者不一样的视角，有助于更好的理解自己的程序，写出bug少的程序。
原文地址：https://www.cnblogs.com/yorkyer/p/10907827.html