--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on July 2009 ---
> /*@ 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