--- layout: fc_discuss_archives title: Message 35 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



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                    |