[boost] [contract] move operations and class invariants

Subject: [boost] [contract] move operations and class invariants
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2017-11-29 04:39:23

Hello all,

This is not really a question about Boost.Contract, but more a
question on how contract programming interacts with C++ move
operations.

C++ requires that moved-from objects can still be destructed. Because
contract programming requires class invariants to hold at destructor
entry, it follows that moved-from objects must still satisfy class
invariants.

That sounds restrictive... and it might force the class invariants to
be empty. For example, for vector a class invariant is size() <=
capacity(). Should that sill hold after the vector has been moved?
That means I can still call size() and capacity() on a moved-from
object, which might not be the case.

If some sort of moved() function could be called on a moved-from
object, the invariants could be programmed as follow to work around
this issue:

class vector {
    void invariant() cont {
        if(!moved()) BOOST_CONTRACT_ASSERT(size() <= capacity());
        ... // Only invariants that are truly needed to execute the destructor.
    }

    bool moved() const;

public:
    vector(vector&& other) {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                 BOOST_CONTRACT_ASSERT(!moved());
                 BOOST_CONTRACT_ASSERT(other.moved());
            })
        ;
        ...
    }

    ...
};

I'm not really sure... What do you think? Do you know if this topic
"C++ move & class invariants" has already been discussed somewhere?

Thanks.
--Lorenzo