--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on August 2010 ---
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,