# 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] Axiomatic Definition of Rounding Function

*Subject*: [Frama-c-discuss] Axiomatic Definition of Rounding Function*From*: Claude.Marche at inria.fr (Claude Marché)*Date*: Mon, 23 Jun 2014 10:07:41 +0200*In-reply-to*: <alpine.LNX.2.03.1406191745590.1273@dordowsky.de>*References*: <alpine.LNX.2.03.1406190917260.1273@dordowsky.de> <CAOH62Jh78V2ja1fHAOY7Hmy1q+NCOkMHzD_Zd6f6HhRroDDAdA@mail.gmail.com> <alpine.LNX.2.03.1406191745590.1273@dordowsky.de>

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 |

**References**:**[Frama-c-discuss] Axiomatic Definition of Rounding Function***From:*frank at dordowsky.de (Frank Dordowsky)

**[Frama-c-discuss] Axiomatic Definition of Rounding Function***From:*pascal.cuoq at gmail.com (Pascal Cuoq)

**[Frama-c-discuss] Axiomatic Definition of Rounding Function***From:*frank at dordowsky.de (Frank Dordowsky)

- Prev by Date:
**[Frama-c-discuss] Using frama-c script to get proof obligations** - Next by Date:
**[Frama-c-discuss] Axiomatic Definition of Rounding Function (Claude March?)** - Previous by thread:
**[Frama-c-discuss] Axiomatic Definition of Rounding Function** - Next by thread:
**[Frama-c-discuss] Example to understand -slevel influence on Value analysis's result** - Index(es):