Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Problems with division in lemmas
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
  • Date: Thu, 16 Jul 2009 16:53:45 +0200
  • References: <283BBA28B2314A2ABCDA8F0487D9B207@AHARDPLACE>
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