--- layout: fc_discuss_archives title: Message 82 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



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? 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.