gbalduzzi gbalduzzi - 4 months ago 14
Java Question

Iterate through a matrix with openJML

I have a class with a matrix initialized with all 0 and 1 in a specific position:

public class MatrixTest {
/*@ spec_public @*/ int[][] griglia;

//@requires true;
//@ensures griglia[2][3] == 1;
public MatrixTest() {
griglia = new int[6][6];

for (int i=0; i < 6; i++) {
for (int j=0; j < 6; j++){
griglia[i][j] = 0;
}
}

griglia[2][3] = 1;

}
}


I would like to add an invariant to check that i always have only one 1 cell with a value of 1 and 35 cells with a value of 0. I tried doing that:

//@ public invariant (\num_of int i, j; i >= 0 && i < 6 && j >= 0 && j < 6; griglia[i][j] == 1) == 1;


But it gives me invariant error just after the constructor. How can i iterate through a matrix to check a property?

Answer

After a lot of research, it seems like you can only do it with \forall, other commands didn't work for me.

\forall int i; i >= 0 && i < matrix.length; (\forall int j; j >= 0 && j < matrix[i].length; /* your check here */)

So, just don't use openJML if you are working with multi-dimensional arrays