--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on May 2010 ---
[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.