Boost logo

Boost :

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


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

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

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

        void push_back(const T& element)
                (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) ({
        }) )

        std::vector<T> vector_;

Major changes:

1) Removed use of self,, 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).


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:
>> 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
> . Let me know if all the informations are right.
> Good work,
> Vicente
> _______________________________________________
> Unsubscribe & other changes:

Boost list run by bdawes at, gregod at, cpdaniel at, john at