Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 06.07.12 15:37, Dmitry A. Kazakov wrote:
>>> I'd rather stay on the safe side
>>> >> considering sqrt (-1.0) happen. So, what about the effect?
>> > 
>> > If you know that you might be running an incorrect program,
>> > the effect is similar to that of using Unchecked_Conversion.
> Maybe for Ada 202X, but in contemporary Ada it is Constraint_Error
> propagation.

Could you leave clauses of an explicitly state contract in the
text where there was one?

   function sqrt (x : REAL) return REAL
     with   Pre => x >= 0.0;

Ada's sqrt, as opposed to the sqrt above, adds a run-time check,
fully dynamic. The programmer can throw anything at Ada's sqrt,
quite carelessly. Its contract isn't specified in source text,
but requires that the programmer study the language manual in
order to learn about his obligations, and possible consequences.
When not, the program needs to handle Constraint_Error all over
the place because he or she *never* knows what precondition
to establish, other than by reading through more or less formal
comments.

Triply bad. If we had

   function sqrt (x : REAL) return REAL
     with   Pre => True
          Post  => sqrt'result * sqrt'result = x � eps or else *@$!;

instead, then (1) we not only have to handle exceptions, but (2) we cannot
really see from sqrt's specification what to do in order to avoid them,
and (3) we cannot have an efficient sqrt because Ada's sqrt forces
a test on us that is quite unnecessary once we know, i.e. have shown,
that x >= 0.0 is always true before calling sqrt.

So Ada's sqrt is programmed defensively, whereas the line of defence
in a program designed by contract is to feel obliged by the contract
and then either demonstrate correctness, or leave the checks in!