JML(The Java Modeling Language)を使ってみました。

JMLを選んだ理由は、「コメントに条件式を書く」というのが気に入ったことと、フリーで開発者が多いことです。
まずはダウンロード。
http://www.cs.iastate.edu/~leavens/JML/index.shtml
http://sourceforge.net/project/showfiles.php?group_id=65346
次に、(jml.dir)/bin/jmlenv.bat 内にあるパスを自分の環境に合わせて変えます。
そして、(jml.dir)/bin をパスに追加します。
適当なプログラムを書いてみます。（意図的にマチガイを埋め込んでいます）

class GCD {

    /*@ requires a>0 && y>0;
     @ ensures a % \result == 0 && b % \result == 0;
     @*/
    public static int gcd(int a, int b) {
        if (b == 0) {
            return a;
        }
        else {
            return gcd(b, a % a);
        }
    }

    public static void main(String[] args) {
        System.out.println(gcd(100,24));    // 4
        System.out.println(gcd(24,24));     // 24
        System.out.println(gcd(23,24));     // 1
        System.out.println(gcd(-32,24));    // ERROR
        System.out.println(gcd(0,24));      // 24
    }
}

契約の書き方が正しいかどうかチェックします。

C:\user\java\test\JML>jml GCD.java

コンパイルし、チェックコードが埋め込まれたクラスファイルを作ります。

C:\user\java\test\JML>jmlc GCD.java

クラスファイルを実行します。

C:\user\java\test\JML>jmlrac GCD

以下が修正したプログラムです。

class GCD {

    /*@ requires a>=0 && b>=0;
     @ ensures a % \result == 0 && b % \result == 0;
     @*/
    public static int gcd(int a, int b) {
        if (b == 0) {
            return a;
        }
        else {
            return gcd(b, a % b);
        }
    }

    public static void main(String[] args) {
        System.out.println(gcd(100,24));    // 4
        System.out.println(gcd(24,24));     // 24
        System.out.println(gcd(23,24));     // 1
//      System.out.println(gcd(-32,24));    // ERROR
        System.out.println(gcd(0,24));      // 24
    }
}

参考
http://www.cs.iastate.edu/~leavens/JML/prelimdesign/prelimdesign_toc.html