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] Problem with real division

> /*@ lemma div1 : \forall real x; x > 0 ==> 1.0/x > 0;
>    lemma add1:  \forall real x,y; x > 0 && y > 0 ==> x+y > 0;
> */
>
> /*@ requires R1 > 0 && R2 > 0;
>    ensures \result > 0;
> */
> double R_ges(double R1, double R2)
> {
>  return 1.0/( 1.0/R1 + 1.0/R2 );
> }

If what you want to verify is the program, with its floating-point
operations, and not a model of the program where the computations
are made with reals, it's going to be rather difficult.

The lemma div1 is true with finite doubles, but for entirely different  
reasons
than make it true for reals. It wouldn't be true with 1e-16 for the  
constant
instead of 1.0.

If your objective is to ensure that R_ges does not return +infinity,
then proving that the divisor is >0 is not enough.

Whether you are interested in computations on doubles or on reals,
you would have better chances with the tool Gappa,
which does not analyze C programs but understand both
real and floating-point arithmetic and is able to provide powerful
results on floating-point computations.

http://lipforge.ens-lyon.fr/www/gappa/

Pascal

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090729/67b8ffc7/attachment.htm