--- layout: fc_discuss_archives title: Message 49 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



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