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



Thanks for the pointer. I actually tried the example in the slides with 
Frama-C and Alt-Ergo and CVC3 as solvers. I get 'unknown' and 'timeouts' 
for 5 of the loop invariants, but I still get a green bullet for the  
post-condition. Although the slides show that CVC3 can verify all of the 
conditions, but they don't pass in the version I am running (i.e. CVC3 
2.2 ). I tried to do a sanity check by negating the post-condition and I 
still get the green bullet for the post-condition.  That doesn't sound 
right, or am I missing something obvious here?

thanks,
naghmeh



> Pedro Pereira and Ulisses Costa, brilliant students with excellent
> taste in the choice of their personal projects, proved the correctness
> of a bubble sort algorithm a while back (including termination).
> Looking at their slides briefly, it seems that the difficult part was
> first finding the invariant for the outer loop (slide 28) and that
> once you had that, it became a little clearer in which direction to
> look for the variant. In their version, there was a program variable
> that expressed almost directly how much of the (end of the) array was
> sorted (that variable was named i in their program).
>
> In yours, there doesn't seem to be such a variable, but you can always
> add to the program a ghost variable and ghost statements to make the
> logic of the loop clearer. Then the loop invariant and variant would
> be expressed in function of this ghost variable. To make your version
> somewhat similar to theirs, the ghost variable would represent the
> number of iterations of the outer loop so far.
>
> http://www.slideshare.net/UlissesCosta/correct-sorting-with-framac
>
> Good luck,
>
> Pascal
>
> _______________________________________________
> 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
>    
wha

-- 
Naghmeh Ghafari, Ph.D.
Research Associate
Critical Systems Labs, Inc.
Tel: (604) 638 7393
Cell: (778) 994 4802