Re: about the new Ada 2012 pre/post conditions

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Fri, 06 Jul 2012 18:34:37 +0200, Georg Bauhaus wrote:

> On 06.07.12 15:37, Dmitry A. Kazakov wrote:
> 
>    function sqrt (x : REAL) return REAL
>      with   Pre => True
>           Post  => sqrt'result * sqrt'result = x � eps or else *@$!;

Post =>
   (  X'Valid
   and then
      X >= 0.0
   and then
      (  sqrt'Result * sqrt'Result = X
     or else
         (  sqrt'Result * sqrt'Result > X
        and then
            sqrt'Result * sqrt'Result = X'Succ
         )
     or else
         (  sqrt'Result * sqrt'Result < X
        and then
            sqrt'Result * sqrt'Result = X'Pred
   )  )  )
or else
   (  (not X'Valid or else X < 0.0)
   and then
      Constraint_Error raised
   );

> instead, then (1) we not only have to handle exceptions,

1. Wrong. An exception is still there.

> but (2) we cannot really see from sqrt's specification what to do in order to avoid them,

2. Wrong, it is clearly seen from the post-condition

> 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.

3. Wrong. There is no whatsoever difference to dynamic check in that
respect. The implementation is same. That is BTW why there is no such thing
as "dynamic check." And surely the second part of the postcondition can be
ignored if proven that X > 0.0, which would let the optimizing compiler to
deploy a modified body without check.

See, doing things properly is always safer and no less efficient.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de