Re: Preconditions which anyway would be caught?

[Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org>]

On 08/09/2014 08:35 AM, Victor Porton wrote:
> function Inverse (X: Float) is
> begin
>     return 1/X;
> end
>     with Pre => (X /= 0);
>
> Is this precondition superfluous? (it anyway could be caught by erroneous
> 1/X operation)

This won't compile, so you have no problem.

Considering your general question, there are a number of differences between the 2:

Preconditions serve an important documentation purpose, which simply having an 
error caught at run time doesn't fulfill.

Preconditions can be used by tools, which might not be able to use the run-time 
check on division.

The precondition adds a check to every call of the function, and the division is 
not performed if the precondition fails. The division, and any associated check, 
is always performed without the precondition.

An alternative might be to use a subtype

subtype Invertable_Float is Float with
    Dynamic_Predicate => Invertible_Float /= 0.0;

function Invert (X : Invertable_Float) return Float;

Finally, are you sure the division will raise an exception?

with Ada.Command_Line;
with Ada.Text_IO;

procedure Inverse_Test is
    function Inverse (X : Float) return Float is
       -- Empty declarative part
    begin -- Inverse
       return 1.0 / X;
    end Inverse;

    F : constant Float :=
       Inverse (Float'Value (Ada.Command_Line.Argument (1) ) );
begin -- Inverse_Test
    Ada.Text_IO.Put_Line (Item => Float'Image (F) );
end Inverse_Test;

$ gnatmake -gnatano -fstack-check -gnatwa inverse_test.adb
gcc-4.6 -c -gnatano -fstack-check -gnatwa inverse_test.adb
gnatbind -x inverse_test.ali
gnatlink inverse_test.ali -fstack-check
$ ./inverse_test 0.0
  +Inf*******

You might want to review floating-point types and look at the 'Machine_Overflows 
attribute.

-- 
Jeff Carter
"Insufficient laughter--that's grounds for divorce."
Play It Again, Sam
126