草稿:JML
 | 本草稿尚未提交審核
提交前，請先查閱維基百科不是什麼，以免犯下常見錯誤。 要讓草稿被接受，需要至少滿足以下要求：
我們強烈不鼓勵您創建與您自己、您所在的組織、其對手或其產品相關的條目。如果您仍要這麼做，請申報利益衝突。 注意：若您提交之後，本模板出現在頁面最下方，表示您已成功提交。
如何改善您的草稿
本草稿由WilliamSkyWalk（貢獻·日誌）於40天前最後編輯。 |  |
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 等價。