Re: [boost] [contract] diff n1962

Subject: Re: [boost] [contract] diff n1962
From: Steven Watanabe (watanabesj_at_[hidden])
Date: 2010-04-10 11:49:49

AMDG

Lorenzo Caminiti wrote:
>     struct z {
>         static int counter;
>         int number;
>
>         CONTRACT_CLASS( (z)
>         (static) (invariant) ({ // Static class invariants (no object here).
>             CONTRACT_ASSERT( counter >= 0 );
>         })
>         (invariant) ({ // Non-static class invariants (`this` present).
>             CONTRACT_ASSERT( number <= counter );
>         }) )
>
>         ...
>     };
>
> Why does n1962 not support static class invariants?
>   

Would it be possible to have something like
CONTRACT_INVARIANT {
    // arbitrary code
};
CONTRACT_STATIC_INVARIANT {
    // arbitrary code
};

To me at least, this would look cleaner than having
all the parentheses.

> Finally, the use of CONTRACT_OLDOF(variable) requires programmers to
> explicitly indicate that the variable type is copyable using
> (copyable) in the function signature adding syntactic overhead.
>   

This kind of worries me.  Do you always make a copy
whether it's needed or not when the object is marked
as copiable?

> 12) CONSTANT-CORRECTNESS
> Block invariants are constant-correct in n1962 but not in
> Boost.Contract. (Class invariants and pre/postconditions are
> constant-correct in both n1962 and Boost.Contract.)
>
> Unfortunately, I do not know how to enforce constant-correctness of
> block invariants (and also of loop variants) for Boost.Contract
> because I cannot inject const within a code block:
>
>     class z {
>         void f() {
>             const { // Can't do this... so f() is not const and block
> invariants are also not const in this context...
>                 ... // block invariant here
>             }
>         }
>     };
>
> This is a limitation of Boost.Contract.
>   

You can pull the code block out into a separate function.

In Christ,
Steven Watanabe