Проверьте транспонирование матрицы, используя frama-c -wp

Question

У меня есть проблема с проверкой функциональной правильности транспонирования матрицы, и эта проблема симптоматична для других, которые я использовал frama-c -wp.Я не уверен, как включить Frama-C лучше рассуждать о разделении памяти.В других сценариях я прибегал к индуктивным определениям (включая unchanged), но мне было бы интересно, если я что-то здесь упускаю.

Вот программа, которая проверяет минус пункт гарантированно о функциональной корректности.Я пытался переносить его как инварианты цикла, но, похоже, возникла проблема, и 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];
    }
  }
}

Например, вот некоторые инварианты, которые позволяют выполнить условие post, но нельзя доказать сохранение инварианта 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];
    }
  }
}

Мой вопрос заключается в том, чтобы обойти эту проблемуразделение памяти с использованием транспонирования в качестве эталона.Вот почему мне интересно, как можно вообще сформулировать здесь критерий правильности и доказать его.