Java建模语言

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

语法

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

关键字

requires

定义紧随其后方法的前置条件。

ensures

定义紧随其后方法的后置条件。

signals

定义当指定异常被方法抛出时的后置条件。

signals_only

定义在满足给定前置条件时允许抛出的异常。

assignable

定义方法可以修改的字段。

pure

声明方法无副作用（等同于 assignable \nothing，但也可抛出异常）。此外，纯方法应始终正常终止或抛出异常。

invariant

定义类的不变量属性。

loop_invariant

为循环定义循环不变量。

also

组合规范案例，也可声明方法继承自其超类型的规范。

assert

定义 JML 断言。

spec_public

将受保护或私有变量对规范公开。

表达式

\result

表示紧随其后方法的返回值标识符。

\old(<expression>)

引用方法开始时 <expression> 的旧值。

(\forall <decl>; <range-exp>; <body-exp>)

全称量词。

(\exists <decl>; <range-exp>; <body-exp>)

存在量词。

a ==> b

表示 a 蕴含 b。

a <== b

表示 b 蕴含 a。

a <==> b

当且仅当 a 与 b 等价。

优势

发展

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