Skip to content

Design Contracts in C++

20081125 (2008 November 25 Tuesday)

It can be difficalt to write code that is ProvablyCorrect, or to know what code does when we wish to reuse it. It is easier if we know what services are provided by the other code, and it can be difficaly to work this out from the class/method names and comments alone.

Design Contracts consist of prerequesits and post-conditions. A prerequesits is the part of the contract that the client/caller has to honner, and the post-conditions is the part of the contract that the server/called has to honner. Therefore: If a post condition detects an error, the error is in that routine somewhere, but if a prerequasit detects an error it is the caller that is in error.

Therefore, Use Design Contracts with in your code.

Post Conditions

At the end of every method add some post-conditions, using an Ensure clause.

Ensure( condition );
Ensure( another condition );

Pre Conditions

At the begginging of every method add some pre-requasits,using a Require clause. It is better to have no pre conditions, but where you have then state them with a Require clause. It is very unsociable to use private methods in the pre condition clause. How could a client be expected to honner a contract that he can not know if he is violating.

Require( condition );
Require( another condition );


Pre and post conditions sometimes are not enough. So it you need to part way through a method use a Check. Checks are not part of the contract.

Check( condition);

Example method

SetSizeAndColour( SIZE p_Size, COLOUR p_Colour )
    Require( p_Size>=0 );
    //The code that does the work,
    //I don't care as long as the post condition is met.
    //Well nearly, it is difficalt to state all the
    //things that should not happen in a post condition.
    Ensure(m_Size EQU p_Size);
    Ensure(m_Colour EQU p_Colour);


An invarient is in two parts, the public invarient and the private invarient. Use the public invarient to state relationships about public querry functions. Use the private invarient to cut down on the number of possable states of the private data. We have no mechanisem for invarients, but here is an example of how to do it. Call the invariant at the end of every command method (non const method (we use deep const checking, the default is shallow but this is insufficent))

void inveriant() const
    //public invarient
    Check( IFF(is_Empty,Count() EQU 0 ));
    //private invarient
    Check( IMPLIES( m_is_Data1, m_is_Data2 ));
    Check( m_Data3 >= 0 );


To allow as to write expressions for the contracts that do not change things, we need to follow CommandQuerrySeporation

No comments yet

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: