--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on August 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Integer-arithmetics, rational postconditions



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,