[boost] Proposal: Design by Contract / Pre & Postconditions library

From: Yariv Tal (yariv_tal2003_at_[hidden])
Date: 2005-04-17 08:56:05

Is there a need for a Design by Contract (a.k.a Pre & Post conditions)
library?

I've written a library that allows for pre & post conditions and adds an
additional "exceptional" condition type.
Each condition is tested at a different point in the methods invocation,
and an assert occurs if the condition does not hold.

Unlike many other such libraries it allows for defining all condition
types at the begining of the method, instead of making you define the
"post" checks just before method exit (which usually constrains you
to a single-point-of-method-exit design).

See EXAMPLES below.

Here's a quick summary of condition types:

- Pre conditions - tested immidiately

- Post conditions - tested on exiting the method normally (not due to
     an exception). You can use both "pre"(=old) values and "post"
     (=current) values in the test expression (i.e.
     "pre(size) < post(size)").
     If the method returns a value then you can also, with some work on
     your part, test against it (i.e. "retval > 0").

- Exceptional conditions - tested on exiting the method due to an
     exception. You can use both "pre" and "post" values in the test
     expression.

- Delayed Assert - this is just a small add-on that allows you to
     seperate between an assert's definition time and testing time.
     It's useful when an assert needs to compare some new value to an
     "old" value (usually solved by saving the old value in a temp
     variable, which I find messy).

Again, see EXAMPLES below.

I've been using it with the current project at my work place and found
it to be very useful.

The implementation uses scope guards to execute user defined predicate
functors at the correct points in the method's life cycle.
The predicate functors can be explicitly defined or defined on the fly
(boost.lambda is my favourite tool for this).
When a scope guard is destroyed I check to see if an exception occured
(I found 2 ways to do this, see below) and according to the condition
type the predicate is executed, causing an assertion failure if it
returns false.

The pre/post conditions can be written in either an Eifel like way
(require/ensure within a conditions-body-endbody block) or simply
via pre/post condition macros (require that you compiler support the
uncaught_exception function).

Any comments and questions are, of course, welcome.
Yariv Tal.

P.S. Here are the EXAMPLES:

==[Eifel like require & ensure]=========================================

// Defining a contract for a stack's class "push" method
// using Eifle style (within conditions-body-endbody block)
void Stack::push(const T &a_item)
{
  CONDITIONS
    // Conditions that must hold when entering the method
    REQUIRE(m_buf != NULL);
    REQUIRE(m_used <= m_size);
    REQUIRE(m_size > 0);

    // Conditions that must hold when exiting the method
    // Note that I do not assume a single exit point
    ENSURE(post(m_used) <= post(m_size));
    ENSURE(post(m_size) >= m_size);
    ENSURE(post(m_used) > m_used);

    // Conditions that must hold if an exception occurs
    EXCEPTIONAL(post(m_used) == m_used);
    EXCEPTIONAL(post(m_buf) == m_buf);
    EXCEPTIONAL(post(m_size) == m_size);
  BODY
    if(m_used == m_size)  // grow if necessary
    {
      unsigned int newSize = (m_size+1)*2; // grow factor
      T* newBuf = NewCopy( m_buf, m_size, newSize);

      delete[] m_buf;  // again, this can't throw
      m_buf = newBuf;
      m_size = newSize;
    }

    m_buf[m_used] = a_item; // if this copy throws, the increment
    ++m_used;         //  isn't done and the state is unchanged
  ENDBODY
}

------------------------------------------------------------------------

==[Pre/Post style]======================================================

// Defining a contract for a stack's class "push" method
// using pre/post style (requires that compiler support
// the uncaught_exception function)
void Stack::push(const T &a_item)
{
  // Conditions that must hold when entering the method
  PRECOND(m_buf != NULL);
  PRECOND(m_used <= m_size);
  PRECOND(m_size > 0);

  // Conditions that must hold when exiting the method
  // Note that I do not assume a single exit point
  POSTCOND(post(m_used) <= post(m_size));
  POSTCOND(post(m_size) >= m_size);
  POSTCOND(post(m_used) > m_used);

  // Conditions that must hold if an exception occurs
  EXCEPTCOND(post(m_used) == m_used);
  EXCEPTCOND(post(m_buf) == m_buf);
  EXCEPTCOND(post(m_size) == m_size);

  if(m_used == m_size)  // grow if necessary
  {
    unsigned int newSize = (m_size+1)*2; // grow factor
    T* newBuf = NewCopy( m_buf, m_size, newSize);

    delete[] m_buf;  // again, this can't throw
    m_buf = newBuf;
    m_size = newSize;
  }

  m_buf[m_used] = a_item; // if this copy throws, the increment
  ++m_used;           //  isn't done and the state is unchanged
}

------------------------------------------------------------------------

==[Using a Delayed Assert]==============================================

void Stack::push(const T &a_item)
{
  // ... conditions are defined here, as in previous examples

  if(m_used == m_size)  // grow if necessary
  {
    // =[Define a Delayed Assert]====
    // Use the "assertdef" macro to define a delayed assert.
    // This assert will be evaluated at a later time, when we use the
    // "assertnow" macro, and will check that the buffer, m_buf,
    // has changed. Note that we must give the assertion a name.
    assertdef(GrowChangesBufferToNewBuffer, post(m_buf) != m_buf);

    unsigned int newSize = (m_size+1)*2; // grow factor
    T* newBuf = NewCopy( m_buf, m_size, newSize);

    delete[] m_buf;  // again, this can't throw
    m_buf = newBuf;
    m_size = newSize;

    // =[Test the Delayed Assert]====
    // Assert the previously defined "delayed assert".
    assertnow(GrowChangesBufferToNewBuffer);
  }

  m_buf[m_used] = a_item; // if this copy throws, the increment
  ++m_used;           //  isn't done and the state is unchanged
}

------------------------------------------------------------------------