--- layout: fc_discuss_archives title: Message 84 from Frama-C-discuss on May 2010 ---
Boris Hollas wrote: > On Thu, 2010-05-20 at 13:44 +0200, Claude Marche wrote: > > >> The lemma itself is not proved of course, you have to convince yourself >> of its truth by other means: from human review to use of a proof assistant. >> > > Does that mean that Jessie/why doesn't prove a user supplied lemma? It generates a proof obligation for it, of course. If some automatic provers proves it you are happy, if not and if you are brave, you can use a proof assistant (and if you are not brave enough, try to convince yourself that it is true anyway) > The > ACSL reference is unclear on this, it states "Of course, a complete > verification of an ACSL specification has to provide a proof for each > lemma." It's unclear to me who has to provide this proof. > Quite a philosophical question, indeed ;-) Let me remind the main "theorem" behind the Jessie/Why plugin: if all the proof obligations are valid formulas, then the code satisfies its ACSL annotations. It does not tell you anything about who is going to guarantee that they are valid! - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |