--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on May 2010 ---
Naghmeh Ghafari wrote: > Hi, > > I am trying to verify a very simple bubble sort example, using jessie > (Beryllium). My default solver is Alt-Ergo. I used HAVOC (and Z3) to > verify this example, which was relatively straight forward. I am using > similar loop invariants, but still there is a safety property > 'variant decrease' that I can't verify. I think this is because of the > While(true) loop I have for which I cannot come up with a proper > strictly decreasing loop variant. I also cannot verify my post > condition. I appreciate any suggestions or hint. Hi, I'm very surprised that you could prove your post-condition with HAVOC. For me you need a smart loop invariant for the inner loop to prove it. Could you double-check the annotations you gave to havoc, and perhaps share the annotated file with us ? Regarding the termination of the loop: my guess is that by default, havoc does not check termination. - Claude > In my version of jessie, I cannot use #pragma > JessieTerminationPolicy (user). It is not recognized in my version. > > cheers, > naghmeh > > #define TRUE 1 > #define FALSE 0 > > > /*@ requires size > 0; > @ requires \valid(arr+ (0..size-1)); > @ ensures \forall int i; 0 <= i <= size - 2 ==> arr[i] <= arr[i+1]; > */ > > void bubble_sort(int *arr, int size) { > > while (TRUE) { > int aux = 0; > int i = 0; > > /*@ loop invariant 0 <= i && i <= size -1 ; > @ loop variant size - i; > @*/ > while (i < size-1) { > if (arr[i] > arr[i+1]) { > int tmp = arr[i]; > arr[i] = arr[i+1]; > arr[i+1] = tmp; > aux = i; > } > i++; > } > if (aux == 0) break; > } > } > > > > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |