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

for me:

//*@ lemma test1 : \forall integer x; x/1 == x; */
/*@ lemma test1b : \forall integer x; x != 0 ==> x/x == 1; */
/*@ lemma test2 : \forall integer x; x/x == 1; */
/*@ lemma mean1 : \forall integer x,y; x <= y ==> x <= (x+y)/2 <= y; */

test1, mean1 are proved by Alt-Ergo 0.9, which will hopefully be 
released very soon.

test2 is not proved, which is fortunate since it is wrong. But test1b is 
also not proved.

That's true that division is very poorly supported by SMT provers. E.g 
there is no SMT-LIB category involving division.

- Claude

Kerstin Hartig wrote:
> 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
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>   


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