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

[Frama-c-discuss] Lemma from ACSL doc doesn't verify



Hollas Boris (CR/AEY1) wrote:
> Oops, sorry I meant
>
> //@ lemma mean_property: \forall int l, h; l <= h  ==>  l <= l + (h-l)/2 <= h;
>
> still doesn't verify. I haven't tried the latest version of why however. I have AltErgo 0.7.3 and Z3 1.3.
>
> -Boris
>
> _______________________________________________
> 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
>   
As far as I know, SMT provers do not know the division operator, so it 
is not surpriseing they don't verify these.
For Alt Ergo 0.9, a few set of axioms for div are known, so these lemma 
verify.

But the way, for using these lemmas in your codes, PLEASE USE TYPE 
integer INSTEAD OF TYPE int

/@ lemma mean_property: \forall integer l, h; l <= h  ==>  l <= l + (h-l)/2 <= h;


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