0

特定の位置にすべて 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 セルと値が 0 の 35 セルが常に 1 つしかないことを確認したいと思います。

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

しかし、コンストラクタの直後に不変エラーが発生します。プロパティをチェックするためにマトリックスを反復処理するにはどうすればよいですか?

4

1 に答える 1

1

多くの調査の結果、\forall でしか実行できないようです。他のコマンドは機能しませんでした。

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

したがって、多次元配列を使用している場合は、openJML を使用しないでください。

于 2016-07-12T10:23:05.963 に答える