java - JML 无法捕获违反的前提条件

Question

在我的类 Test 中，我有一个名为 a 的五个 int 数组，以及将一个添加到所选单元格的方法 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 消息。