Boost logo

Boost :

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/


Boost list run by bdawes at acm.org, gregod at cs.rpi.edu, cpdaniel at pacbell.net, john at johnmaddock.co.uk