
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 <contract/utility.hpp>. 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 <contract/trivial.hpp> // the trivial contract helpers #include <boost/concept_check.hpp> 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-tp3563993p379443... Sent from the Boost - Dev mailing list archive at Nabble.com.