Re: Preconditions which anyway would be caught?

[Peter Chapin <PChapin@vtc.vsc.edu>]

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