From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.66.66.196 with SMTP id h4mr16348981pat.22.1407612092879;
        Sat, 09 Aug 2014 12:21:32 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.glorb.com!h18no10808312igc.0!news-out.google.com!b3ni23560qac.1!nntp.google.com!Xl.tags.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sat, 09 Aug 2014 14:21:32 -0500
Date: Sat, 09 Aug 2014 15:21:31 -0400
From: Peter Chapin <PChapin@vtc.vsc.edu>
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64;
 rv:31.0) Gecko/20100101 Thunderbird/31.0
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Preconditions which anyway would be caught?
References: <ls5f3l$4t8$1@speranza.aioe.org>
In-Reply-To: <ls5f3l$4t8$1@speranza.aioe.org>
Message-ID: <7vydnShDldsh6XvO4p2dnAA@giganews.com>
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-In7UkmZEs52cfHwR+kPFstAyWCy4FVUPxL9CD+O7fHMRoSFWrlc76xETO9FpaYO/AjnutLfrMY4yVLC!nBvvchzr7yH5IdDwAz1r8u+q84PWOkTFJKqwEDN76FZ1h0dZKFhVjzC53AhHcvc=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint
 properly
X-Postfilter: 1.3.40
X-Original-Bytes: 2663
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 7bit
Xref: news.eternal-september.org comp.lang.ada:21625
Date: 2014-08-09T15:21:31-04:00
List-Id: <comp.lang.ada>

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