Re: [boost] [contract] syntax redesign

Subject: Re: [boost] [contract] syntax redesign
From: lcaminiti (lorcaminiti_at_[hidden])
Date: 2011-09-06 16:05:59

Andrzej Krzemienski wrote:
> 
>> This use case is different then the above (more compelling). The
>> issues here is that when programming contracts you quickly start using
>> extra checks (and especially ==) which add additional requirements on
>> generic types. For example, in this case T does not have to be
>> EqualityComparable to program the body but you still want to program
>> and check the postcondition when T happens to be EqualityComparable. I
>> have been thinking to solve this issue by providing:
> 
>> namespace contract {
> 
>> temlate< typename T>
>> bool equal(T const& left, T const& right) ...
>> }
> 
>> equal will return true if T is not EqualityComparable and left ==
>> right if T is EqualityComparable. That way you can program the
>> contracts using contract::equal(x, y) without introducing additional
>> requirements on T at all but still checking the contract conditions
>> for EqualityComparable types. I will also expand equal to handle
>> containers (compare all elements of a vector, etc) and I will provide
>> similar functions for other operations. All of these contract helper
>> functions will be in a separate header &lt;contract/utility.hpp&gt;. I
>> have
>> not started to implement this yet.
> 
> To me, this problem with equality indicates that Boost.Concept already
> proves useful, as it explores practical aspects of implementing DbC in C++
> and its interactions with other C++ features.
> 

I am thinking to address the issue of "how to write contracts using == (or
similar operations) for generic types that might not be EqualityComparable
without adding the EqualityComparable type requirement when it is not
necessary for implementing the body" as follow: I can provide a
contract::trivial::operator== which trivially returns true. Programmers can
add a using directive in their contracts (e.g., postconditions) if they wish
to use such a trivial operator. The trivial operator will be used by C++
only if no other operator if found for the type so only if the type was not
EqualityComparable.

For example:

#include <contract.hpp>
#include &lt;contract/trivial.hpp&gt; // the trivial contract helpers
#include &lt;boost/concept_check.hpp&gt;

template< typename T >
class Addable { // User-defined concept.
    T x;
    T y;
    void return_type ( T ); // Used to check addition returns type `T`.
public:
    BOOST_CONCEPT_USAGE(Addable) {
        return_type(x + y); // Check addition `T operator+(T x, T y)`.
    }
};

CONTRACT_FUNCTION(
template( typename T ) requires( Addable<T> )
(T) (add) ( (T) x, (T) y )
    postcondition(
        using contract::trivial::operator==, // (1)
        auto result = return,
        result == x + y // Trivial == if T not EqualityComparable.
    )
) {
    return x + y;
}

Note that using directives (and namespace aliases) such as (1) above are
allowed within contracts because they cannot change the run-time state so
they maintain the contract constant-correctness requirement. Furthermore,
contracts are specified with the function declarations so usually in header
files where namespace manipulations are best avoided and therefore it might
be handy to manipulate names locally within the contracts to simply names.

--Lorenzo

--
View this message in context: http://boost.2283326.n4.nabble.com/contract-syntax-redesign-tp3563993p3794436.html
Sent from the Boost - Dev mailing list archive at Nabble.com.