Re: [boost] [contract] Strong exception safety guarantees

15 Jul 2016

      On Fri, Jul 15, 2016 at 10:56 AM, Andrzej Krzemienski
 wrote:
...
2016-07-15 19:37 GMT+02:00 Andrzej Krzemienski :
...
2016-07-15 19:22 GMT+02:00 Lorenzo Caminiti :
...
On Fri, Jul 15, 2016 at 12:35 AM, Andrzej Krzemienski
 wrote:
...
2016-07-15 6:04 GMT+02:00 Lorenzo Caminiti :
template<typename T>
void vector<T>::push_back(T const& value) {
    boost::contract::old_ptr 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 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