STL containers with contracts, any interest?
I am writing a set of contract verification classes for the various STL containers. These are wrapper classes which verify DbC style contracts (i.e. preconditions, postconditions and invariants). I have already written one for std::vector you can see it at: http://www.ootl.org/pwc/ Is anyone interested in seeing this submitted Boost, if I extend it to cover the basic collections? e.g. list, map, set, multimap, multiset, deque, queue, stack? Thanks, Christopher Diggins Object Oriented Template Library (OOTL) http://www.ootl.org
Just a quick note: in the swap method you've got void swap(inherited& x) { PRE(&x != this); ... } But self-swapping is legal. Joaquín M López Muñoz Telefónica, Investigación y Desarrollo christopher diggins ha escrito:
I am writing a set of contract verification classes for the various STL containers. These are wrapper classes which verify DbC style contracts (i.e. preconditions, postconditions and invariants). I have already written one for std::vector you can see it at: http://www.ootl.org/pwc/
Is anyone interested in seeing this submitted Boost, if I extend it to cover the basic collections? e.g. list, map, set, multimap, multiset, deque, queue, stack?
Thanks,
Christopher Diggins Object Oriented Template Library (OOTL) http://www.ootl.org
_______________________________________________ Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
On Feb 23, 2005, at 2:32 AM, christopher diggins wrote:
I am writing a set of contract verification classes for the various STL containers. These are wrapper classes which verify DbC style contracts (i.e. preconditions, postconditions and invariants). I have already written one for std::vector you can see it at: http://www.ootl.org/pwc/
Is anyone interested in seeing this submitted Boost, if I extend it to cover the basic collections? e.g. list, map, set, multimap, multiset, deque, queue, stack?
Is there any advantage to this kind of markup vs. the "debug modes" that most standard libraries now have? The latest standard libraries from Metrowerks, Dinkumware, GCC, and STLport all have some form of debug mode that AFAICT actual do more checking (e.g., checking for uses of invalid iterators). Here's the reference for GCC's debug mode: http://gcc.gnu.org/onlinedocs/libstdc++/debug.html#safe Doug
Christopher Diggins Object Oriented Template Library (OOTL) http://www.ootl.org ----- Original Message ----- From: "Douglas Gregor" <doug.gregor@gmail.com> To: <boost@lists.boost.org> Sent: Wednesday, February 23, 2005 8:27 AM Subject: Re: [boost] STL containers with contracts, any interest?
On Feb 23, 2005, at 2:32 AM, christopher diggins wrote:
I am writing a set of contract verification classes for the various STL containers. These are wrapper classes which verify DbC style contracts (i.e. preconditions, postconditions and invariants). I have already written one for std::vector you can see it at: http://www.ootl.org/pwc/
Is anyone interested in seeing this submitted Boost, if I extend it to cover the basic collections? e.g. list, map, set, multimap, multiset, deque, queue, stack?
Is there any advantage to this kind of markup vs. the "debug modes" that most standard libraries now have? The latest standard libraries from Metrowerks, Dinkumware, GCC, and STLport all have some form of debug mode that AFAICT actual do more checking (e.g., checking for uses of invalid iterators). Here's the reference for GCC's debug mode: http://gcc.gnu.org/onlinedocs/libstdc++/debug.html#safe
Doug
Hi Doug, 1) The proposed PwC approach would provide consistent behaviour across STL implementations. 2) The contract verification classes would make it much easier to write new classes which model STL containers and verify that they exhibit correct behaviour. Also consider the following code: template<Vector_T> void MyAlgorithm(Vector_T& x) { // do stuff ... } If we get a hand-rolled vector type (instead of an STL vector) we have no way of knowing whether or not it conforms to the expected contract even if we can check it conforms to the correct concept. Using contract classes we could instead write (using an imaginary vector_contract_concept): template<Vector_T> void MyAlgorithm(Vector_T& x) { #ifdef DEBUG BOOST_STATIC_ASSERT(vector_contract_concept<Vector_T>::satisfied) #endif // do stuff } I am not saying that this is the best usage of the contract classes, but it is one possible way to use them. There are probably better examples, but I haven't had my coffee yet ;-) Btw thanks to Joaquín for pointing out the error in swap. Christopher Diggins http://www.ootl.org
On Feb 23, 2005, at 10:34 AM, christopher diggins wrote:
Christopher Diggins Object Oriented Template Library (OOTL) http://www.ootl.org ----- Original Message ----- From: "Douglas Gregor" <doug.gregor@gmail.com> To: <boost@lists.boost.org> Sent: Wednesday, February 23, 2005 8:27 AM Subject: Re: [boost] STL containers with contracts, any interest? Hi Doug,
1) The proposed PwC approach would provide consistent behaviour across STL implementations.
Isn't that more a property of the adaptor approach than PwC? You can pass any container to the adaptor, regardless of the underlying library, and it will perform the checks when it interfaces with that container. At least two of the debug modes I'd mentioned (GCC libstdc++ and STLport) use wrappers/adaptors to implement debug-mode semantics, and I suspect the others do as well. Nothing actually ties the debug modes to a particular library except a few #defines and/or some namespace shuffling.
2) The contract verification classes would make it much easier to write new classes which model STL containers and verify that they exhibit correct behaviour.
Sure.
Also consider the following code:
template<Vector_T> void MyAlgorithm(Vector_T& x) { // do stuff ... }
If we get a hand-rolled vector type (instead of an STL vector) we have no way of knowing whether or not it conforms to the expected contract even if we can check it conforms to the correct concept. Using contract classes we could instead write (using an imaginary vector_contract_concept):
template<Vector_T> void MyAlgorithm(Vector_T& x) { #ifdef DEBUG BOOST_STATIC_ASSERT(vector_contract_concept<Vector_T>::satisfied) #endif // do stuff }
I don't understand this part... it looks like a concept check (i.e., syntax), but above it sounds like you're saying that this verifies the contract (i.e., semantics). How can we check the semantics with a static assert? Doug
----- Original Message ----- From: "Douglas Gregor" <doug.gregor@gmail.com>
On Feb 23, 2005, at 10:34 AM, christopher diggins wrote:
<doug.gregor@gmail.com> To: <boost@lists.boost.org>
1) The proposed PwC approach would provide consistent behaviour across STL implementations.
Isn't that more a property of the adaptor approach than PwC? You can pass any container to the adaptor, regardless of the underlying library, and it will perform the checks when it interfaces with that container.
My turn to be confused. What difference does it make whether we call the approach an adapator or PwC?
template<Vector_T> void MyAlgorithm(Vector_T& x) { #ifdef DEBUG BOOST_STATIC_ASSERT(vector_contract_concept<Vector_T>::satisfied) #endif // do stuff }
I don't understand this part... it looks like a concept check (i.e., syntax), but above it sounds like you're saying that this verifies the contract (i.e., semantics). How can we check the semantics with a static assert?
We can check that the passed type is wrapped in the appropriate contract class. This is not a general solution, but it is one possible application of contracts. CD
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] It's not documented (yet) but you can see a test/sample file under the vc7.1 directory. Yariv Tal "christopher diggins" <cdiggins@videotron.ca> wrote in message news:000501c51979$cc1d32d0$d9958242@heronnest...
I am writing a set of contract verification classes for the various STL containers. These are wrapper classes which verify DbC style contracts (i.e. preconditions, postconditions and invariants). I have already written one for std::vector you can see it at: http://www.ootl.org/pwc/
Is anyone interested in seeing this submitted Boost, if I extend it to cover the basic collections? e.g. list, map, set, multimap, multiset, deque, queue, stack?
Thanks,
Christopher Diggins Object Oriented Template Library (OOTL) http://www.ootl.org
_______________________________________________ Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
----- 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
----- 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
"christopher diggins" <cdiggins@videotron.ca> wrote in message news:004b01c519c0$f3b185c0$d9958242@heronnest... 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?
True. For one liners you are probably right. However, if you want to allow conditionally removing the contract code (i.e. for release code) you are still left with the definitions and code of taking the "old_value" in some of your checks, i.e.: void push_back(const T& x) { size_t old_size = size(); // in release version this is unwanted code... inherited::push_back(x); POST(!empty()); POST(size() == old_size + 1); } The solution I propose never actually defines named temp variables, so all of the contracts code can be removed in release code (of course, your approach is to change the vector typedef so you also have no problem, but in general this could be a problem). Theoretically an optimizer should be able to remove the code that stores the old value - if you it can see the code of the methods called for getting that value in the first place (to ensure there are no side effects) and assuming it is allowed to remove named temporary variables (I think the standard says it isn't...)
The EXCEPTIONAL(...) macro is a very good idea which I overlooked, and will be borrowing ;-)
enjoy. I would love it if you add a comment referencing the ensure++ lib for this, but it's up to you (in other words: I don't claim to have any special rights on the idea).
Concerning:
ENSURE(post(&vector_contract::size, this) == size() - 1);
If I understand this correctly, the "vector_contract::" is superflous is it not?
I'm not sure. Maybe this is something I am carrying from MSVC6, maybe vc7.1 requires it, maybe the standard requires it or maybe it was never needed. Anyone out there knows the answer?
Thanks for sharing this with us!
Christopher Diggins Object Oriented Template Library (OOTL) http://www.ootl.org
_______________________________________________ Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
From: "Yariv Tal" <yariv_tal2003@hotmail.com>
"christopher diggins" <cdiggins@videotron.ca> wrote in message news:004b01c519c0$f3b185c0$d9958242@heronnest...
From: "Yariv Tal" <yariv_tal2003@hotmail.com>
Concerning:
ENSURE(post(&vector_contract::size, this) == size() - 1);
If I understand this correctly, the "vector_contract::" is superflous is it not?
I'm not sure. Maybe this is something I am carrying from MSVC6, maybe vc7.1 requires it, maybe the standard requires it or maybe it was never needed. Anyone out there knows the answer?
The only conforming way to take the address of a class member is &class_name::member_name (5.3.1/3). -- Rob Stewart stewart@sig.com Software Engineer http://www.sig.com Susquehanna International Group, LLP using std::disclaimer;
participants (5)
-
christopher diggins -
Douglas Gregor -
Joaquín Mª López Muñoz -
Rob Stewart -
Yariv Tal