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]

參考文獻

^ ^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 （中文）.

外部連結

JML website

[aop-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.

[gc-2] 宋玉婷; 孫文輝. 基于JML的标记—清扫垃圾收集验证. 計算機應用與軟體. 2014, 31 (9): 32–36. ISSN 1000-386X. Wikidata Q136721869 （中文）.

[1]

[2]