Preconditions which anyway would be caught?

Preconditions which anyway would be caught?

[Victor Porton]

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)

-- 
Victor Porton - http://portonvictor.org

Re: Preconditions which anyway would be caught?

[mockturtle]

On Saturday, August 9, 2014 5:35:21 PM UTC+2, 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)

Still not a LL... I would say it is not.  It depends on the "reason" for specifying the precondition.  As I see it, the precondition is a kind of "formal documentation" of the conditions that must be satisfied when you call the function.  As a side effect, you can have those conditions checked at run-time as a "bug trap," but, for example, they could be used by some formal checking software.  So, even if calling the function with X=0 will cause an error, I would keep the precondition.

Riccardo

Re: Preconditions which anyway would be caught?

[Jeffrey Carter]

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

Re: Preconditions which anyway would be caught?

[Peter Chapin]

On 2014-08-09 11:35, 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)

Proper syntax here is

function Inverse(X : Float)
  with Pre => (X /= 0) is
begin
   return 1/X;
end;

SPARK 2014 will attempt to prove that the precondition is satisfied at
every call site. It will also try to prove that 1/X will never entail
division by zero, which is trivial to do with the precondition present.

If you remove the precondition, SPARK will not try to prove anything
about X at the call site but it will still try to prove that 1/X does
not entail division by zero. Unfortunately there isn't enough
information to make that second proof go through so you'll end up with
an undischarged verification condition.

The precondition is a statement about the intended behavior of the
subprogram. It is, in some sense, part of the subprogram's design.
Without the precondition you are implying that it is okay to call
Inverse for any Float value at all. What is the subprogram supposed to
do when given 0.0? Raising Constraint_Error is unsightly because it
typically means the programmer made a mistake. So the version without
the precondition might more correctly be written as

function Inverse(X : Float) is
begin
   if X = 0.0. then
      raise Invalid_Domain;  -- Documented exception for this purpose.
   else
      return 1/X;
   end if;
end;

Peter

Re: Preconditions which anyway would be caught?

[Peter Chapin]

On 2014-08-09 15:21, Peter Chapin wrote:

> Proper syntax here is
> 
> function Inverse(X : Float)
>   with Pre => (X /= 0) is
> begin
>    return 1/X;
> end;

Well that's closer. How about

function Inverse(X : Float) return Float
  with Pre => (X /=0) is
begin
   return 1/X;
end;

Peter

Re: Preconditions which anyway would be caught?

[Niklas Holsti]

On 14-08-09 22:24 , Peter Chapin wrote:
> On 2014-08-09 15:21, Peter Chapin wrote:
> 
>> Proper syntax here is
>>
>> function Inverse(X : Float)
>>   with Pre => (X /= 0) is
>> begin
>>    return 1/X;
>> end;
> 
> Well that's closer. How about
> 
> function Inverse(X : Float) return Float
>   with Pre => (X /=0) is
> begin
>    return 1/X;
> end;

Just to be a pedant: shouldn't that have some decimals on the literals:

function Inverse(X : Float) return Float
  with Pre => (X /= 0.0) is
begin
  return 1.0/X;
end;

In addition, is it really true that all Float numbers /= 0.0 can be
inverted without error? What if X is a denormalized number which has
suffered gradual underflow... won't its inverse overflow, because there
is no concept of "gradual overflow" in IEEE floats?

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
      .      @       .

Re: Preconditions which anyway would be caught?

[Peter Chapin]

On 2014-08-09 17:04, Niklas Holsti wrote:

> Just to be a pedant: shouldn't that have some decimals on the literals:
> 
> function Inverse(X : Float) return Float
>   with Pre => (X /= 0.0) is
> begin
>   return 1.0/X;
> end;
> 
> In addition, is it really true that all Float numbers /= 0.0 can be
> inverted without error? What if X is a denormalized number which has
> suffered gradual underflow... won't its inverse overflow, because there
> is no concept of "gradual overflow" in IEEE floats?

I wondered about that also, in fact.

I just tried it with your corrections so it actually *does* compile.
Without any precondition SPARK 2014 complains that

	overflow check might fail
	divide by zero check might fail

With the precondition of X /= 0.0 SPARK says

	overflow check might fail

However, this proves fine:

   function Inverse(X : Float) return Float
     with Pre => not(-1.0E-35 < X and X < +1.0E-35) is
   begin
      return 1.0/X;
   end;

I didn't experiment to see how close to zero I could make the bounds in
the precondition but clearly your concern is a valid one.

Peter

Re: Preconditions which anyway would be caught?

[Dmitry A. Kazakov]

On Sun, 10 Aug 2014 00:04:11 +0300, Niklas Holsti wrote:

> On 14-08-09 22:24 , Peter Chapin wrote:
>> On 2014-08-09 15:21, Peter Chapin wrote:
>> 
>>> Proper syntax here is
>>>
>>> function Inverse(X : Float)
>>>   with Pre => (X /= 0) is
>>> begin
>>>    return 1/X;
>>> end;
>> 
>> Well that's closer. How about
>> 
>> function Inverse(X : Float) return Float
>>   with Pre => (X /=0) is
>> begin
>>    return 1/X;
>> end;
> 
> Just to be a pedant: shouldn't that have some decimals on the literals:
> 
> function Inverse(X : Float) return Float
>   with Pre => (X /= 0.0) is
> begin
>   return 1.0/X;
> end;
> 
> In addition, is it really true that all Float numbers /= 0.0 can be
> inverted without error? What if X is a denormalized number which has
> suffered gradual underflow... won't its inverse overflow, because there
> is no concept of "gradual overflow" in IEEE floats?

But 1.0/0.0 is perfectly OK in IEEE floats. It is NaN.

Methodically the approach is wrong. A precondition is chosen to ensure the
post-condition. What is the post-condition of Inverse?

1. Whatever garbage but no exceptions
2. 1.0/X * X in 1.0 - err .. 1.0 + err
...

Once the post-condition is defined, the precondition is the least
constraint allowing an implementation that ensures it.

Specifying precondition for the sake of having them is meaningless.

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

Re: Preconditions which anyway would be caught?

[Niklas Holsti]

On 14-08-10 01:57 , Peter Chapin wrote:
> On 2014-08-09 17:04, Niklas Holsti wrote:
> 
>> Just to be a pedant: shouldn't that have some decimals on the literals:
>>
>> function Inverse(X : Float) return Float
>>   with Pre => (X /= 0.0) is
>> begin
>>   return 1.0/X;
>> end;
>>
>> In addition, is it really true that all Float numbers /= 0.0 can be
>> inverted without error? What if X is a denormalized number which has
>> suffered gradual underflow... won't its inverse overflow, because there
>> is no concept of "gradual overflow" in IEEE floats?
> 
> I wondered about that also, in fact.
> 
> I just tried it with your corrections so it actually *does* compile.
> Without any precondition SPARK 2014 complains that
> 
> 	overflow check might fail
> 	divide by zero check might fail
> 
> With the precondition of X /= 0.0 SPARK says
> 
> 	overflow check might fail
> 
> However, this proves fine:
> 
>    function Inverse(X : Float) return Float
>      with Pre => not(-1.0E-35 < X and X < +1.0E-35) is
>    begin
>       return 1.0/X;
>    end;
> 
> I didn't experiment to see how close to zero I could make the bounds in
> the precondition but clearly your concern is a valid one.

I think the actual precondition and function were only examples to
illustrate the OP's question, so we are off-topic, too bad. But to
continue: I wrote a program that initializes X to 1.0 and repeatedly
divides by 2.0 until X is zero, printing X and 1.0/X each time. The
break is here:

X =  1.17549E-38, 1.0/X =  8.50706E+37
X =  5.87747E-39, 1.0/X =  1.70141E+38
X =  2.93874E-39, 1.0/X =  +Inf*******
X =  1.46937E-39, 1.0/X =  +Inf*******

and the last non-zero value is

X =  1.40130E-45, 1.0/X =  +Inf*******

This is with an unconstrained X : Float. Float'Machine_Overflows is
False. If I assign 1.0 / X to a variable Y of the subtype "Float range
Float'Range" I of course get a Constraint_Error instead of the +Inf.

Computing 1.0 / Float'Last gives 2.93874E-39, and a compile-time (!)
warning from GNAT that "gradual underflow causes loss of precision". Neat.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
      .      @       .

Re: Preconditions which anyway would be caught?

[Shark8]

On 10-Aug-14 01:24, Dmitry A. Kazakov wrote:
> Specifying precondition for the sake of having them is meaningless.

Not all preconditions imply a post-condition; sometimes it's simply to 
constrain the values that you're willing to entertain; for example if 
you have Natural_Float being a subtype of float (range 0.0 .. 
Float'Last) you could use this in an internal simple simulator with 
Square_Root(X: Natural_Float) return Float being a function therein.

Re: Preconditions which anyway would be caught?

[Dmitry A. Kazakov]

On Sun, 10 Aug 2014 18:00:36 -0600, Shark8 wrote:

> On 10-Aug-14 01:24, Dmitry A. Kazakov wrote:
>> Specifying precondition for the sake of having them is meaningless.
> 
> Not all preconditions imply a post-condition; sometimes it's simply to 
> constrain the values that you're willing to entertain;

All.

> for example if 
> you have Natural_Float being a subtype of float (range 0.0 .. 
> Float'Last) you could use this in an internal simple simulator with 
> Square_Root(X: Natural_Float) return Float being a function therein.

The precondition of Square_Root en-force is True, thus calling Square_Root
(-1.0) is not an error.

Constraints are "dynamic preconditions" in Ada 2012 Newspeak.

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