--- layout: fc_discuss_archives title: Message 84 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Small function with Shifting



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                    |