Re: SPARK - runtime checks question

[Adam Beneschan <adam@irvine.com>]

On Jun 19, 8:26 am, Maciej Sobczak <see.my.homep...@gmail.com> wrote:
> Consider the following:
>
> -- my_package.ads:
> package My_Package is
>    function Distance (X : in Natural; Y : in Natural) return Natural;
> end My_Package;
>
> -- my_package.adb:
> package body My_Package is
>
>    function Distance (X : in Natural; Y : in Natural) return Natural
>    is
>       Result : Natural;
>    begin
>       if X > Y then
>          Result := X - Y;    // line 8
>       else
>          Result := Y - X;    // line 10
>       end if;
>       return Result;
>    end Distance;
>
> end My_Package;

Apologies in advance for answering a question you didn't ask, but...
any reason not to simply return abs(X-Y)?  If you're thinking that the
result of X-Y will raise a Constraint_Error if it's negative---it
won't.  (At least not in Ada.  I don't know much about SPARK---it
wouldn't raise Constraint_Error there either, would it?)

                                -- Adam