--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on July 2009 ---
On Christoph Weber's request I forward the following mail: ----------------------------- Integerdivision Hello, I am exploring the limitations of divisions and annotations and I would like to know, how many VC can be proven with your development tools: But I pay special attention to the terms connected with the division. Sincerely Christoph //==================================================================== /*@ lemma division: \forall integer x; 0 < x ==> 0 <= x/2; */ /*@ requires limit > 0; ensures limit == \result; */ int integerdivision(int limit) { int b = 1; int a = limit; int index = 0; int old_a=a; int old_b=b; /*@ loop invariant a/2 >= 0; loop invariant 0 <= a <= limit; loop invariant 1 <= b <= limit; loop invariant index == 0 ==> b == old_b; loop invariant index == 0 ==> a == old_a; loop invariant index > 0 ==> b == old_b/2; loop invariant index > 0 ==> a == old_a*2; */ while (0 < a) { old_a=a; old_b=b; a = a/2; b = b*2; index ++; } return b; } //====================================================================