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