JML及其工具链
JML发展概述及语法回顾
Java Modeling Language (JML)是一种接口行为规格描述语言，使用它我们可以快速建模接口行为，同时借助各种工具实现一些自动化的检查，确保程序各部分符合功能需求。
基本使用：
对接口的前置条件、后置条件及副作用进行断言式描述
requires pre-cond... // 前置条件ensures post-cond... // 后置条件signals ... // 抛出异常
使规格描述与预期的接口行为等价，则当接口的某个实现不符合规格时，可以借助JML检查工具快速发现并修复该实现
工具链
参考
The AspectJML tool is able to specify and do runtime assertion checking for both Java and AspectJ programs. Ajmlc uses aspect-oriented compilation techniques to provide significantly improved runtime assertion violation messages, and also works with JavaME.
AspectJML是一个为Java和AspectJ提供运行时断言检测的工具，支持一些面向切面编程的高级特性
The jml4c tool is a JML compiler built on the Eclipse Java compiler. It translates a significant subset of JML specifications into runtime checks. Notable features of JML4c include (1) support for Java 5 features such as generics and enhanced for loops, (2) support >for nested classes, (3) improved compilation speed, and (4) improved error messages. Using JML4c, one can now verify Java 5 classes annotated with JML specifications.
jml4c是一个基于Eclipse Java编译器的JML编译器，它可以将一部分JML规格翻译为运行时检查
Sireum/Kiasan for Java, which is a JML contract-based automatic verification and test case generation tool-set for Java program units.
Sireum/Kiasan是契约式的Java测试样例生成工具
JMLEclipse, which is a pre-alpha version of the JML tool-suite developed on top of Eclipse's JDT compiler infrastructure.
JMLEclipse是JML在Eclipse中的支持组件，目前仍处在开发阶段
JMLUnitNG is an automated unit test generation tool for JML-annotated Java code, including code using Java 1.5+ features such as generics, enumerated types, and enhanced for loops. Like the original JMLUnit, it uses JML assertions as test oracles. It >improves upon the original JMLUnit by allowing easy customization of data to be used for each method parameter of a class under test, as well as by using Java reflection to automatically generate test data of non-primitive types.
JMLUnitNG是一个针对JML自动化生成单元测试的工具，它支持Java5之后的高级语法特性，基于反射等特性为JML的检查提供语言层面和数据层面的易定制的扩展
JMLOK is a tool that uses random tests to check Java code against JML specifications and suggest likely causes for non-conformance problems it finds.
JMLOK是一个使用随机数据对JML规格进行检测的工具
尝试使用JMLUnitNG自动生成测试样例
对于如下测试代码：
package adder;public class Adder { /*@ public normal_behaviour @ ensures \result == a + b; */ public static int add(int a, int b) { return a + b; }} 运行：
java -jar jmlunitng.jar adder\Adder.java
生成测试文件，编译：
javac -cp jmlunitng.jar adder\*.javajava -jar openjml.jar -rac adder/adder.java
运行：
java -cp jmlunitng.jar adder.Adder_JML_Test
结果如下：
[TestNG] Running: Command line suitePassed: racEnabled()Passed: constructor Adder()Failed: static add(-2147483648, -2147483648)Passed: static add(0, -2147483648)Passed: static add(2147483647, -2147483648)Passed: static add(-2147483648, 0)Passed: static add(0, 0)Passed: static add(2147483647, 0)Passed: static add(-2147483648, 2147483647)Passed: static add(0, 2147483647)Failed: static add(2147483647, 2147483647)===============================================Command line suiteTotal tests run: 11, Failures: 2, Skips: 0===============================================
成功检测了算术溢出
架构梳理
三次作业中，MyRailSystem - MyGraph - MyPathContainer存在明显的继承层级关系。第三次作业为了引入观察者模式，为MyPathContainer实现了Registerable接口，同时将MyGraph的连通性查询改为并查集维护、bfs部分重新封装为BfsSpSolver，除此之外基本没有其他重构
第三次作业为了引入几种不同的最短路，抽象了SpSolver接口描述一个最短路计算类的基本行为，并在其上实现了BaseCachedSpSolver这个抽象基类，实现结果缓存、注册观察者等基本行为。再在此基础上实现了BfsSpSolver和DijSpSoverl，描述bfs和迪杰斯特拉的基本算法模型，前者替换第二次作业中最短距离的计算部分，后者将用于实现本次的三个变种最短路查询寻求。
本次的新增三种查询需求我使用的是1+x的拆点做法，参考讨论区，
三个问题的共同点是
- 边权与方向无关
- 从某个源点/汇点到一条path的边权为一个常数
- path上两点之间的权为一个常数或权值只与这两点的编号相关
所以很容易用继承关系实现复用。考虑到需求已固定，出于尽量简化架构规避错误的目的，没有进一步考虑有向图、可变权等更复杂需求的可扩展性。
类图：
注意到SpSolver使用观察者模式将自身注册入图对象，当发生图结构变更时图对象会通知所有已注册的观察者作出响应，在作业里响应的内容主要为清空缓存/将Solver状态标记为已更新
Bug汇总及测试相关
自己遇到的bug主要是算法实现方面的。在考虑缓存后对dij的中间结果可以予以保存，即对于起点是v的最短路，只要图结构未发生改变，其至所有结点的最短路可以在有限次运算后全部求出，求解顺序与终点u无关。但是若使用d(v,u)的中间结果计算d(u’,v)，则会破坏迪杰斯特拉算法的正确性导致错误。
互测中遇到的问题主要有：
- 不合理使用静态数组造成越界
- 使用迪杰斯特拉算法求解最短路时，使用一个固定的大常数作为INF值导致中间运算出现溢出或其他错误
个人认为这两个问题都是设计时欠缺工程化考虑或对问题边界缺乏分析造成的。
总结体会
本单元的主要内容是规格化编程及基于其的一系列实际问题。我认为这是很有启发性的一个单元，在契约式的开发过程中，每个单元模块、接口的功能由规格制定方描述，实现方负责实现功能以满足规格，这样的开发在团队中做到了提高效率与明确功能需求间的平衡。设计架构时，规格制定者不需要太过拘泥于具体的代码细节，只需要借助规格将功能界限描述清除，而实现者可以将目光更多地集中于接口中，而不需要关心代码的其他部分是如何耦合的，只需要满足规格即可满足程序正确运行。
除此之外，这个单元也让我意识到，好的代码架构不仅可以满足一般的逻辑需求，在应用某些特定算法追求性能时一个好的设计架构依旧能为我们带来效率与质量的收益。