--- layout: fc_discuss_archives title: Message 86 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 15:30 +0200, Virgile Prevosto wrote:
>   
>> No, jessie always generates a proof obligation corresponding to the
>> lemma. However, no automated prover will be able to discharge it
>> (otherwise, they would prove the PO from the ensures clause directly).
>> Thus, some additional work is needed (e.g. by using the coq output of
>> why).
>>     
>
> I don't understand that why no automatic prover will be able to prove a
> user-supplied lemma. Isn't this what SMT provers are supposed to do?
> I thought that a lemma is a way to reduce the search space for the
> prover by giving it a hint on how to prove the postcondition.
>
>   
Indeed, you are right and Virgile is not: It is possible that a prover 
proves both the lemma
and the assertion which need that lemma, but does not prove the 
assertion without the lemma.
So yes, a lemma may act as an hint.

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