--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on May 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] 2d array and \separated with WP



Hello Frama-C list,
I’m trying to prove (using WP) some simple programs dealing with 2-dimensional arrays, represented as arrays of pointers.   I’m running into trouble reasoning about separation.  Can anyone tell me if the following lemma is valid?   It may be that I am misunderstanding the meaning of \separated.  In any case, I haven’t been able to prove this lemma…

/*@
  predicate Sep2d(int **a, int n, int m) =
    \separated(a[0..n-1]+(0..m-1));

  predicate SepRows(int **a, int n, int m) =
    \forall integer i1, i2, j1, j2;
      (0<=i1<n && 0<=i2<n && i1!=i2 && 0<=j1<m && 0<=j2<m) ==>
        \separated(&a[i1][j1], &a[i2][j2]);

  lemma SepLem1: \forall int **a, int n, int m;
    (n>=0 && m>=0 && Sep2d(a, n, m)) ==> SepRows(a, n, m);

 */

One thing I noticed, using the Frama-C GUI and Why3 as prover, is that my Sep2d predicate seems to have been translated to “true”. 

Below is the actual function I am trying to prove, which copies a 2d array:

/*@
  predicate EqualRange(int *a, integer n, int *b) =
  \forall integer i; 0<=i<n ==> a[i] == b[i];

  predicate EqualRange2d(int **a, integer n, integer m, int **b) =
  \forall integer i; 0<=i<n ==> EqualRange(a[i], m, b[i]);

  predicate Valid2d(int **a, integer n, integer m) =
  \valid(a + (0..n-1)) && \valid(a[0..n-1] + (0..m-1));
 */

/*@ requires n>=0 && m>=0;
  @ requires Valid2d(a, n, m);
  @ requires Valid2d(b, n, m);
  @ requires \separated(a + (0..n-1), a[0..n-1] + (0..m-1), b + (0..n-1), b[0..n-1] + (0..m-1), &n, &m);
  @ assigns a[0..n-1][0..m-1];
  @ ensures EqualRange2d(a, n, m, b);
  @*/
void copy2d(int **a, int n, int m, int **b) {
  /*@ loop invariant i1: 0<=i<=n;
    @ loop invariant i2: EqualRange2d(a, i, m, b);
    @ loop assigns i, a[0..n-1][0..m-1];
    @ loop variant n - i;
    @*/
  for (int i=0; i<n; i++) {
    /*@ loop invariant 0<=j<=m;
      @ loop invariant z1: EqualRange2d(a, i, m, b);
      @ loop invariant z2: EqualRange(a[i], j, b[i]);
      @ loop assigns j, a[i][0..m-1];
      @ loop variant m - j;
      @*/
    for (int j=0; j<m; j++) {
      // I can’t prove the following assertion …
      //@ assert sep1 : \separated(&a[i][j], a[0..i-1] + (0..m-1));
      a[i][j] = b[i][j];
    }
  }
}

-Steve