使用 openJML 遍历矩阵答案

【问题标题】：Iterate through a matrix with openJML使用 openJML 遍历矩阵
【发布时间】：2016-09-27 10:20:09
【问题描述】：

我有一个类，其矩阵在特定位置初始化为全 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;

但它在构造函数之后给了我不变的错误。如何遍历矩阵来检查属性？

【问题讨论】：

标签： java matrix design-by-contract openjml

【解决方案1】：

经过大量研究，您似乎只能使用 \forall 来完成，其他命令对我不起作用。

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

所以，如果您正在处理多维数组，请不要使用 openJML

【讨论】：