frama-c - 使用 frama-c -wp 验证矩阵转置

Question

我在验证矩阵转置的功能正确性时遇到问题，这个问题是我使用过的其他人的症状frama-c -wp。我不确定如何让 Frama-C 更好地推理内存分离。在其他情况下，我使用了归纳定义（包括unchanged），但我想知道我是否在这里遗漏了一些东西。

这是一个验证程序，减去有关功能正确性的 Ensure 子句。我尝试将它作为循环不变量携带，但似乎存在问题，并且 Frama-C 被内存分离弄糊涂了。

所以作为一个挑战，你将如何验证矩阵转置？

#define N 100

/*@
requires 0 < rows < N;
requires 0 < cols < N;
requires 0 <= r < rows;
requires 0 <= c < cols;
ensures 0 <= \result < rows*cols;
 */
int index(int rows, int cols, int r, int c) {
  return r*cols+c;
}

/*@
predicate inv(int *a, int rows, int cols) =
  0 < rows < N && 0 < cols < N && \valid(a+(0..rows*cols-1));
*/

/*@
requires inv(a, cols, rows);
requires inv(o, rows, cols);
requires \forall int i; \forall int j; 0 <= i < rows*cols && 0 <= j < rows*cols ==> \separated(a+i, o+j);
requires \forall int i; \forall int j; 0 <= i < rows*cols && i < j < rows*cols ==> \separated(o+i, o+j);

ensures \forall int r; \forall int c; 0 <= r < rows && 0 <= c < cols ==> o[r*cols+c] == a[c*rows+r];

assigns o[0..rows*cols-1];
 */
void transpose(int *a, int *o, int rows, int cols) {
  int r = 0;
  /*@
    loop invariant 0 <= r <= rows;
    loop assigns r, o[0..rows*cols-1];
    loop variant rows - r;
  */
  for (int r = 0; r < rows; r++) {
    /*@
      loop invariant 0 <= c <= cols;
      loop assigns c, o[r*cols..(r+1)*cols-1];
      loop variant cols - c;
    */
    for (int c = 0; c < cols; c++) {
      o[r*cols+c] = a[c*rows+r];
    }
  }
}

例如，这里有一些使后置条件能够通过的不变量，但不能证明不变量 2、4、5 被保留。

/*@
requires inv(a, cols, rows);
requires inv(o, rows, cols);
requires \forall int i; \forall int j; 0 <= i < rows*cols && 0 <= j < rows*cols ==> \separated(a+i, o+j);
requires \forall int i; \forall int j; 0 <= i < rows*cols && i < j < rows*cols ==> \separated(o+i, o+j);

ensures \forall int r; \forall int c; 0 <= r < rows && 0 <= c < cols ==> o[r*cols+c] == a[c*rows+r];

assigns o[0..rows*cols-1];
 */
void transpose(int *a, int *o, int rows, int cols) {
  int r = 0;
  /*@
    loop invariant 0 <= r <= rows;
    loop invariant \forall int i; \forall int j; 0 <= i < r && 0 <= j < cols ==> o[i*cols+j] == a[j*rows+i];
    loop assigns r, o[0..rows*cols-1];
    loop variant rows - r;
  */
  for (int r = 0; r < rows; r++) {
    /*@
      loop invariant 0 <= c <= cols;
      loop invariant \forall int i; \forall int j; 0 <= i < r && 0 <= j < cols ==> o[i*cols+j] == a[j*rows+i];
      loop invariant \forall int j; 0 <= j < c ==> o[r*cols+j] == a[j*rows+r];
      loop assigns c, o[r*cols..(r+1)*cols-1];
      loop variant cols - c;
    */
    for (int c = 0; c < cols; c++) {
      o[r*cols+c] = a[c*rows+r];
    }
  }
}

我的问题是使用转置作为基准来解决内存分离问题。这就是为什么我想知道如何在这里制定正确性标准并证明它。

标签： frama-c