--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on May 2010 ---
> 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]); } } }