[boost] [contract] Class invariants (also for static and volatile/const-volatile public functions)

Subject: [boost] [contract] Class invariants (also for static and volatile/const-volatile public functions)
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2016-07-21 10:54:33

Hello all,

I would like to discuss class invariants, but also for static and
volatile/const-volatile public member functions, and specifically with
respect to how Boost.Contract handles them.

Class invariants are important... almost as important as
preconditions. For example for a vector container, class invariants
specify among other things the equivalence relationship `(size() == 0)
== empty()` that could be found useful by static analyzers and
optimizes (also discussed in N4160):

    template<typename T>
    class vector {
        [[invariant: (size() == 0) == empty()]]
        [[invariant: size() <= capacity()]]

    public:
        void push_back(T const& value) ... { ... }
    };

The above contract cannot be programmed using preconditions and
postconditions unless: it is repeated (together with all other
invariant assertions) in pre- and postconditions of each public member
functions, it is asserted with try-catches also when those functions
throw, it is repeated in constructor postconditions, in destructor
preconditions, and with try-catches also when destructors throw...
Even if invariants are programmed in some `bool invariant() const`
function to avoid repeating all invariant assertions in each pre- and
postcondition, the code will be cluttered by boiler-plate code
(try-catch to assert invariants on throw, etc.) and an invariant
failure will just report that the invariant() function returned false,
but it will not report which specific invariant condition actually
failed (plus static analyzers and optimizes will not be able to parse
the conditions from the invariant function):

    template<typename T>
    class vector {
        bool invariant() const {
            // But cannot distinguish which of the two assertions failed...
            // and cannot be used by static analyzers and optimizers.
            return (size() == 0) == empty() && size() <= capacity();
        }

    public:
        void push_back(T const& value)
            ...
            [[requires: invariant()]]
            [[ensures: invariant()]]
        {
            try { ... }
            catch(...) { [[assert: invariant()]]; throw }
        }
    };

Class invariants cannot be effectively emulated using pre- and
postconditions... they should be added to a contract framework as
their own feature.

In Boost.Contract:

    template<typename T>
    class vector {
        void invariant() const {
            BOOST_CONTRACT_ASSERT((size() == 0) == empty());
            BOOST_CONTRACT_ASSERT(size() <= capacity());
        }

    public:
        void push_back(T const& value) {
            boost::contract::guard c =
boost::contract::public_function(*this) ... ;
            ...
        }
    };

Note that the above invariant function `void invariant() const` cannot
be declared static or const-volatile because it will need to call
queries like size(), empty(), capacity(), etc. that are const and not
static or const-volatile. Thus the above invariant function, being
const, cannot be called at entry and exit of static and
volatile/const-volatile public functions. A contract framework for C++
should support also static and const-volatile class invariants to
properly handle static and volatile/const-volatile public functions
(even if static and const-volatile class invariants are not mentioned
in any C++ contract proposal):

* Static public functions check static class invariants at entry, at
exit, and if body throws.
* Volatile and const-volatile public functions check static and
const-volatile class invariants (in that order) at entry, at exit, and
if body throws.
* Non cv-qualified and const public functions check static,
const-volatile, and const class invariants (in that order) at entry,
at exit, and if body throws.
* Constructors check static class invariants at entry, at exit, and if
body throws (because those do not require the object to be
constructed). Then constructors check const-volatile and const class
invariants (in that order) at exit (if body does not throw, because
those require the object to be constructed).
* Destructors check static class invariants at entry, at exit, and if
body throws (because those do not require a constructed object). Then
destructors check const-volatile and const class invariants (in that
order) at entry and if body throws (because those require a
constructed object).

In Boost.Contract:

    struct a {
        static void static_invariant()  { BOOST_CONTRACT_ASSERT(...); }
        void invariant() const volatile { BOOST_CONTRACT_ASSERT(...); }
        void invariant() const          { BOOST_CONTRACT_ASSERT(...); }

        // Following check all static_invariant(), invariant() const
volatile, and invariant() const (in that order).

        a() {
            boost::contract::guard c= boost::contract::constructor(this);
        }

        virtual ~a() {
            boost::contract::guard c = boost::contract::destructor(this);
        }

        void m() /* no cv qualifiers */ {
            boost::contract::guard c = boost::contract::public_function(*this);
        }

        void c() const {
            boost::contract::guard c = boost::contract::public_function(*this);
        }

        // Following check both static_invariant() and invariant()
const volatile (in that order).

        void v() volatile {
            boost::contract::guard c = boost::contract::public_function(*this);
        }

        void cv() const volatile {
            boost::contract::guard c = boost::contract::public_function(*this);
        }

        // Following check only static_invariant().

        static void s() {
            boost::contract::guard c = boost::contract::public_function<a>();
        }
    };

Maybe volatile member functions are rarely used in C++ so
const-volatile class invariants will also be used rarely if at all...
Nevertheless, if const-volatile class invariants are not supported, it
will not be possible to specify invariants for classes with volatile
public functions so const-volatile class invariants should be
supported for completeness.

Static class invariant could instead be useful when programming
contracts for the static part of the object state. In particular,
Boost.Contract also supports postconditions for destructors (those
should be checked by a static function because they should not access
the object `this` that has been destroyed after the execution of the
destructor body). Destructor postconditions are not mentioned in any
contract proposal... but together with constructor and other function
pre- and postconditions, and together with static class invariants,
they can specify contracts for the static part of the object state.
For example, consider the contracts for a class that counts the number
of its object instances:

    struct a : private noncopyable, private nonmovable {
        static void static_invariant() {
            BOOST_CONTRACT_ASSERT((instances() != 0) == exists());
        }

        a() {
            boost::contract::old_ptr<unsigned> old_instances =
                    BOOST_CONTRACT_OLDOF(instances());
            boost::contract::guard c = boost::contract::constructor(this)
                .postcondition([&] {
                    BOOST_CONTRACT_ASSERT(instances() == old_instances + 1);
                })
            ;

            ++instances_;
        }

        virtual ~a() {
            boost::contract::old_ptr<unsigned> old_instances =
                    BOOST_CONTRACT_OLDOF(instances());
            boost::contract::guard c = boost::contract::destructor(this)
                .postcondition([&] { // Must never use object `this`.
                    BOOST_CONTRACT_ASSERT(instances() == old_instances - 1);
                })
            ;

            --instances_;
        }

        static unsigned instances() {
            boost::contract::guard c = boost::contract::public_function<a>();
            return instances_;
        }

        static bool exists() {
            boost::contract::guard c = boost::contract::public_function<a>();
            return instances_ != 0;
        }

    private:
        static unsigned instances_;
    };

    unsigned a::instances_ = 0;

--Lorenzo