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: naghmeh.ghafari at cslabs.com (Naghmeh Ghafari)
- Date: Thu, 13 May 2010 16:06:27 -0700
- In-reply-to: <4BEAC8E6.1050107@inria.fr>
- References: <4BDF2C15.5010201@cslabs.com> <4BEAC8E6.1050107@inria.fr>
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 ? That's not exactly what I meant. I cannot verify the example below (with the given invariants in the inner loop) with HAVOC. The bubble sort example comes in the HAVOC package, and in the original code (with havoc annotation) there is another invariant for the inner loop. Below is the HAVOC annotated code where using Z3 , the post condition can be verified. ---------------------------- typedef int *PINT; __declare_havoc_bvar(_H_i); __declare_havoc_bvar(_H_j); #define array_elems(a,s,t) (__setminus(__array(a, sizeof(int), t) , __array(a, sizeof(int), s))) #define all_array_elems(a,t) array_elems(a,0,t) #define sorted(a,s) (__forall(__qvars(_H_i,_H_j), all_array_elems(a,s), _H_i <= _H_j ==> *_H_i <= *_H_j)) #define TRUE 1 #define FALSE 0 __requires(arr > 0) __requires(__forall(_H_i, all_array_elems(arr,size), __type(_H_i, PINT))) __requires(size > 0) __ensures(sorted(arr,size)) __modifies (all_array_elems(arr,size)) void bubble_sort(int *arr, int size) { __loop_invariant( __loop_modifies (all_array_elems(arr,size)) ) while (TRUE) { int aux = 0; int i = 0; __loop_invariant ( __loop_assert(0 <= i && i < size) __loop_assert(__forall(__qvars(_H_i,_H_j), array_elems(arr, aux, i+1), _H_i <= _H_j ==> *_H_i <= *_H_j)) __loop_modifies (all_array_elems(arr,size)) ) 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; } } ------------------------------------- I was trying to verifying the same code using Frama-C. Even if I translate the second loop_assert for the inner loop as following: @ loop invariant \forall int a,b; ((aux < a <= i+1) && (aux < b <= i+1) ==> (a <= b ==> arr[a] <= arr[b])); (which I am not sure if it is completely equivalent to the HAVOC notation), I still cannot use Frama-C to verify this code. Then I tried the implementation that was suggested by Pascal (on this mailing list) and I cannot verify even th eother implementation using Frama-C. I am relatively new to both tools. I have worked with Boogie and Z3 before, but not with HAVOC front end, so now exploring both HAVOC and jessie plugin at the same time. That's why I am trying to use the same implementation. I really appreciate any help and suggestions. > Regarding the termination of the loop: my guess is that by default, > havoc does not check termination. Yes, ture, havoc cannot check for termination. But with the above example, it comes back with an answer that the post-condition is verified. thanks, naghmeh > > - 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 > >
- Follow-Ups:
- [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
- 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: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] question about a simple example and jessie
- Prev by Date: [Frama-c-discuss] Jessie plugin
- Next by Date: [Frama-c-discuss] question about a simple example and jessie
- 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):