Итерация через матрицу с openJML

Question

У меня есть класс с матрицей инициализируется со всеми 0 и 1 в определенном положении:

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; 

    } 
} 

Я хотел бы добавить инвариант, чтобы проверить, что я всегда есть только один 1 ячейка со значением 1 и 35 ячеек со значением 0. Я пытался сделать это:

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

Но это дает мне инвариантного ошибку только после того, как конструктор. Как я могу перебирать матрицу, чтобы проверить свойство?

Answer 1

После многих исследований кажется, что вы можете делать это только с помощью \ forall, другие команды не работают для меня.

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

Таким образом, просто не использовать openJML, если вы работаете с многомерными массивами