
Boost : 
Subject: Re: [boost] [contract] toward N3351 concepts
From: Vicente J. Botet Escriba (vicente.botet_at_[hidden])
Date: 20121002 17:29:34
Le 26/09/12 21:00, Lorenzo Caminiti a écrit :
> Hello all,
>
>
>
> However, N3351 says that axioms should not be checked by the compiler...
>
> ``Axioms express the semantics of a concept’s required syntax; they
> are assumed to be true and
> must not be checked by the compiler beyond conformance to the C++
> syntax. Any additional
> checking is beyond the scope of the compiler’s translation
> requirements. The compiler must not
> generate code that evaluates axioms as preconditions, either. This
> could lead to program errors
> if the evaluated assertions have side effects. For example, asserting
> that distance(first, last) > 1
> when the type of those iterators is istream_iterator will consume the
> first element of the range,
> causing the assertion to pass, but the algorithm to have undefined behavior.''
>
> So what am I supposed to do with axioms? Do nothing? Axioms are just
> "comments" that document the semantic?
>
> For example:
>
> ``
> concept EqualityComparable<typename T> =
> requires (T a, T b, T c) {
> bool { a == b };
> bool { a != b };
> axiom { a == b <=> eq(a, b); } // true equality
> axiom {
> a == a; // reflexive
> a == b => b == a; // symmetric
> a == b && b == c => a == c; // transitive
> }
> axiom { a != b <=> !(a == b); } // complement
> };
>
> So, EqualityComparable<T> is true if T
> 1. has == and != with result types that can be converted to bool
> 2. == compares for true equality
> 3. == is reflexive, symmetric, and transitive
> 4. != is the complement of ==
> However, the compiler can only check the first of these conditions.
> The rest must be verified
> through other means (i.e. manually).
> ''
>
Hi Lorenzo,
Not only the compiler should not check the axioms, but it will in
general be unable to do it. So a type modeling the nonaxiom part is
seen as a model of the concept even if doesn't satisfy the axioms.
An alternative for the concept definition could be to force the modeler
to state explicitly that the class satisfies some kind of semantic trait
associated to the axiom.
The preceding example can be rewrite as follows
concept EqualityComparable<typename T> =
TrueEquality<T> && EqualReflexive<T> && EqualSymetric<T> && EqualTransitive<T> &&
requires (T a, T b, T c) {
bool { a == b };
bool { a != b };
};
where
concept TrueEquality<typename T> = is_true_equal<T>::value &&
requires (T a, T b) {
axiom { a == b <=> eq(a, b); } // true equality
};
concept EqualReflexive<typename T> = is_equal_reflexive<T>::value &&
requires (T a) {
a == a; // reflexive
};
concept EqualSymmetric<typename T> = is_equal_symetric<T>::value &&
requires (T a, T b) {
a == b => b == a; // symmetric
};
concept EqualTransitive<typename T> = is_equal_transitive<T>::value &&
requires (T a, T b, T c) {
a == b && b == c => a == c; // transitive
};
The traits is_true_equal, is_equal_reflexive, is_equal_symmetric and
is_equal_transitive could be defined for the builtin types as a
truetype and a falsetype otherwise. A user defining a class X that is
a model of EqualityComparable should need however to specialize these traits
template <> is_true_equal<X>: true_type {};
template <> is_equal_reflexive<X>: true_type {};
template <> is_equal_symmetric<X>: true_type {};
template <> is_equal_transitive<X>: true_type {};
In this way, the compiler could take advantage of the axioms but only
when the modeler has given permission.
This has of course a lot of disadvantages as ...
Best,
Vicente
Boost list run by bdawes at acm.org, gregod at cs.rpi.edu, cpdaniel at pacbell.net, john at johnmaddock.co.uk