Re: [boost] [contract] diff n1962

Subject: Re: [boost] [contract] diff n1962
From: vicente.botet (vicente.botet_at_[hidden])
Date: 2010-04-11 12:35:39

----- Original Message ----- 
From: "Steven Watanabe" <watanabesj_at_[hidden]>
To: <boost_at_[hidden]>
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/