Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] 2d array and \separated with WP
  • From: siegel at udel.edu (Stephen Siegel)
  • Date: Wed, 16 May 2018 05:07:00 -0400
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