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] 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                    |