Re: [boost] [contract] diff n1962

Subject: Re: [boost] [contract] diff n1962
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2010-04-11 23:27:59

Hello,

On Sun, Apr 11, 2010 at 12:35 PM, vicente.botet
<vicente.botet_at_[hidden]> wrote:
> From: "Steven Watanabe" <watanabesj_at_[hidden]>
>> 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

This is possible, in fact you could use `void contract_invariant_()
const {...}` directly without any macro (the state, class type, etc
will eventually remain in CONTRACT_CLASS( (class-type) (base-type1)
(base-type2) ... )). However, this has the following drawbacks:

1) As indicated by Vicente programmers will have to add the #ifdef to
remove contract code when invariants are not checked. However, it was
proposed by Andrzej to always leave contract code there so it is
compiled and checked syntactically (this could be implemented in the
future) -- Boost.Contract will not execute invariant checking at
run-time when CONTRACT_CHECK_CLASS_INVARIANT is #undef anyway.

2) However, this is NOT possible for member functions because they
have result value and arguments. Therefore, CONTRACT_FUNCTION() will
need to use the parenthesis for (precondition) and (postcondition).
Given that, I think it is better for the library to provide a
consistent interface across both its macros CONTRACT_FUNCTION() and
CONTRACT_CLASS() therefore using (invariant). What do you think?

Let me unveil the macro magic so this will become more clear:

    template<typename T>
    class myvector: public pushable<T> {

        CONTRACT_CLASS( (myvector) (pushable<T>)
        (invariant) (
            ( (size() == 0) == empty() )
        ) )

        CONTRACT_FUNCTION(
        (void) (push_back)( (const T&)(element) ) (copyable)
            (precondition) (
                ( size() < max_size() )
            )
            (postcondition) (
                ( size() == (CONTRACT_OLDOF(this)->size() + 1) )
            )
        ({
            vector_.push_back(element);
        }) )

        ...
    };

Expands to code equivalent to:

    template<typename T>
    class myvector: public pushable<T> {

        // CONTRACT_CLASS() expands to:
        typedef myvector contract_class_type_;
        typedef pushable<T> contract_base_type0_;
        friend class contract::state;
        mutable contract::state contract_state;
        static void contract_static_invariant_() { // (1)
        }
        void contract_invariant_() const { // (2)
            if (!((size() == 0) == empty())) throw
contract::failure(__FILE__, __LINE__, "(size() == 0) == empty()");
        }

        // CONTRACT_FUNCTION expands to:
    public: void push_back(const T& element) {
            contract_push_back_element_().call(this, element);
        }
    private: void contract_precondition_push_back_element_(const T&
element) const {
             ... // preconditions throwing contract::failure()
        }
    private: void contract_postcondition_push_back_element_( // (3)
                const contract_class_type* old_this,  // old value for
object this
                const T& element, contract::noold // no old value  for element
                ) const {
             ... // postconditions throwing contract::failure()
        }
    protected: void contract_body_push_back_(const T& element) { // (4)
            vector_.push_back(element);
        }
    protected: struct contract_push_back_element_:
contract::nonstatic_member_function<
                void (contract::copyable<contract_class_type>*, const
T&), // contracted member function type
                contract_base_type::contract_push_back_element_> { //
subcontracting
            contract_push_back_element_(): contract::nonstatic_member_function<
                    void (contract::copyable<contract_class_type>*, const T&),
                    contract_base_type::contract_push_back_element_>(
                &class_type::contract_body_push_back,
                &class_type::contract_precondition_push_back_element_,
                &class_type::contract_postcondition_push_back_element) {}
        };
    public:

        ...
   };

(For simplicity, I left out #ifdef for optional contract compilation,
introspection code to determine base class from which to subcontract,
and original type vs. noold type selection based on copyable<> type
tag.)

You can see that (1) and (2) can easily be pulled out from
CONTRACT_CLASS() as you suggested. However, pulling out (3) and (4)
from CONTRACT_FUNCTION() will require programmers to repeat the
contracted function arguments in (3) and (4), plus the original type
or noold for the relative oldof values in (4), plus the eventual
result value as an extra parameter of (4) (not present in this
example). That will be a lot of code to program and it would not be
much different than requiring to program the entire expanded code
above. BTW, the code above is part of Boost.Contract public API and
programmers can always use it if they do not want to use the macros
(but that's a lot of setup code to write...).

For consistency, I think that if (precondition) and (postcondition)
are part of CONTRACT_FUNCTION() then (invariant) should be kept in
CONTRACT_CLASS().

>>> 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?

However, why does this worry you? If programmers do not need
CONTRACT_OLDOF() then they simply do not tag the type (copyable) and
there is no overhead. Note that the (copyable) is used within the
function contract, so the object can be (and should be) tagged
(copyable) only for the member functions that use
CONTRACT_OLDOF(this).

Let me explain:
1) Yes, Boost.Contract always makes a copy whether it is needed of not
for object and arguments that are tagged (copyable).
2) Boost.Contract documentation explains that programmers should tag a
type (copyable) only when (a) the relative variable old value
CONTRACT_OLDOF(variable-name) is used in postconditions and (b) the
type has a constant correct copy constructor.
3) Boost.Contract will generate a compile-time error if
CONTRACT_OLDOF() is used on a variable not tagged (copyable) and/or
the tagged type does not have the constant-correct copy constructor.
4) Boost.Contract cannot detect if a variable tagged (copyable) is not
used in postconditions by CONTRACT_OLDOF() in which case the copy and
relative run-time overhead will be wasted.

Ideally, Boost.Contract will be able to automatically detect if
CONTRACT_OLDOF(variable-name) is used in postconditions, then tag the
related type (copyable) at compile-time, and therefore make the copy
at run-time. This is exactly why I was asking if is_macro_called() can
be implemented but it seems that it is not possible...

> 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?

This option suggested by Vicente should be feasible but it complicates
the syntax. (Eventually, I like the old variable to follow
(postcondition) as suggested here instead that being after the
function signature.)

>>> 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.

One key issue is that is that the const function will have to offer
all the original function arguments, plus local variables, etc because
everything that is in scope can be used by BLOCK_INVARIANT() (in
constant-correct context) to make the assertion:

    class x {
        void f(int a) {
            int b = a;
            CONTRACT_BLOCK_INVARIANT( a == b );
            ...
        }
        ...
    };

How do I expand this to the separate const-correct function call? Of
course programmers can manually program it:

    class x {
        void bool f_check1_(const int& a, const int& b) { return a == b; }

        void f(int a) {
            int b = a;
            CONTRACT_BLOCK_INVARIANT( f_check1_(a, b) );
            ...
        }
        ...
    };

(I tried to do this with classes declared locally within f() where
BLOCK_INVARIANT() is used but I was not able to get it to work because
you still do not see the function arguments, local variables, outer
object `this`, etc.)

Thank you very much for your comments.
Lorenzo