[boost] [contract] extra type requirements for contracts

Subject: [boost] [contract] extra type requirements for contracts
From: lcaminiti (lorcaminiti_at_[hidden])
Date: 2011-09-19 13:12:32

Hello all,

Andrzej and I have been discussing off-line the following issue:

    How to program contract assertions without adding extra type
requirements.

I would like to get Boosters' input on possible solutions for this problem.

THE PROBLEM

Consider the following contract for vector::push_back:

CONTRACT_CLASS(
template( typename T )
class (myvector)
) {
    ...

    CONTRACT_FUNCTION_TPL(
    public void (push_back) ( (const T&) value )
        precondition(
            size() < max_size(),
        )
        postcondition(
            auto old_size = CONTRACT_OLDOF size(),
            auto old_capacity = CONTRACT_OLDOF capacity(),
            back() == value, // (1)
            size() == old_size + 1,
            capacity() >= old_capacity,
        )
    ) ;
};

Postcondition (1) introduces the extra requirement EqualityComparable<T>.
This is not ideal because this requirement is only needed to check the
contract but not to implement the push_back functionality (body). For
example:

struct pod {}; // not EqualityComparable

std::vector<pod> v;
v.push_back(pod()); // ok, does not require EqualityComparable<pod>

myvector<pod> w;
w.push_back(pod()); // complier-error, can't find operator== for type pod...

Because of postcondition (1), myvector cannot be used on pod while the
std::vector can!

This is a general issue with contracts. In general, an arbitrary complex
(const) expression can be used to assert preconditions, postconditions, or
invariants. Such a complex assertion might introduce an arbitray set of
extra requirements on the types used, requirements that might not be
necessary to implement the function body. The extra type requirements
introduced by the contracts are especially problematic when programming
templates because the used types are generic and it is not know a priori to
the function programmer if the generic types will or not satisfy the
requirements.

POSSIBLE SOLUTIONS

A possible solution is to specify the type requirements that a given
assertion introduces. If the type requirements are met, the assertion will
be compiled and checked at run-time. If the type requirements are not met,
the assertion will not be compiled (so not compiler-error "missing
operator== for type ...") and not checked at run-time for that specific
type. For example:

    CONTRACT_FUNCTION_TPL( // Option 1
    public void (push_back) ( (const T&) value )
        precondition(
            size() < max_size(), requires has_less<size_type>::value
        )
        postcondition(
            auto old_size = CONTRACT_OLDOF size(),
                    requires const_copy_constructor<size_type>::value
            auto old_capacity = CONTRACT_OLDOF capacity(),
                    requires const_copy_constructor<size_type>::value
            back() == value, requires has_equal_to<T>::value // assertion
type requirements
            size() == old_size + 1,
                    requires has_equal_to<size_type>::value &&
                             has_plus<size_type>::value
            capacity() >= old_capacity,
                    requires has_greater_equal<size_type>::value
        )
    ) ;

Here I have specified assertion type requirements using `requires` for each
assertion. However, size_type is known a priori to be essentially an
unsigned int for which all these type requirements will always be met so the
type requirements on size_type could have been omitted. That said, you can
easily imagine an example for a different template class or function where
size_type is also a generic type for which const copy constructor, +, ==,
etc might not always be available.

Another option would be would be to specify the type requirements for
precondition/postcondition instead than for each assertion:

    CONTRACT_FUNCTION_TPL( // Option 2.
    public void (push_back) ( (const T&) value )
        precondition(
            size() < max_size(),
        ) requires has_less<size_type>::value // pre/postcondition type
requirements
        postcondition(
            auto old_size = CONTRACT_OLDOF size(),
            auto old_capacity = CONTRACT_OLDOF capacity(),
            back() == value,
            size() == old_size + 1,
            capacity() >= old_capacity,
        ) requires
                const_copy_constructor<size_type>::value && 
                has_equal_to<T>::value &&
                has_plus<size_type>::value &&
                has_greater_equal<size_type>::value
    ) ;

Options 2 is less verbose and it does not specify the same type requirements
multiple time for the different assertions. However, I prefer Option 1
because if T is not equality comparable, only the postcondition `back() ==
value` is not checked but all the other postconditions are still checked.
With Option 2 if one type requirement is not met, then all
preconditions/postconditions are not checked causing more bugs to go
unobserved.

If the re-use of the preprocessor "keyword" `requires` was found confusing
because of its different semantics when used with concepts, a different
preprocessor "keyword" like `unless` could be used instead:

CONTRACT_FUNCTION( // Option 3
template( typename InIter1, typename InIter2, typename OutIter, typename
BinOp )
    requires(
        boost::InputIterator<InIter1>,
        boost::InputIterator<InIter2>,
        typename CONTRACT_IDENTITY_TYPE(( boost::OutputIterator&lt;OutIter,
                typename boost::InputIterator&lt;InIter1&gt;::value_type >
)),
        typename CONTRACT_IDENTITY_TYPE(( boost::BinaryFunction&lt;BinOp,
                typename boost::InputIterator&lt;InIter1&gt;::value_type,
                typename boost::InputIterator<InIter1>::value_type,
                typename boost::InputIterator<InIter2>::value_type> ))
    )
(OutIter) (mytransform) ( (InIter1) first1, (InIter1) last1, (InIter2)
first2,
        (OutIter) result, (BinOp) op )
    precondition( contract::trivial::range(first1, last1).valid() )
    postcondition(
        auto return_value = return,
        return_value == result, unless !has_equal_to<T>::value // use unless
    )
) {
    return std::transform(first1, last1, first2, result, op);
}

Reflections:
a) All these solutions require extensive type traits support to write the
contract type requirements (I cannot use concepts because they greedily
generate compiler-errors when they are not met). However, I see no way
around this: I must be able to check the type requirements (extensively
using type traits) in order to disable the assertion compilation and their
run-time check.
b) All these solutions leave the assertions in the contracts so the contract
code retains its self-documentation value even then the assertion checking
is disabled because the type requirements are not met.
c) N1962, Eiffel, D, A++, and all other Contract Programming references that
I have seen do not address the issue of the extra type requirements. I am
not sure why... Eiffel has generic types but you can always compare them for
equality, for non Void, etc.
d) In practice, this might not be a big deal because most of the times
old-of is applied to counters (int) and postconditions are the ones
introducing the extra requirement but only of EqualityComparable. However,
in general I think I need to provide a solution for this issue.

What do you think?

Thanks a lot!
--Lorenzo

--
View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-extra-type-requirements-for-contracts-tp3824535p3824535.html
Sent from the Boost - Dev mailing list archive at Nabble.com.