Re: [boost] [contract] Mixin Boost.Contract and Boost.STM

Subject: Re: [boost] [contract] Mixin Boost.Contract and Boost.STM
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2010-04-02 15:52:36

Hi,

On Sat, Mar 20, 2010 at 10:34 AM, Lorenzo Caminiti
<lorcaminiti_at_[hidden]> wrote:
> On Tue, Mar 16, 2010 at 6:54 PM, vicente.botet <vicente.botet_at_[hidden]> wrote:
>> I was wondering if instead of repeating the fuction signature and the class 'signature'
>> you could be able to provide a macro CONTRACT_FUNCTION2 that allows to just write
>> #define CONTRACT_CLASS (class) (myvector) (inherit)(pushable<T>)
>>    CONTRACT_FUNCTION2(
>>            ((public) (void) (push_back)( (const T&)(element) ))
>
> I have experimented with this a similar idea in the past. However, I
> concluded that copyable class type and inheritance both need to be
> specified at the function-contract level (not at the class-contract
> level) because:

I was able to implement the CONTRACT_CLASS() macro with an interface
similar to what Vicente suggested.

I think this was an important improvement because:
1) Programmers no longer need to repeat the class and base classes
types within CONTRACT_FUNCTION()  for every function. The class and
base classes types are only specified once within CONTRACT_CLASS().
2) Perhaps more importantly, now the library is able to
_automatically_ inspect the base classes to see if a specific function
should subcontract or not. This way programmers of derived classes can
no longer "cheat" avoiding to subcontract by omitting (inherit) in
CONTRACT_FUNCTION() -- in fact, (inherit) is gone all together from
the library API.

The myvector example of the documentation
http://dbcpp.sourceforge.net/index.html#contract__.introduction.an_example
now becomes:

#include "pushable.hpp"
#include <contract.hpp>
#include <vector>

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

    CONTRACT_CLASS( (myvector) (pushable<T>) /***** Class and base
classes specified here and only once *****/
    (invariant) ({ // For static class invariants use `(static)
(invariant) ({ ... })`.
        CONTRACT_ASSERT( (size() == 0) == empty() );
    }) )

public:
    void push_back(const T& element)
    CONTRACT_FUNCTION( /***** No class and no (inherit) here anymore *****/
            (public) (void) (push_back)( (const T&)(element) )
(copyable) /***** Copyable qualifier for the object is moved at the
end of the function signature (same as cv-qualifier) *****/
    (precondition)({
        CONTRACT_ASSERT( size() < max_size() );
    })
    (postcondition)({
        CONTRACT_ASSERT( size() == (CONTRACT_OLDOF(this)->size() + 1) );
    })
    (body)({
        vector_.push_back(element);
    }) )

    typedef typename std::vector<T>::size_type size_type;
    size_type size(void) const { return vector_.size(); }
    size_type max_size(void) const { return vector_.max_size(); }
    bool empty(void) const { return vector_.empty(); }
    const T& back(void) const { return vector_.back(); }
private:
    std::vector<T> vector_;
};

Note that the (copyable) object qualifier is still specified at
function scope because for the same class a function might need
CONTRACT_OLDOF(this) in its postconditions while another might not. I
have decided to specify the (copyable) object qualifier at the end of
the function signature so to follow a similar syntax as for the
cv-qualifier "(const)/(volatile)/(copyable) at the end of a member
function signature qualify the object as const/volatile/copyable
within that member function".

>From an implementation prospective:
1) CONTRACT_CLASS() defines typedefs for the class and base classes
types with predefined names so that CONTRACT_FUNCTION() knows how to
access them.
2) CONTRACT_FUNCTION() expands to code that uses uses SFINAE to
inspect the base class types looking for the struct which defines the
function contract (see  the "[has_function]" email thread).
3) The function contract struct has a unique name for a given function
within a class plus it differentiates if a base function is virtual or
not.
This way the library can automatically subcontract x::f() from the
contract of y::f() only if y is a base of x, and y is virtual, and
y::f() has a contract.

Thanks a lot for the suggestion.
Lorenzo