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/下载。

心得体会

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

05-02 19:41