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

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



Hello Boris,

Le mer. 25 nov. 2009 15:20:57 CET,
"Hollas Boris (CR/AEY1)" <Boris.Hollas at de.bosch.com> a ?crit :

> //@ lemma mean_property: \forall integer x,y; x <= (x+y)/2 <= y;
> 
> It doesn't verify with Alt-Ergo or Z3, which is correct since the lemma doesn't hold. However,

Oops, thanks for spotting that. I guess it would be better to write
examples of properties that are true in the documentation.

> 
> //@ lemma mean_property: \forall integer x,y; x <= y  ==>  x <= (x+y)/2 <= y;
> 
> still doesn't verify, as well as
> 
> //@ lemma mean_property: \forall int l, h; l <= l + (h-l)/2 <= h;
> 
> The latter is known by VCC without explicit specification. I therefore 

and without the constraint that l<=h ? If that's the case, there is a
problem. If the real formula is 
\forall int l, h; l<=h ==> l <= l + (h-l)/2 <= h;
it is proved (as well as the variant using (x+y)/2) by alt-ergo 0.9,
the latest available version. Z3 v2.0 (the version for linux on
why.lri.fr) fails to prove them indeed.

> assume that Z3 knows about this fact. How does Jessie handle such 
> formulas, are they passed to the SMT solver?

My guess would be that VCC/Boogie produces formulas in z3's own
language, while alt-ergo uses the smt language. I suspect that this is
due to the fact that smt's int theory does not contain division and
that z3 fails to interpret the div_int symbol chosen by Why to
represent it (Why not providing axioms over div_int doesn't help
either).

Hope this helps,
-- 
E tutto per oggi, a la prossima volta.
Virgile