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]