# 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

*Subject*: [Frama-c-discuss] question about a simple example and jessie*From*: pascal.cuoq at gmail.com (Pascal Cuoq)*Date*: Sun, 16 May 2010 14:13:27 +0200*In-reply-to*: <AANLkTimC8urWahq3ptbCx-KehmfOz-4H2r91hmjkCQlS@mail.gmail.com>*References*: <4BDF2C15.5010201@cslabs.com> <x2xb15d09071005031421v51333b13ma27dc52ec76a51dc@mail.gmail.com> <4BEC6D3B.8060105@cslabs.com> <4BEF92A7.2030706@inria.fr> <AANLkTimC8urWahq3ptbCx-KehmfOz-4H2r91hmjkCQlS@mail.gmail.com>

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

**References**:**[Frama-c-discuss] question about a simple example and jessie***From:*naghmeh.ghafari at cslabs.com (Naghmeh Ghafari)

**[Frama-c-discuss] question about a simple example and jessie***From:*pascal.cuoq at gmail.com (Pascal Cuoq)

**[Frama-c-discuss] question about a simple example and jessie***From:*naghmeh.ghafari at cslabs.com (Naghmeh Ghafari)

**[Frama-c-discuss] question about a simple example and jessie***From:*Claude.Marche at inria.fr (Claude Marche)

**[Frama-c-discuss] question about a simple example and jessie***From:*pascal.cuoq at gmail.com (Pascal Cuoq)

- Prev by Date:
**[Frama-c-discuss] question about a simple example and jessie** - Next by Date:
**[Frama-c-discuss] ANN: cil-0.0.1** - Previous by thread:
**[Frama-c-discuss] question about a simple example and jessie** - Next by thread:
**[Frama-c-discuss] question about a simple example and jessie** - Index(es):