--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on June 2014 ---
Hi, Interesting example. Via the Jessie plugin, both three provers CVC3 2.4.1, Z3 3.2 and Z3 4.3.1 are able to prove your assertions, except of course the third (on 3.5) which is not true. A few remarks: 1) the axiom axiom exists_value: \forall real x; \exists integer n; lround(x) == n; is pretty useless since lround returns an integer 2) since your asserts does not depend on your code, they should be better stated as global lemmas, e.g. //@ lemma round30: lround(3.0) == 3; //@ lemma round31: lround(3.1) == 3; //@ lemma round35: lround(3.5) == 4; //@ lemma round39: lround(3.9) == 4; 3) I'm unable to prove that roundit(x) returns lround(x), but this is another story. Hope this helps, - Claude Le 19/06/2014 17:47, Frank Dordowsky a ?crit : > Thanks for the hints and the link. The blog is very impressive and was > surprising to me, but I must admit that I did not yet delve too much > into floating point analysis. > > Weakening the post-conditions leaves an ambiguity: if x == 3.5 for > example, both 3 and 4 satisfy the predicate. > > I nevertheless modified my definition of lround, and also added > another axiom that claims the existence of a function value: > > /*@ axiomatic Rounding { > @ logic integer lround(real x); > @ axiom exists_value: > @ \forall real x; \exists integer n; lround(x) == n; > @ axiom rounded_value: > @ \forall real x ; -0.5 <= (x - lround(x)) <= 0.5; > @ } > @*/ > > I have also tried one of the implementation examples of the blog, and > added some trivial assertions: > > // file: round.c > #include "round.h" > > int roundit(float x) > { > //@ assert lround(3.0) == 3; > //@ assert lround(3.1) == 3; > //@ assert lround(3.5) == 4; > //@ assert lround(3.9) == 4; > > if (x >= 0x1.0p23) return x; > return (int)(x+0.49999997f); > } > > I still cannot prove the post condition, but even the assertions are > not proved, which surprises me, and I have no explanation for it. > > Frank > _______________________________________________ > 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 | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |