草稿:JML
 | 本草稿尚未提交審核
提交前，请先查閱維基百科不是什麼，以免犯下常見錯誤。 要让草稿被接受，需要至少满足以下要求：
我们强烈不鼓励您創建與您自己、您所在的組織、其對手或其產品相關的條目。如果您仍要这么做，请申报利益冲突。 注意：若您提交之后，本模板出现在页面最下方，表示您已成功提交。
如何改善您的草稿
本草稿由WilliamSkyWalk（贡献·日志）於12天前最后编辑。 |  |
Java建模语言（英語：Java Modeling Language，缩写JML）是一种用于Java程式码的规约语言，使用 Hoare风格的前置条件、后置条件和不变式，并遵循契约式设计范式。
语法
[编辑]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 等价。