--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on August 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Integer-arithmetics, rational postconditions



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                    |