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

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
>