--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on November 2008 ---
Hi, > > I added an assigns clause and a loop assigns but the post-condition cannot > be proven (Hydrogen). Is there something else missing or is it due to the > Hydrogen. > Loop assigns is not supported yet in the Jessie plugin, a warning is now issued. To better answer your question, we need precisions, such as: - what VC exactly are not proved - which ATP you use In your case, you are directly using quantifiers, for which is not easy to get automatic proofs. The best way is to hide quantifiers by defining equivalent predicates and logic functions with appropriate axioms, that should be expressed in a way that facilitates the proof by ATP. This last thing is probably the hardest part, and needs most of all experiments on the specific programs you want to prove, with the provers you want to use. To help the prood go through, it is usually a good idea to add logical assertions (//@ assert ...) that direct the proof, and help you understand which parts of a bigger formula are not proved. HTH -- Yannick -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081111/b7d06f47/attachment.html