Java建模语言

Java建模语言（，缩写JML）是一种用于Java程式码的规约语言，使用 Hoare风格的前置条件、后置条件和不变式，并遵循契约式设计（）范式。由于JML是为Java专门定制的，其基本语法结构以及编程风格都跟Java语言十分相似。

语法
JML规范以注释的形式添加到Java代码中。

关键字
; requires : 定义紧随其后方法的前置条件。
; ensures : 定义紧随其后方法的后置条件。
; signals : 定义当指定异常被方法抛出时的后置条件。
; signals_only : 定义在满足给定前置条件时允许抛出的异常。
; assignable : 定义方法可以修改的字段。
; pure : 声明方法无副作用（等同于 assignable \nothing，但也可抛出异常）。此外，纯方法应始终正常终止或抛出异常。
; invariant : 定义类的不变量属性。
; loop_invariant : 为循环定义循环不变量。
; also : 组合规范案例，也可声明方法继承自其超类型的规范。
; assert : 定义 JML 断言。
; spec_public : 将受保护或私有变量对规范公开。

表达式
; \result : 表示紧随其后方法的返回值标识符。
; \old() : 引用方法开始时 的旧值。
; (\forall ; ; ) : 全称量词。
; (\exists ; ; ) : 存在量词。
; a ==> b : 表示 a 蕴含 b。
; a : 表示 b 蕴含 a。
; a b : 当且仅当 a 与 b 等价。

优势
发展
Rebêlo等人提出并实现了一种新的JML编译器，称为ajmlc（AspectJ JML Compiler），利用了面向方面编程（AOP）机制来处理JML契约的运行时断言检查。结果表明该编译器生成的代码大小的开销非常小，适合Java ME应用程序使用。

参考文献
外部链接

• [http://www.eecs.ucf.edu/~leavens/JML/index.shtml JML website]