--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Why 2.27 released



> 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