Click here to Skip to main content
Click here to Skip to main content

Design by Contract Framework for C++

, 19 Jun 2002
Rate this:
Please Sign up or sign in to vote.
An implementation of Design by Contract in C++
<!-- Add the rest of your HTML here -->

Introduction

These classes and supporting macros provide a Design by Contract framework for use in C++ projects. It has been tested in Visual C++ 6 and 7 but should work with minor modifications under any Standard C++-conforming compiler. For example, it uses the _ASSERTE macro defined in <crtdbg.h> for Visual C++. This may be defined elsewhere for another compiler.

Design by Contract is a method made famous by Bertrand Meyer in the Eiffel programming language where support is built right into the language constructs.

See Chapter 11 of Object-Oriented Software Construction - 2nd Edition (Prentice Hall, 1997) by Bertrand Meyer and http://www.eiffel.com/doc/manuals/technology/contract/

The basic idea is that a class can be viewed as having a contract with its clients whereby the class guarantees to provide certain results (postconditions of its methods) provided that the clients agree to satisfy certain requirements (preconditions of the class's methods). For example, consider a routine:

string FindCustomer(int customerID) 

The precondition might be that customerID is positive. The postcondition might be that we guarantee to find the customer, e.g., possibly among other things, that the return value is a non-empty string.

A failure of the precondition indicates a bug in the caller, the client. A failure of the postcondition indicates a bug in the routine, the supplier. These conditions, or specifications, are implemented by assertion statements. In C/C++ code the assert macro is used for these purposes. These generate an "abort, ignore, retry" message box on assertion failure. An alternative approach is to use exception-handling. The framework that I describe below allows you to use either by defining or not defining a conditional compilation constant.

We cannot be as comprehensive in C++ as in Eiffel but we can go some of the way. The following framework provides exception classes to represent preconditions, postconditions, class invariants and general assertions. To simplify usage I have supplied macros to generate the appropriate exceptions on contract failure. Alternatively, a conditional compilation flag can be set to use the C assert macro instead of throwing an exception. When debugging, sometimes, you want to be able to ignore assertions and continue stepping through code, especially when routines are still in a state of flux. For example, an assertion may no longer be valid but you still want to have the assertion flagged to remind you that you've got to fix the code (remove the assertion or replace it with another).

The framework attempts to provide the utmost flexibility.

For each project that includes the Design by Contract framework you can:

  1. Generate debug assertions instead of exceptions.
  2. Separately enable or disable precondition, postcondition, invariant and assertion checks. However, the framework, as shipped, has defined a logical scheme based on an argument in Meyer's book.
  3. Disable precondition, postcondition, invariant or assertion checks on a class-by-class or method-by-method basis.
  4. Supply a description for each assertion or not. If you do not the framework will tell you what type of error - precondition, postcondition, etc. - you have generated.
  5. Define different rules for Debug and Release builds. The framework, as shipped, allows you the option of enabling or disabling only preconditions in Release builds but this can be amended if desired by editing the header file.

Contracts and Inheritance

There are certain rules that should be adhered to when Design by Contract is used with inheritance. Eiffel has language support to enforce these but in C++ we must rely on the programmer. The rules are, in a derived class (Meyer Chapter 16):

  1. An overriding method may [only] weaken the precondition. This means that the overriding precondition should be logically "or-ed" with the overridden precondition.
  2. An overriding method may [only] strengthen the postcondition. This means that the overriding postcondition should be logically "and-ed" with the overridden postcondition.
  3. A derived class invariant should be logically "and-ed" with its base class invariant.

Example (using pseudo-C++ syntax)

class D : public B
virtual int B::foo(int x)
{
  REQUIRE(1 < x < 3);
  ...
  ENSURE(result < 15);
  return result;
}
virtual int D::foo(int x)
{
  REQUIRE(1 < x < 3 or 0 < x < 5); // weakened precondition
  ...
  ENSURE(result < 15 and result < 3); // strengthened postcondition
  return result;
}

Eiffel has code constructs to support the above. In D::foo() we would write:

require else 0 < x < 5

meaning check base class precondition first and if it fails check the derived class version.

ensure then result < 3

meaning check base class postcondition and the derived class postcondition and ensure they both pass.

For C++ we need only write:

REQUIRE(0 < x < 5 )
ENSURE(result < 3)

making sure that the precondition is always equal to or weaker than the base version and the postcondition is always equal to or stronger than the base version.

For invariants, in B we might have

INVARIANT(B::a > 0 and B::b > 0);

and in D

INVARIANT(D::c > 0 and D::d > 0);

The rule says we should combine these in D

INVARIANT(B::a > 0 and B::b > 0 and D::c > 0 and D::d > 0);

or

INVARIANT(B::a > 0 and B::b > 0);
INVARIANT(D::c > 0 and D::d > 0);

Conditional Compilation Constants

Global settings

DESIGN_BY_CONTRACT - Enable Design by Contract checks
USE_ASSERTIONS - Use ASSERT macros instead of exceptions

For enabling and disabling each type of contract

These suggestions are based on Meyer p393.

CHECK_ALL - Check assertions - implies checking preconditions, postconditions and invariants
CHECK_INVARIANT - Check invariants - implies checking preconditions and postconditions
CHECK_POSTCONDITION - Check postconditions - implies checking preconditions
CHECK_PRECONDITION - Check preconditions only, e.g., in Release build

So to enable all checks and use exception handling then, in a header file, write:

#define DESIGN_BY_CONTRACT
#define CHECK_ALL

or define them as preprocessor settings.

In your implementation file write:

#include "mydefines.h"
#include "DesignByContract.h"
using namespace DesignByContract;

Example

The following code will execute in Visual C++ 6 or 7. It has been set up to use assertion macros rather than exceptions so that by clicking "Ignore" in the error dialog box you can step through all the assertion failures to see some of the different message display options at work. All of the assertions will execute because CHECK_ALL has been defined.

The framework classes are defined in the header file, DesignByContract.h which can be found in the source download.

// DesignByContract.cpp : Defines the entry point for the console application.
//

#include <span class="code-string">"stdafx.h"
</span>
#include <span class="code-string">"dbcdefs.h"
</span>
#include <span class="code-string">"DesignByContract.h"
</span>
#include <span class="code-keyword"><iostream>
</span>
#include <span class="code-keyword"><string>
</span>

using namespace std;

// Example debugging flags - can make this as fine-grained as we want

#ifdef _DEBUG
    static const bool NOT_CHECK_FOO = false; // we are debugging: enable 
                                             // DBC check for foo()
#else
    static const bool NOT_CHECK_FOO = true; // we are not debugging: 
                                            //disable DBC check for foo()
#endif

using namespace DesignByContract;

int foo(const char* customerName) // throw(AssertionException)
{
    // Precondition check on function arguments 
    // but only if foo() is being monitored
    REQUIRE(NOT_CHECK_FOO || customerName != NULL, "Must specify a customer");

    int val = 3;

    // General assertion check 
    // Override our monitoring flag for foo() to always check this 
    // (No description supplied)
    CHECK0(val < 3); 

    // Invariant check (contrived)
    // (No description supplied)
    INVARIANT0(customerName != NULL && val > 0);

    // Postcondition check on function return value
    // but only if foo() is being monitored
    ENSURE(NOT_CHECK_FOO || val == 2, "Value must be 2");

    return val;
}


int main(int argc, char* argv[])
{
    try
    {
        const char* customerName = 0;
        int val = foo(customerName);
    }
    catch(const DesignByContractException & e)
    {
        cout << e; // Note: "<<" is overloaded to produce meaningful output
    }

    return 0;
}

The header file dbcdefs.h looks like this:

#ifndef __DBCDEFS_H__
#define __DBCDEFS_H__

// Note: If this file is included as-is your client code will execute with
// DESIGN_BY_CONTRACT, USE_ASSERTIONS and CHECK_ALL defined.

// If, say, you want to use exception-handling and precondition checking only
// then comment out the #defines USE_ASSERTIONS, CHECK_ALL, CHECK_INVARIANT 
// and CHECK_POSTCONDITION

// If you want postconditions and preconditions
// then comment out the #defines USE_ASSERTIONS, CHECK_ALL, CHECK_INVARIANT

// and so on.

// In a production environment you might wish to define these in preprocessor 
// settings rather than use this file.

#define DESIGN_BY_CONTRACT // Enable Design by Contract checks
#define USE_ASSERTIONS     // Use ASSERT macros instead of exceptions

#define CHECK_ALL           // Check assertions - implies checking preconditions, 
                            // postconditions and invariants
#define CHECK_INVARIANT     // Check invariants - implies checking preconditions 
                            // and postconditions
#define CHECK_POSTCONDITION // Check postconditions - implies checking 
                            // preconditions 
#define CHECK_PRECONDITION  // Check preconditions only, e.g., in Release build

#endif //__DBCDEFS_H__

Running this example and clicking "Ignore" to step through the assertions produces the following output.

Assertion Failure Image

Assertion Failure Image

Assertion Failure Image

Assertion Failure Image

History

20 June 2002 - updated downloads

License

This article has no explicit license attached to it but may contain usage terms in the article text or the download files themselves. If in doubt please contact the author via the discussion board below.

A list of licenses authors might use can be found here

Share

About the Author

Kevin McFarlane
Web Developer
United Kingdom United Kingdom
No Biography provided

Comments and Discussions

 
GeneralMinor Correction PinmemberKevin McFarlane17-Jun-03 6:07 
GeneralWhat's Changed PinmemberKevin McFarlane28-Jun-02 0:29 
QuestionContracts for Speed & Memory Consumption? PinmemberAnonymous3-Mar-02 17:26 
AnswerRe: Contracts for Speed & Memory Consumption? PinmemberAnonymous21-Jun-02 13:45 

General General    News News    Suggestion Suggestion    Question Question    Bug Bug    Answer Answer    Joke Joke    Rant Rant    Admin Admin   

Use Ctrl+Left/Right to switch messages, Ctrl+Up/Down to switch threads, Ctrl+Shift+Left/Right to switch pages.

| Advertise | Privacy | Mobile
Web04 | 2.8.140821.2 | Last Updated 20 Jun 2002
Article Copyright 2002 by Kevin McFarlane
Everything else Copyright © CodeProject, 1999-2014
Terms of Service
Layout: fixed | fluid