[contract] Strong exception safety guarantees
Hello all, I've been considering adding a .except(...) construct to Boost.Contract that will allow to specify conditions to check at function exit but when the function body throws (in contrast to postconditions that are checked at function exit but only when the function body does not throw). I think .except(...) could be used to assert strong exception safety guarantees... (note that class invariants are already checked at exit of public functions and also when the public function bodies throw, but invariants are suited to assert only basic, and not strong, exception safety guarantees). That might help addressing a point made in P0147R0 under the "Contracts and Exceptions" section: ``Some operations make stronger exception safety claims. In particular, they claim that an exception thrown from a member function will leave the state of an object unchanged from its state on function entry. If we invalidate postconditions on exceptions, we appear to have no mechanism to describe strong exception safety.'' For example, the following swap ensures to leave its arguments unchanged when it throws: void swap(std::string& a, std::string& b) { boost::contract::old_ptr<std::string> old_a = BOOST_CONTRACT_OLDOF(a); boost::contract::old_ptr<std::string> old_b = BOOST_CONTRACT_OLDOF(b); boost::contract::guard c = boost::contract::function() .postcondition([&] { // Checked at function exit but only if body does not throw. BOOST_CONTRACT_ASSERT(a == *old_b); BOOST_CONTRACT_ASSERT(b == *old_a); }) .except([&] { // Checked if body throws (strong exception safety guarantees). BOOST_CONTRACT_ASSERT(a == *old_a); BOOST_CONTRACT_ASSERT(b == *old_b); }) ; ... // Body implementation (which might throw). } Would this be beneficial? Thanks, --Lorenzo
2016-07-15 6:04 GMT+02:00 Lorenzo Caminiti <lorcaminiti@gmail.com>:
Hello all,
I've been considering adding a .except(...) construct to Boost.Contract that will allow to specify conditions to check at function exit but when the function body throws (in contrast to postconditions that are checked at function exit but only when the function body does not throw).
I think .except(...) could be used to assert strong exception safety guarantees... (note that class invariants are already checked at exit of public functions and also when the public function bodies throw, but invariants are suited to assert only basic, and not strong, exception safety guarantees).
How would you express the strong guarantee on std::vector::push_back? Regards, &rzej;
On Fri, Jul 15, 2016 at 12:35 AM, Andrzej Krzemienski <akrzemi1@gmail.com> wrote:
2016-07-15 6:04 GMT+02:00 Lorenzo Caminiti <lorcaminiti@gmail.com>:
I've been considering adding a .except(...) construct to Boost.Contract that will allow to specify conditions to check at function exit but when the function body throws (in contrast to postconditions that are checked at function exit but only when the function body does not throw).
I think .except(...) could be used to assert strong exception safety guarantees... (note that class invariants are already checked at exit of public functions and also when the public function bodies throw, but invariants are suited to assert only basic, and not strong, exception safety guarantees).
How would you express the strong guarantee on std::vector::push_back?
vector::push_back exception safety: ``If no reallocations happen, there are no changes in the container in case of exception (strong guarantee). If a reallocation happens, the strong guarantee is also given if the type of the elements is either copyable or no-throw moveable. Otherwise, the container is guaranteed to end in a valid state (basic guarantee). If allocator_traits::construct is not supported with val as argument, it causes undefined behavior.'' http://www.cplusplus.com/reference/vector/vector/push_back/ Hmm... so assuming the allocator API can be augmented with an allocations() const query that returns the number of allocations done so far, and that operator== can be used to check if the vector has not changed, maybe something like this: template<typename T> void vector<T>::push_back(T const& value) { boost::contract::old_ptr<vector<T> > old_me = BOOST_CONTRACT_OLDOF(*this); boost::contract::old_ptr<unsigned> old_allocations = BOOST_CONTRACT_OLDOF(get_allocator().allocations()); boost::contract::guard c = boost::contract::public_function(this) ... // Preconditions and postconditions. .except([&] { if( get_allocator().allocations() == *old_allocations || is_copyable<T>::value || is_nothrow_movable<T>::value ) BOOST_CONTRACT_ASSERT(*this == *old_me); // Otherwise, just basic guarantees as asserted by the class invariants. }) ; ... // Body implementation. } I'm not 100% sure... what do you think? Thanks, --Lorenzo P.S. A part from this example, for sure there will be specifications that cannot be programmed with contracts (e.g., inability to express programmatically "iterator range is valid, or invalid" and something like properties would help here...). But this is an old limitation of Contract Programming, it was already discussed by Bertrand Meyer in Object Oriented Software Construction for Eiffel in the 1990s. Nevertheless, contracts are still useful for those specifications that can be expressed programmatically, even if not all specifications can. So I'd expect the same to be true if using contracts to program (both strong with .except(...) and basic with invariants) exceptions safety guarantees.
2016-07-15 19:22 GMT+02:00 Lorenzo Caminiti <lorcaminiti@gmail.com>:
On Fri, Jul 15, 2016 at 12:35 AM, Andrzej Krzemienski <akrzemi1@gmail.com> wrote:
2016-07-15 6:04 GMT+02:00 Lorenzo Caminiti <lorcaminiti@gmail.com>:
I've been considering adding a .except(...) construct to Boost.Contract that will allow to specify conditions to check at function exit but when the function body throws (in contrast to postconditions that are checked at function exit but only when the function body does not throw).
I think .except(...) could be used to assert strong exception safety guarantees... (note that class invariants are already checked at exit of public functions and also when the public function bodies throw, but invariants are suited to assert only basic, and not strong, exception safety guarantees).
How would you express the strong guarantee on std::vector::push_back?
vector::push_back exception safety:
``If no reallocations happen, there are no changes in the container in case of exception (strong guarantee). If a reallocation happens, the strong guarantee is also given if the type of the elements is either copyable or no-throw moveable. Otherwise, the container is guaranteed to end in a valid state (basic guarantee). If allocator_traits::construct is not supported with val as argument, it causes undefined behavior.''
http://www.cplusplus.com/reference/vector/vector/push_back/
Hmm... so assuming the allocator API can be augmented with an allocations() const query that returns the number of allocations done so far, and that operator== can be used to check if the vector has not changed, maybe something like this:
template<typename T> void vector<T>::push_back(T const& value) { boost::contract::old_ptr<vector<T> > old_me = BOOST_CONTRACT_OLDOF(*this); boost::contract::old_ptr<unsigned> old_allocations = BOOST_CONTRACT_OLDOF(get_allocator().allocations()); boost::contract::guard c = boost::contract::public_function(this) ... // Preconditions and postconditions. .except([&] { if( get_allocator().allocations() == *old_allocations || is_copyable<T>::value || is_nothrow_movable<T>::value ) BOOST_CONTRACT_ASSERT(*this == *old_me); // Otherwise, just basic guarantees as asserted by the class invariants. }) ;
... // Body implementation. }
I'm not 100% sure... what do you think?
It bothers me that I have to copy the entire vector upon each push_back. Because OLDOF stuff must do a copy, right? I do not think I could afford that; even in debug builds. Regards, &rzej;
2016-07-15 19:37 GMT+02:00 Andrzej Krzemienski <akrzemi1@gmail.com>:
2016-07-15 19:22 GMT+02:00 Lorenzo Caminiti <lorcaminiti@gmail.com>:
On Fri, Jul 15, 2016 at 12:35 AM, Andrzej Krzemienski <akrzemi1@gmail.com> wrote:
2016-07-15 6:04 GMT+02:00 Lorenzo Caminiti <lorcaminiti@gmail.com>:
I've been considering adding a .except(...) construct to Boost.Contract that will allow to specify conditions to check at function exit but when the function body throws (in contrast to postconditions that are checked at function exit but only when the function body does not throw).
I think .except(...) could be used to assert strong exception safety guarantees... (note that class invariants are already checked at exit of public functions and also when the public function bodies throw, but invariants are suited to assert only basic, and not strong, exception safety guarantees).
How would you express the strong guarantee on std::vector::push_back?
vector::push_back exception safety:
``If no reallocations happen, there are no changes in the container in case of exception (strong guarantee). If a reallocation happens, the strong guarantee is also given if the type of the elements is either copyable or no-throw moveable. Otherwise, the container is guaranteed to end in a valid state (basic guarantee). If allocator_traits::construct is not supported with val as argument, it causes undefined behavior.''
http://www.cplusplus.com/reference/vector/vector/push_back/
Hmm... so assuming the allocator API can be augmented with an allocations() const query that returns the number of allocations done so far, and that operator== can be used to check if the vector has not changed, maybe something like this:
template<typename T> void vector<T>::push_back(T const& value) { boost::contract::old_ptr<vector<T> > old_me = BOOST_CONTRACT_OLDOF(*this); boost::contract::old_ptr<unsigned> old_allocations = BOOST_CONTRACT_OLDOF(get_allocator().allocations()); boost::contract::guard c = boost::contract::public_function(this) ... // Preconditions and postconditions. .except([&] { if( get_allocator().allocations() == *old_allocations || is_copyable<T>::value || is_nothrow_movable<T>::value ) BOOST_CONTRACT_ASSERT(*this == *old_me); // Otherwise, just basic guarantees as asserted by the class invariants. }) ;
... // Body implementation. }
I'm not 100% sure... what do you think?
It bothers me that I have to copy the entire vector upon each push_back. Because OLDOF stuff must do a copy, right? I do not think I could afford that; even in debug builds.
My point being: the idea is theoretically sound, but seems impractical. This is simply my impression. My personal view on DbC is that only the preconditions are really important, as they help discover misunderstanding and miscommunications between library/component authors and users. Postconditions are mostly useful (in my view) in that they can be matched with other functions' preconditions. In this view, the "expect" functionality is even more remote to preconditions (and hence, of less practical use). Regards, &rzej;
On Fri, Jul 15, 2016 at 10:56 AM, Andrzej Krzemienski <akrzemi1@gmail.com> wrote:
2016-07-15 19:37 GMT+02:00 Andrzej Krzemienski <akrzemi1@gmail.com>:
2016-07-15 19:22 GMT+02:00 Lorenzo Caminiti <lorcaminiti@gmail.com>:
On Fri, Jul 15, 2016 at 12:35 AM, Andrzej Krzemienski <akrzemi1@gmail.com> wrote:
2016-07-15 6:04 GMT+02:00 Lorenzo Caminiti <lorcaminiti@gmail.com>:
template<typename T> void vector<T>::push_back(T const& value) { boost::contract::old_ptr<vector<T> > old_me = BOOST_CONTRACT_OLDOF(*this); boost::contract::old_ptr<unsigned> old_allocations = BOOST_CONTRACT_OLDOF(get_allocator().allocations()); boost::contract::guard c = boost::contract::public_function(this) ... // Preconditions and postconditions. .except([&] { if( get_allocator().allocations() == *old_allocations || is_copyable<T>::value || is_nothrow_movable<T>::value ) BOOST_CONTRACT_ASSERT(*this == *old_me); // Otherwise, just basic guarantees as asserted by the class invariants. }) ;
... // Body implementation. }
I'm not 100% sure... what do you think?
It bothers me that I have to copy the entire vector upon each push_back. Because OLDOF stuff must do a copy, right? I do not think I could afford that; even in debug builds.
Absolutely, that's a very valid concern. If I decided to put such an expensive except contract in real code, I'd probably guard it with some sort of "audit" (or even "axiom") condition: template<typename T> void vector<T>::push_back(T const& value) { #if CONTRACT_AUDIT boost::contract::old_ptr<vector<T> > old_me = BOOST_CONTRACT_OLDOF(*this); boost::contract::old_ptr<unsigned> old_allocations = BOOST_CONTRACT_OLDOF(get_allocator().allocations()); #endif boost::contract::guard c = boost::contract::public_function(this) ... // Preconditions and postconditions. #if CONTRACT_AUDIT .except([&] { if( get_allocator().allocations() == *old_allocations || is_copyable<T>::value || is_nothrow_movable<T>::value ) BOOST_CONTRACT_ASSERT(*this == *old_me); // Otherwise, just basic guarantees as asserted by class invariants. }) #endif ; ... // Body implementation. } (Actually, Thorsten Ottosen mentioned something like "audit" 5+ years ago on this mailing list when discussing with me the "importance ordering" feature that was present in some of his early n-papers on contracts but later removed from N1962. He mentioned he essentially just needed "importance ordering" to the extent it allowed to specify if a given contract assertion increases the big-o complexity of the body or not. The "audit" guard can be used that way.)
My point being: the idea is theoretically sound, but seems impractical. This is simply my impression. My personal view on DbC is that only the preconditions are really important, as they help discover misunderstanding and miscommunications between library/component authors and users. Postconditions are mostly useful (in my view) in that they can be matched with other functions' preconditions. In this view, the "expect" functionality is even more remote to preconditions (and hence, of less practical use).
True. I'd also add the usefulness of class invariants (checked at entry or exit, but probably not both) in between the one of preconditions and postconditions. Actually, something similar to this was already discussed by Bertrand Meyer in Object Oriented Software Construction and then more by Mitchell & McKim in Design by Contract, by Example (books from 1990s and early 2000s respectively). That said, no reason for the framework to not offer class invariants, postconditions, and maybe even except along the side of preconditions. Some code might not even use preconditions because of performance, and that's OK. Some (most?) code will limit to using preconditions and maybe (exit) invariants. Other code (not much?) might also use postconditions and maybe even except (probably together with some "audit" or similar guards). Depending on the application, programmers can freely chose which part of the framework to use. Thanks. --Lorenzo
participants (2)
-
Andrzej Krzemienski -
Lorenzo Caminiti