JML语言理论基础

Java建模语言（Java Modeling Language，JML）是一种进行详细设计的符号语言，他鼓励你用一种全新的方式来看待Java的类和方法。JML是一种行为接口规格语言 （Behavior Interface Specification Language，BISL），基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。通过在Java代码中增加了一些符号，这些符号用来标识一个方法是干什么的，却并不关心它的实现。使用JML，我们就能够描述一个方法的预期的功能而不管他如何实现。通过这种方式，JML把过程性的思考延迟到方法设计中，从而扩展了面向对象设计的这个原则。

JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。JML引入了大量用于描述行为的结构，比如有模型域、量词、断言可视范围、预处理、后处理、条件继承以及正常行为（与异常行为相对）规范等等。

 

JML应用工具链

JML相应的工具链，可以自动识别和分析处理JML 规格。常用的有openjml，其使用SMT Solver来对检查程序实现是否满足所设计的规格(specification)。目前openjml封装了四个主流的solver：z3, cvc4, simplify, yices2。z3由Microsoft开发的，并已在github上开源：https://github.com/Z3Prover/z3 其正式发布版可通过https://www.microsoft.com/en-us/download/details.aspx?id=52270获得。cvc4由Standford开发，可以通过http://cvc4.cs.stanford.edu/downloads/下载。 

心得体会

三次作业做下来都是一直在进行各种重构，所以所还是要一开始就有清晰的思路。希望下个单元的作业会比较顺利。