Re: [boost] [contract] Contract Programming Library

Subject: Re: [boost] [contract] Contract Programming Library
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2010-02-09 00:02:28

Hello all,

I simplified the library syntax as shown by the example below.

I think with these changes the library matches very closely the
Contract Programming C++ standard proposal (see n1962, Crowl and
Ottosen, 2006). A notable difference is still the (unavoidable) many
extra parenthesis required by the Boost.Preprocessor signature
sequence.

Comments?

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

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

        CONTRACT_INVARIANT( ({
            CONTRACT_ASSERT( (size() == 0) == empty() );
        }) )

    public:
        void push_back(const T& element)
        CONTRACT_FUNCTION(
                (class) (copyable)(myvector) (inherit)(pushable<T>)
// Subcontracting.
                (public) (void) (push_back)( (const T&)(element) )
        (precondition) ({
            CONTRACT_ASSERT( size() < max_size() );
        })
        (postcondition) ({
            CONTRACT_ASSERT( size() == (CONTRACT_OLDOF(this)->size() +
1) );    // Old value.
        })
        (body) ({
            vector_.push_back(element);
        }) )

    private:
        std::vector<T> vector_;
    };

Major changes:

1) Removed use of self, variable.now, and variable.old in writing contracts.
Object (this) and variables are now accessed as usual in member
functions. `CONTRACT_OLDOF(variable)` is used to access old values in
postconditions (users could `#define oldof(name) CONTRACT_OLDOF(name)`
for convenience).

2) Added (precondition), (postcondition), and (body) to specify
contracts within the function signature sequence.
If no preconditions then `(precondition) ({...})` is simply omitted
from the sequence (same for postconditions, body is mandatory
instead). For non-void functions users can name the result argument
with `(postcondition) (myresult) ({...})`.

3) Added block invariants and Eiffel-like loop variants (not shown above).

4) Added static class invariants which are always checked (also at
constructors entry, destructor exit, and by static member functions --
not shown above).

Regards,
Lorenzo

On Tue, Jan 5, 2010 at 1:28 PM, vicente.botet <vicente.botet_at_[hidden]> wrote:
> ----- Original Message -----
> From: "Lorenzo Caminiti" <lorcaminiti_at_[hidden]>
> To: <boost_at_[hidden]>
> Sent: Tuesday, January 05, 2010 6:54 AM
> Subject: [boost] [contract] Contract Programming Library
>
>
>>
>> Hi all,
>>
>> I am thinking to submit a library for Contract Programming (a.k.a.
>> Design By Contract (TM) ) for C++.
>>
>> I have drafted some of the library documentation in Boost-like format:
>> http://dbcpp.sourceforge.net/boost/libs/contract/doc/html/
>>
>> Comments?
>
> Hi,
>
> I find your library very interesting and except some unavoidable preprocessor ugly (), the syntax follows quite closely the C++ proposal.
>
> Have you considered to add block invariants? Maybe you can complete the table Contract Programming Feature Comparison.
>
> If I have understood your library require the type is CopyConstructible to manage with postconditions. Have you considered to relax this constraint?
>
> I have taken the freedonm to add it to the Boost Libraries Under Construction
> https://svn.boost.org/trac/boost/wiki/LibrariesUnderConstruction . Let me know if all the informations are right.
>
> Good work,
> Vicente
>
>
> _______________________________________________
> Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
>