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

[Frama-c-discuss] question about a simple example and jessie



> Another interesting
> tidbit is that Jessie is (probably rightly so) worried about integer
> overflows. Requiring an upper bound for tam seem to help prove some
> sub-properties.

My mistake: after fixing was was really wrong, the upper bound on tam
was not helping any more, so I removed it.

I changed the inner loop invariant to make it more readable to me, but
I don't know if the old one was wrong or not.

The way to prove the post-condition:

 ensures \forall integer a; 0 <= a < tam
             ==> (\exists integer b; 0 <= b < tam
                && \old(vector[b]) == vector[a]) ;

is probably to prove that the property is preserved at each step of
the computation, that is, to include the same property in both the
inner and outer loop invariants. I named that property "SameElements".
I didn't get alt-ergo to prove either initialization (for the outer
loop!) or preservation (for the inner loop) of that invariant, but at
least the post-condition is proved from it.

Note that the specification is not a complete specification of a
sorting algorithm as one could expect: a function that copied
vector[0] all over vector would satisfy it. But it would be a good
milestone to verify this specification before moving up to a complete
one, and a good second milestone on the way would be to add the
post-condition SameElements{Old, Here}(vector, tam) to the contract.

Frama-C 20100401 (Boron), Why 2.24 patched, alt-ergo 0.9, command-line:

frama-c -jessie b.c

_______

# pragma SeparationPolicy(none)

/*@ predicate Sorted{L}(int *a, integer l, integer h) =
    \forall integer i; l <= i < h ==> a[i] <= a[i+1] ;
*/

/*@ predicate SameElements{Hr, Thr}(int *v, integer tam) =
  \forall integer a; 0 <= a < tam
    ==> (\exists integer b; 0 <= b < tam
        && \at(v[b],Hr) == \at(v[a],Thr)) ;

*/

/*@
    requires \valid(i) ;
    requires \valid(j) ;
    assigns *i, *j;
    ensures *j == \old(*i) ;
    ensures *i == \old(*j) ;
*/
void swap (int *i, int *j)
{
  int tmp=*i;
  *i = *j;
  *j = tmp;
}

/*@
  requires 0 < tam ;
  requires \valid_range(vector, 0, tam-1) ;
  assigns vector[0..tam-1] ;
  ensures SameElements{Here, Old}(vector, tam) ;
  ensures Sorted(vector, 0, tam-1) ;
*/
void bubbleSort(int *vector, int tam)
{
  int j,i;
  j = i = 0;

  /*@
    loop invariant 0 <= i <= tam ;
    loop invariant Sorted{Here}(vector, tam-i-1, tam-1) ;
    loop invariant 0 < i < tam
      ==> \forall int a, b; 0 <= b <= tam-i-1 <= a < tam
        ==> vector[a] >= vector[b] ;
    loop invariant SameElements{Here, Pre}(vector, tam) ;
    loop variant tam-i ;
  */
  for (i=0; i<tam; i++)
    {
      /*@
	loop invariant 0 <= j < tam-i ;
	loop invariant
	   \forall int a; 0 <= a < j
	      ==> vector[a] <= vector[j] ;
        loop invariant SameElements{Here, Pre}(vector, tam) ;
	loop variant tam-i-j-1 ;
      */
      for (j=0; j<tam-i-1; j++)
	{
	  if (vector[j] > vector[j+1])
	    swap(&vector[j], &vector[j+1]);
	}
    }
}