
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 } ------------------------------------------------------------------------