Javaモデリング言語

Java Modeling Language ( JML ) は、 Javaプログラム用の仕様記述言語であり、 Hoare スタイルの事前条件、事後条件、および不変条件を使用し、契約による設計パラダイムに従います。仕様は、ソースファイルへのJava アノテーションコメントとして記述されるため、任意の Javaコンパイラでコンパイルできます。

ランタイムアサーションチェッカーや拡張静的チェッカー（ESC/Java）などのさまざまな検証ツールは、開発を支援します。

JMLは、Javaモジュールの振る舞いインターフェース仕様言語です。JMLは、Javaモジュールの振る舞いを形式的に記述するためのセマンティクスを提供し、モジュール設計者の意図に関する曖昧さを解消します。JMLは、 Eiffel、Larch、およびRefinement Calculusの理念を受け継ぎ、厳密な形式的セマンティクスを提供しつつ、あらゆるJavaプログラマが利用できるように設計されています。JMLの振る舞い仕様を利用する様々なツールが利用可能です。仕様はJavaプログラムファイル内の注釈として記述することも、別の仕様ファイルに保存することもできるため、JML仕様を持つJavaモジュールは、どのJavaコンパイラでも変更せずにコンパイルできます。

JML仕様は、コメント内の注釈の形でJavaコードに追加されます。Javaコメントは、@記号で始まる場合、JML注釈として解釈されます。つまり、次の形式のコメントはJML注釈として解釈されます。

//@ <JML仕様>

または

/*@ <JML仕様> @*/

基本的なJML構文では、以下のキーワードが提供されます。

requires

後続のメソッドに対する前提条件を定義します。

ensures

後続のメソッドに対する事後条件を定義します。

signals

後続のメソッドによって特定の例外がスローされた場合の事後条件を定義します。

signals_only

指定された前提条件が満たされた場合にスローされる可能性のある例外を定義します。

assignable

後続のメソッドによって値を割り当てることが許可されるフィールドを定義します。

pure

副作用のないメソッドであることを宣言します（assignable \nothing例外をスローする可能性もあります）。さらに、純粋メソッドは常に正常に終了するか、例外をスローするかのいずれかであるべきです。

invariant

クラスの不変プロパティを定義します。

loop_invariant

ループの不変条件を定義します。

also

仕様ケースを組み合わせることができ、メソッドがスーパークラスから仕様を継承していることを宣言することもできます。

assert

JMLアサーションを定義します。

spec_public

仕様策定の目的で、保護された変数またはプライベート変数をパブリックに宣言します。

基本的なJMLでは、以下の式も提供されています。

\result

後続のメソッドの戻り値を識別するための識別子。

\old(<expression>)

<expression>メソッドに入る時点での値を参照するための修飾子。

(\forall <decl>; <range-exp>; <body-exp>)

全称量化子。

(\exists <decl>; <range-exp>; <body-exp>)

存在量化子。

a ==> b

a暗示するb

a <== b

a暗示されているのはb

a <==> b

aかつその場合に限りb

論理積、論理和、論理否定を表す標準のJava構文も使用できます。JMLアノテーションは、アノテーション対象のメソッドのスコープ内にあり、適切な可視性を持つJavaオブジェクト、オブジェクトメソッド、演算子にもアクセスできます。これらを組み合わせて、クラス、フィールド、メソッドのプロパティの正式な仕様を提供します。たとえば、単純な銀行クラスのアノテーション付き例は次のようになります。

public class BankingExample { public static final int MAX_BALANCE = 1000 ; private /*@ spec_public @*/ int balance ; private /*@ spec_public @*/ boolean isLocked = false ; //@ public invariant balance >= 0 && balance <= MAX_BALANCE; //@ assignable balance; //@ ensures balance == 0; public BankingExample () { this . balance = 0 ; } //@ requires 0 < amount && amount + balance < MAX_BALANCE; //@ assignable balance; //@ ensures balance == \old(balance) + amount; public void credit ( final int amount ) { this . balance += amount ; } //@ requires 0 < amount && amount <= balance; //@ assignable balance; //@ ensures balance == \old(balance) - amount; public void debit ( final int amount ) { this . balance -= amount ; } //@ ensures isLocked == true; public void lockAccount () { this . isLocked = true ; } //@ requires !isLocked; //@ ensures \result == balance; //@ also //@ requires isLocked; //@ signals_only BankingException; public /*@ pure @*/ int getBalance () throws BankingException { if ( ! this . isLocked ) { return this . balance ; } else { throw new BankingException (); } } }

JML構文の完全なドキュメントは、JMLリファレンスマニュアルに記載されています。

JMLアノテーションに基づいた機能を提供するツールは数多く存在する。アイオワ州立大学のJMLツールは、JMLアノテーションをランタイムアサーションに変換するアサーションチェックコンパイラ、JMLアノテーションからの追加情報で拡張されたJavadocドキュメントを生成するドキュメントジェネレータ、そしてJMLアノテーションからJUnitテストコードを生成する単体テストジェネレータを提供している。jmlcjmldocjmlunit

独立したグループが、JMLアノテーションを利用するツールの開発に取り組んでいます。これには以下が含まれます。

• ESC/Java2これは、JMLアノテーションを使用して、従来よりも厳密な静的チェックを実行する拡張静的チェッカーです。
• OpenJMLは自らをESC/Java2の後継者と宣言している。
• Daikon は、動的な不変量生成器であり、2005 年 12 月 11 日にWayback Machineにアーカイブされました。
• KeYは、JMLフロントエンドとJMLの構文ハイライトをサポートするEclipseプラグイン（JML Editing）を備えたオープンソースの定理証明器を提供します。
• Krakatoa は、 Why検証プラットフォームに基づいてRocq証明アシスタントを使用する静的検証ツールで、 2009 年 5 月 8 日にWayback Machineにアーカイブされました。
• JMLEclipseは、Eclipse統合開発環境用のプラグインで、JML構文をサポートし、JML注釈を利用する様々なツールへのインターフェースを提供します。
• Sireum/Kiasanは、JMLを契約言語としてサポートする、記号実行に基づく静的解析ツールです。
• JMLUnitは、JML注釈付きJavaファイルに対してJUnitテストを実行するためのファイルを生成するツールです。
• TACOは、JavaプログラムがJavaモデリング言語仕様に準拠しているかどうかを静的にチェックするオープンソースのプログラム解析ツールです。

• Gary T. Leavensと Yoonsik Cheon。JMLとの契約による設計；ドラフトチュートリアル。
• Gary T. Leavens、Albert L. Baker、Clyde Ruby。「JML: 詳細設計のための表記法」; Haim Kilov、Bernhard Rumpe、Ian Simmonds (編)『ビジネスとシステムの振る舞い仕様』、Kluwer、1999年、第12章、175-188ページ。
• Gary T. Leavens、Erik Poll、Curtis Clifton、Yoonsik Cheon、Clyde Ruby、David Cok、Peter Müller、Joseph Kiniry、Patrice Chalin、およびDaniel M. Zimmerman。JMLリファレンスマニュアル（草稿）、2009年9月。HTML
• マリエケ・ユイスマン、ヴォルフガング・アーレント、ダニエル・ブランズ、マルティン・ヘンシェル。 JML による正式な仕様。 2014.ダウンロード (CC-BY-NC-ND)

• JMLウェブサイト