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] proving false and counter examples

Hello,

> Why is it difficult to determine if a formula is false?

It is difficult in this theoretical framework, which is optimized for
the verification of powerful functional properties at the detriment of
nice-to-haves such as the production of counter-examples.

The contract (between you and Jessie) is that if the proof obligations
are true, then the analyzed code is functionally correct. As soon as
there is a loop in the code, getting a false proof obligation ceases
to mean that the specification is incorrect (ideally, as exemplified
with a counter-example) and start to mean in most cases that you have
chosen the wrong loop invariant.

It would still be nice to know: when you get a "false" proof
obligation, you are *sure* that you need to refine your loop
invariant, whereas if you get a timeout, you may have the right proof
invariant and the best course may be to add a lemma or switch to Coq.
One work-around would be to launch the provers on the negation of the
proof obligation. Why developers must have their own opinion on
whether this is a good idea, and a desirable feature in Why.

Pascal

PS: I don't want to seem to be promoting my own stuff too much, but
the value analysis can tell that obviously false specifications are
obviously false. It won't provide a counter-example expressed in terms
of the function's inputs though, because it goes forward only.