java - JML は違反した前提条件をキャッチできません

Question

私のクラス Test には、a という名前の 5 つの int の配列と、選択したセルに 1 を追加するメソッド addOne(int index) があります。メソッドに渡されるインデックスを制御するための単純な前提条件を JML で記述しました。次に、負のインデックスでメソッドを呼び出すこの前提条件に違反しようとしましたが、JML はこのエラーをキャッチできません。どうしたの？

これはテストクラスです:

public class Test {

 public int[] a;

 public Test(){
    a = new int[]{1,1,1,1,1};
 }

 //@ requires index>=0 && index<5;
 public void addOne(int index){
    a[index]+=1;
 }
} 

そして、これはメインです：

public static void main(String[] args) {
    Test t = new Test();
    t.addOne(-2);
}

それは例外をスローします: java.lang.ArrayIndexOutOfBoundsException: -2.

任意の JML メッセージ。