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 14:20:59 -0700
- In-reply-to: <x2xb15d09071005031421v51333b13ma27dc52ec76a51dc@mail.gmail.com>
- References: <4BDF2C15.5010201@cslabs.com> <x2xb15d09071005031421v51333b13ma27dc52ec76a51dc@mail.gmail.com>
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
- Follow-Ups:
- [Frama-c-discuss] question about a simple example and jessie
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [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: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] question about a simple example and jessie
- Prev by Date: [Frama-c-discuss] Jessie does not have "-jessie-no-regions" option anymore?
- Next by Date: [Frama-c-discuss] Jessie plugin
- 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):