1

In my class Test I've an array of five int named a, and the method addOne(int index) that add one to the selected cell. I wrote in JML a simple precondition to control the index passed to the method. Then I try to violate this precondition calling the method with a negative index and JML can't catch this error. What's wrong?

This is Test class:

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;
 }
}

And this is the Main:

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

That throw the exception: java.lang.ArrayIndexOutOfBoundsException: -2.

With any JML message.

MaleMale
  • 11
  • 2
  • What are you doing to check this JML condition? (The Java compiler does not interpret JML; it's just a comment) – user253751 Jul 08 '15 at 11:00
  • I follow this step to enalbe JML for this project: Right click on the project -> Enable JML on this project. JML is written in comment line, i don't know why but when I try to violate a postcondition (//@ ensures condition) it works, but not for a precondition. – MaleMale Jul 08 '15 at 13:39

0 Answers0