--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on July 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with real division



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;
}