--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on July 2009 ---
Hello, I tried to verify the code below as an example to our engineers. R_ges computes the resistance of two resistors in a parallel circuit. However, even with the help of two lemmata I provided, none of the proofs obligation can be verified. Is there a solution? Regards, Boris /*@ 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 ); } int main(void) { double R; R = R_ges(100, 200); return 0; }