----- Original Message ----- From: "Yariv Tal" <yariv_tal2003@hotmail.com> To: <boost@lists.boost.org> Sent: Wednesday, February 23, 2005 9:05 AM Subject: [boost] Re: STL containers with contracts, any interest?
You may want to take a look at a small DbC library I'm working on called ensure++.
You can find it on sourceforge, at http://sourceforge.net/projects/ensure/
It allows you to write the post() part conditions at the _beginning_ of your method, near the pre conditions. Quick example: (note that I already have a plan on how to remove the need for the CONDITIONS, BODY & ENDBODY macros. Software is a constant process of improvement :) )
void push_back(const T& x) { CONDITIONS ENSURE(!post(&vector_contract::empty, this)); ENSURE(post(&vector_contract::size, this) == size() + 1); // let's ensure (some of) the strong exception guarenttee - //no change in size in case of exception EXCEPTIONAL(post(&vector_contract::size, this) == size()); BODY inherited::push_back(x); ENDBODY }
void pop_back() {
CONDITIONS REQUIRE(!empty()); ENSURE(post(&vector_contract::size, this) == size() - 1); // let's ensure (some of) the strong exception guarenttee - //no change in size in case of exception EXCEPTIONAL(post(&vector_contract::size, this) == size()); BODY inherited::pop_back(); ENDBODY }
[I'm writing this example on the fly - so don't kill me if it doesn't quite compile after you download the lib]
Hi Yariv, This appears to be very cool code. However, I am at a loss to find a good reason I would want to place post-conditions at the beginning of a code block given that the contract classes are always one-liners (e.g. inherited::fxn() ). Any comments? The EXCEPTIONAL(...) macro is a very good idea which I overlooked, and will be borrowing ;-) Concerning:
ENSURE(post(&vector_contract::size, this) == size() - 1);
If I understand this correctly, the "vector_contract::" is superflous is it not? Thanks for sharing this with us! Christopher Diggins Object Oriented Template Library (OOTL) http://www.ootl.org