Proposal: Design by Contract / Pre & Postconditions library

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

On 04/17/2005 08:56 AM, Yariv Tal wrote:
Is there a need for a Design by Contract (a.k.a Pre & Post conditions) library? Sure!
[snip]
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).
Sounds great to me.

Yariv Tal <yariv_tal2003 <at> hotmail.com> writes:
Is there a need for a Design by Contract (a.k.a Pre & Post conditions) library?
I tried to write something like this a while ago: http://www.codeproject. com/cpp/DesignByContract.asp . How much impact do your macros have on compile times? I found that the lambda expressions used to implement postconditions really took a toll on compile times with Visual C++ 7.1, and on other compilers, gcc for instance, its probably even worse. Since these macros are part of the function implementation, maybe one shouldn't borrow the name "Design By Contract", since that implies a contract external to the function. Proper DbC contracts need to be stated at the level of function declarations, and would apply to overrides in derived classes as well. Trying to simulate DbC through macros is a battle waiting to be lost, I think. I'd be more interested in a good POSTCONDITION macro, that works like an assertion, except that it kicks in when leaving the surrounding scope. Then people can do whatever they want with it, including rudimentary "DbC". My $0.02. /Jarl.

Hi Jarl, "Jarl Lindrud" <jlindrud@hotmail.com> wrote in message news:loom.20050417T153708-646@post.gmane.org...
Yariv Tal <yariv_tal2003 <at> hotmail.com> writes:
Is there a need for a Design by Contract (a.k.a Pre & Post conditions) library?
I tried to write something like this a while ago: http://www.codeproject. com/cpp/DesignByContract.asp .
I took a look and really liked the syntax and the error messages. I think that storing the values of used variables in order to show them in the condition failure message is a great idea. Do you check at compile time that the used gave all of the variables participating in the expression or do you just let the user state which variables they want to be displayed in the error message? One thing though, I didn't see any handling of disabling testing post conditions when an exception is thrown. Did I miss something?
How much impact do your macros have on compile times? I found that the
expressions used to implement postconditions really took a toll on compile times with Visual C++ 7.1, and on other compilers, gcc for instance, its
lambda probably even
worse. The compile impact isn't small. Probably similar to the one you encountered, although braely use any lambda code in the implementation, so it's as heavy as the user makes it (they can always choose to write an explicit functor or use the std functor manipulators, I guess...)
Since these macros are part of the function implementation, maybe one
shouldn't
borrow the name "Design By Contract", since that implies a contract external to the function. Proper DbC contracts need to be stated at the level of function declarations, and would apply to overrides in derived classes as well. Point taken. Originally I was hoping to add invariants etc., but I didn't get to it. Of course, even with invariants it will still be more at the function level. In general, I think there's a lot to do (temporal invariants as in "keystone ", for example) and since it is so useful (a fact I discover every time a condition in my code is invalidated) it think, IMHO, it should be a library for all to use and for many to contribute to.
Trying to simulate DbC through macros is a battle waiting to be lost, I
think. You are right, but I find even a limited implementation is powerful enough to be useful.
I'd be more interested in a good POSTCONDITION macro, that works like an assertion, except that it kicks in when leaving the surrounding scope. Then people can do whatever they want with it, including rudimentary "DbC". Its in there. Take a look at the second example. (only problem is that it requires the compiler to support uncaught_exception).
My $0.02.
Glad to have read them.
/Jarl.
Yariv.

At Sunday 2005-04-17 09:07, you wrote:
Hi Jarl,
"Jarl Lindrud" <jlindrud@hotmail.com> wrote in message news:loom.20050417T153708-646@post.gmane.org...
Yariv Tal <yariv_tal2003 <at> hotmail.com> writes:
Is there a need for a Design by Contract (a.k.a Pre & Post conditions) library?
I tried to write something like this a while ago: http://www.codeproject. com/cpp/DesignByContract.asp .
I took a look and really liked the syntax and the error messages. I think that storing the values of used variables in order to show them in the condition failure message is a great idea. Do you check at compile time that the used gave all of the variables participating in the expression or do you just let the user state which variables they want to be displayed in the error message?
One thing though, I didn't see any handling of disabling testing post conditions when an exception is thrown. Did I miss something?
I assumed (dangerous, I know) that NO post conditions would be tested on exception but those explicitly done in the exception stuff. (maybe they all will be if NO exception conditions are mentioned? like a default constructor being built by the compiler).
How much impact do your macros have on compile times? I found that the
expressions used to implement postconditions really took a toll on compile times with Visual C++ 7.1, and on other compilers, gcc for instance, its
lambda probably even
worse. The compile impact isn't small. Probably similar to the one you encountered, although braely use any lambda code in the implementation, so it's as heavy as the user makes it (they can always choose to write an explicit functor or use the std functor manipulators, I guess...)
Since these macros are part of the function implementation, maybe one
shouldn't
borrow the name "Design By Contract", since that implies a contract external to the function. Proper DbC contracts need to be stated at the level of function declarations, and would apply to overrides in derived classes as well. Point taken. Originally I was hoping to add invariants etc., but I didn't get to it. Of course, even with invariants it will still be more at the function level. In general, I think there's a lot to do (temporal invariants as in "keystone ", for example) and since it is so useful (a fact I discover every time a condition in my code is invalidated) it think, IMHO, it should be a library for all to use and for many to contribute to.
Trying to simulate DbC through macros is a battle waiting to be lost, I
think. You are right, but I find even a limited implementation is powerful enough to be useful.
I'd be more interested in a good POSTCONDITION macro, that works like an assertion, except that it kicks in when leaving the surrounding scope. Then people can do whatever they want with it, including rudimentary "DbC". Its in there. Take a look at the second example. (only problem is that it requires the compiler to support uncaught_exception).
My $0.02.
Glad to have read them.
/Jarl.
Yariv.
_______________________________________________ Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Victor A. Wagner Jr. http://rudbek.com The five most dangerous words in the English language: "There oughta be a law"

Hi Victor, as you wrote: [snip] "Victor A. Wagner Jr." <vawjr@rudbek.com> wrote in message news:6.2.0.14.2.20050417092516.08342e98@mail.rudbek.com...
I assumed (dangerous, I know) that NO post conditions would be tested on exception but those explicitly done in the exception stuff. (maybe they
all
will be if NO exception conditions are mentioned? like a default constructor being built by the compiler).
You are right. If an exception occurs NO post conditions are tested. If you want a condition to be tested when an exception is thrown, define an EXCEPTIONAL condition (I find this useful for testing that the object was not changed = the strong exception guarentee). By the way, I use the EXCEPtTIONAL condition as a technique to ensure that no exception is thrown (this can be useful if a method's interface allows throwing but you are sure that your current implementation does not throw): EXCEPTIONAL(lambda::constant(false)); // this will always fail if an exception is thrown Hope that clarifies things for you. Yariv.

Yariv Tal <yariv_tal2003 <at> hotmail.com> writes:
Do you check at compile time that the used gave all of the variables participating in the expression or do you just let the user state which variables they want to be displayed in the error message?
The user just states which variables he'd like to see printed, if the condition were to fail, and its fine not to specify any variables at all.
One thing though, I didn't see any handling of disabling testing post conditions when an exception is thrown. Did I miss something?
No you didn't... guilty as charged :)
Since these macros are part of the function implementation, maybe one
shouldn't
borrow the name "Design By Contract", since that implies a contract external to the function. Proper DbC contracts need to be stated at the level of function declarations, and would apply to overrides in derived classes as well. Point taken. Originally I was hoping to add invariants etc., but I didn't get to it. Of course, even with invariants it will still be more at the function level. In general, I think there's a lot to do (temporal invariants as in "keystone ", for example) and since it is so useful (a fact I discover every time a condition in my code is invalidated) it think, IMHO, it should be a library for all to use and for many to contribute to.
Agreed. Formalizing the PRECONDITION and POSTCONDITION macros would be quite useful, I think. But I wouldn't be too worried about trying to emulate DbC, that's a different concept altogether. /Jarl.
participants (4)
-
Jarl Lindrud
-
Larry Evans
-
Victor A. Wagner Jr.
-
Yariv Tal