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

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