--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on May 2018 ---
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