Итерация по матрице с 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, если вы работаете с многомерными массивами