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]
参考文献
编辑- ^ 1.0 1.1 张进; 何成万; 石尤. 基于AOP的契约定义及其与JML契约的转换. 武汉工程大学学报. 2020, 42 (4): 456–461 [2025-11-07]. ISSN 1674-2869. doi:10.19843/j.cnki.cn42-1779/tq.201912025.
- ^ 宋玉婷; 孙文辉. 基于JML的标记—清扫垃圾收集验证. 计算机应用与软件. 2014, 31 (9): 32–36. ISSN 1000-386X. Wikidata Q136721869 （中文）.
