迭代通過與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