--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on October 2010 ---
> while(low <= high) { > ? ?//@ ensures low <= mid <= high; ? // this is the new annotation suggested > ? ?mid = low + (high - low) / 2; > > [...] the cut says > that it should not bother with this division: any other computation giving a > number between low and high would > make the program correct. This is a very interesting remark. If I understand correctly, it means I can make up an interpolation formula, and as long as I can prove that the interpolation part itself does not divide by zero or return an index out of the low..high range, I will get a verified interpolation search. This example has the potential to become my favorite illustration for advantages of design-by-contract. Probably with the computation of mid moved to a function, though, since the "statement contract" syntax confuses people at first (for instance, here, "ensures low <= mid <= high" is a contract on statement "mid = low + (high - low) / 2;". The property therefore applies just after this statement). Pascal