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

I did not know about these slides. I had a look at them, and can find an 
obvious mistake in the post-condition they give:

  \forall integer a; ... ==> \exists integer b; 0 <= b < tam ==> ...

The second "==>" should have been "&&" of course

Unfortunately, I do not know any way to check if someone's specification 
is inconsistent.

The mistake "\exists x; A ==> B" is indeed quite common. For some time, 
I tried to promote the JML syntax
which allows to write "\forall x; A; B" for "\forall x; A ==> B"  and 
"\exists x; A; B" for "\exists x; A && B" but I got no success among the 
ACSL designers.

An argument against is that, as far as I know, there is no such 
syntactic sugar in proof assistants like Coq, Isabelle, PVS, etc.

General speaking, checking inconsistency of user's specifications is 
something we would like to have: any suggestions welcome!

- Claude





>
>
>
>> 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
>