--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on October 2010 ---
On Fri, 2010-10-15 at 15:45 +0200, Pascal Cuoq wrote: > while(low <= high) { > > //@ ensures low <= mid <= high; // this is the new annotation suggested > 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. yes, but the time complexity may differ. > 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). you can also use mid = low + (high - low) / 2; //@ assert low <= mid <= high; Boris