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] 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]);
	}
    }
}