--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on December 2009 ---
More precisely, consider this code: //@ lemma mean_property2: \forall integer l, h; l <= h ==> l <= (l+h)/2 <= h; //@ ensures l <= \result <= h; Int foo(int l, int h) { return (l+h)/2; } Main() { int a = foo(maxint, maxint); } I can't test this with my installation because Beryllium1 doesn't verify mean_property2. If this lemma can be proved however, what result is Jessie supposed to give on this code? - Boris > Lemma mean_property2 DOES HOLD for int since in annotations, + means > addition on integers and not on ints. > - Claude