--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on May 2012 ---
Le 09/05/2012 08:35, Boris Hollas a ?crit : > On Mon, 2012-05-07 at 20:31 +0200, Claude Marche wrote: >> /*@ requires \valid(AB_Ptr)&& \valid(CD_Ptr); >> @ behavior zero: >> @ assumes \exact(*AB_Ptr)> \exact(*CD_Ptr) ; >> @ ensures result == 1 >> @ behavior one: >> @ assumes \exact(*AB_Ptr)<= \exact(*CD_Ptr); >> @ ensures result == 0; >> @ */ > > I have a related question. Is \exact(x), when used in a precondition, > equivalent to x (if x is a parameter of the function)? No it isn't. On the contrary, there is no contraint at all between them. So when using \exact you typically need to put as precondition something like \abs(\round_error(x)) <= some constant > The example in > the ACSL documention suggests it isn't. Indeed. > Are Coq or Gappa required to use \exact and is user interaction > necessary to prove VCs? No and no. Indeed, if one uses the pragma JessieFloatModel(math) then Gappa is typically not needed, and regarding computation on real numbers, some automated provers perform quite well (CVC3, Z3, and sometimes Alt-Ergo). Coq is just an alternative in case the math is too complex for automated provers. Gappa is typically useful to prove something about rounding errors. A few examples of C programs with floats, specified with ACSL and proved with the Jessie-plugin are available at the URLs: http://proval.lri.fr/gallery/fp.en.html http://hisseo.saclay.inria.fr/gallery.html http://www.lri.fr/~sboldo/research.html Hope this helps, - Claude -- 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 |