--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on July 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problems with division in lemmas



On Christoph Weber's request I forward the following mail:
-----------------------------

Hello,

I am exploring the possibilitys of lemmas to assist proofs.

As I allready mentioned before, I cannot proof the lemma (mean) you provided
with any prover.

It seems to me, that the division within prevents a solution.
For example the following:

/*@ lemma test1 : \forall int x; x/1 == x; */
/*@ lemma test2 : \forall int x; x/x == 1; */

The computations would result in unknowns.

I would like to know if this is a general problem and if there is a way to
circumvent it.

Sincerely

Christoph