--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on August 2010 ---
Hi, As Pascal suggested, a trick enforcing the use of division in R instead of Z might help. E.g. ensures \result / 2.0 > x which seems simpler than (\result + 0.0) / 2 to me. However, you might want to enforce the mapping of the division into the division of Q in Coq, instead of R. A way to do it is to introduce your own axiomatization of Q /*@ axiomatic Rat { logic type rat; logic rat rat_of_int(integer n); logic rat frac(integer n, integer d); predicate rat_gt(rat x, rat y); .... } */ and then use //@ ensures rat_gt(frac(\result,2),rat_of_int(x)); and finally, in the Coq generated file, map rat, rat_of_int, etc... to the corresponding symbols of the Coq library. Hope this helps, - Claude Michael Schausten wrote: > Hello, > > I have a function doing calculations based on integers. However, I'd > like to verify the conditions wit Coq based on rational arithmetic. A > simple example: > > /*@ requires x > 0; > ensures (\result / 2 > x); > */ > int function1(int x) { > return (2*x + 1); > } > > With the normal integer arithmetics, (\result / 2 == x) would be > correct. What I'd like to do is cast \result and x to rationals and do > a rational division, so that the ensures-part as above is correct. Is > this possible? > > Sincerely, > > _______________________________________________ > 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 | 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 |