Re: [boost] [contract] diff n1962

11 Apr 2010

      ----- Original Message ----- 
From: "Steven Watanabe" <watanabesj@gmail.com>
To: <boost@lists.boost.org>
Sent: Saturday, April 10, 2010 5:49 PM
Subject: Re: [boost] [contract] diff n1962
...
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.
I think that the major problem with this approach is that is no simple to inhibit the CP code when we don't want to include it. Boost.Contract defines a members in the class check the contract state. We could have a macro for that

#if defined CONTRACT_CHECK_CLASS_INVARIANT ||  \
        defined CONTRACT_CHECK_PRECONDITION || \
        defined CONTRACT_CHECK_POSTCONDITION   
#define BOOST_CONTRACT_STATE \
    friend class contract::state; \
    mutable contract::state contract_state_;
#else
#define BOOST_CONTRACT_STATE 
#endif // contracts

The library can provide also these macros

#define BOOST_CONTRACT_CLASS_STATIC_INVARIANT \
    static void contract_static_invariant_()

#define BOOST_CONTRACT_CLASS_INVARIANT \
    static void contract_invariant_()

Then we can do 

     struct z {
         static int counter;
         int number;

         BOOST_CONTRACT_STATE // (*)
        #if defined CONTRACT_CHECK_CLASS_INVARIANT // (*)
         CONTRACT_INVARIANT  {
             CONTRACT_ASSERT( counter >= 0 );
         }
         CONTRACT_STATIC_INVARIANT { 
             CONTRACT_ASSERT( number <= counter );
         }
        #endif // (*)
         ...
     };

Note the added lines with (*).

Do you think this is satisfactory?
...
...
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?
What do you think of storing in specific variables the old values and use them on the post condition. 
    (postcondition)((old_size) (this)->size())) ({
        CONTRACT_ASSERT( size() == (old_size + 1) );
    })

This has the advantage that only the used old values are copied. 
Do you see another alternative?
...
...
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.
Yes as Steven says, you can always define a function with the needed const qualifiers that checks for the block invariant. But IMHO this complicates things a lot. I don't think that I will use these kind of functions so help to ensure that Block invariants are constant-correct. This could be a minor and aceptable limitation of a library solution.

Best,
_____________________
Vicente Juan Botet Escribá
http://viboes.blogspot.com/

Re: [boost] [contract] diff n1962

vicente.botet