Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2012-10-08 06:06:32

>
> Is it legal "to state" with axioms, something that is not true in
>>> general case?
>>>
>> That's an open question--for me. There may be a good answer to that
>> question in the literature or addressed in other domains.
>>
>
Axioms so far have not been standardized, nor has anyone prepared a formal,
unambiguous specification of how they would be handled. People have
different views on and expectations of axioms. N2887 has been the best
attempt so far to specify what axioms are supposed to mean to the compiler
and other tools. So some answer could be given based on N2887. Basically,
what it says is that axioms only reflect current practice of writing
generic code, rather than inventing something new. So what do you think of
STL algorithms that operate on doubles in C++11?:

  void find_me( std::vector<double> const& vec, double n )
  {
    std::find(vec.begin(), vec.end(), 10.2);
    std::find(vec.begin(), vec.end(), n);
  }

Is it legal? Is it correct? Is it good practice? can 'n' be NaN?

My answer is: STL algorithms will make an assumption that operations on 'T'
are symmetrical, that comparisons for 'T' meet the three relations
(reflexivity, symmetry, transitivity). STL implementations will not in
general verify these assumptions, but may use these assumptions in as many
places as they want, and you will never know when. Some implementations may
do some run-time checks (in debug versions), where they know they could not
spoil the program, but this is QoI issue.

Should the programmer instantiate STL algorithms for 'T' == double? My
answer is: they know the risks (of potentially not meeting the
assumptions), they should assess if the risk is low or make sure they
eliminate the usage of NaNs, and they should make the call at their own
risk. If the program has a bug due to type double not having met the
assumptions on 'T' it is the fault of the programmer who requested the
instantiation of the algorithm with type double.

Axioms (according to N2887) do not change this situation. An assumption of
type 'T' is never 'valid' or 'invalid'. It is just an assumption that one
may use or not. When you request an instantiation of an algorithm
constrained with an 'axiom-rich' concept with type X, you take the
responsibility for X meeting or not the expectations expressed in the
concept.

> Just to clarify: question was about C++ axioms.
> Is it illegal (from formal point of view of C++ axioms), to have:
>
> axiom { a.size() == a.length(); }
> and:
> int T:size() { return 0;}
> int T:length() { return 1;}
> ?
>
> Does compiler have the authority (from formal point of view of C++ axioms)
> to stop compilation with error in such case(of course, if it able to
> diagnose that)?

>
>
>  It may be sufficient to simply assume that floating point operations
>> satisfy the abstract mathematical requirements. We generally do
>> anyways.
>>
>
> For most cases - we may assume floating-point addition associativity. For
> some cases not.
> Currently, we may control this by compiler-dependent flags.
> For instance /fp:fast /fp:precise flags of MSVC compiler - with /fp:fast
> MSVC2012 does auto-vectorization (SSE) of floating-point accumulation.
>
> If compiler has right to reject wrong axioms when he able to diagnose,
> then we can't use C++ axioms to express in code our assumption about
> floating-point addition associativity.
>

This question is somewhat similar to: can compiler refuse to compile the
following code:

  void Terminator() noexcept
  {
    throw std::runtime_error();
  }

We know that the compiler must not in general check this, but in the above
particular case it is obvious that someone has planted a bug. But the
answer is still: the compiler must not reject this code. However, it is
allowed to report a warning (compilation warnings are not in scope of the
C++ standard); and it would be surprising if a good compiler didn't do it.
And you are allowed to set the compiler option to treat warnings (at least
of this type) as errors.

The good strategy for compilers, regarding axioms, would be to make use of
axioms only if they have some way of verifying if type 'X' meets them,
(either by limited static code analysis or run-time checks). This might
require selecting only a subset of all axioms that the compiler is able to
check and utilize only this subset.

Regards,
&rzej