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=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,e58bb9b46b60f0fb
X-Google-Attributes: gid103376,public
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news3.google.com!news2.google.com!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail
From: Peter Amey <peter.amey@praxis-cs.co.uk>
Newsgroups: comp.lang.ada
Subject: subtypes and preconditions (was: subtype of enumeration type)
Date: Tue, 21 Mar 2006 08:37:15 +0000
Message-ID: <489s9rFhkfqdU1@individual.net>
References: <dvmas1$kj8$1@sunnews.cern.ch> <skFTf.835639$x96.281917@attbi_s72>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit
X-Trace: individual.net 8aROBBl0tU9774JqEx6qHQCPE8jAcLTpeAjisP8bf0Glr+M0E=
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US;
 rv:1.4) Gecko/20030624 Netscape/7.1 (ax)
X-Accept-Language: en-us, en
In-Reply-To: <skFTf.835639$x96.281917@attbi_s72>
Xref: g2news1.google.com comp.lang.ada:3517
Date: 2006-03-21T08:37:15+00:00
List-Id: <comp.lang.ada>

Jeff,

Jeffrey R. Carter wrote:
[snip]
> However, using subtypes is cleaner. I much prefer
> 
> function F (A : Natural);
> 
> to
> 
> function F (A : Integer);
> --# pre A >= 0;
> 
> which is often seen in SPARK.
> 

I strongly agree.  Thoughtful use of subtypes is one of the most useful 
things to do in SPARK programs, it greatly assists with exception 
freedom proofs.

I suspect the latter form of your function arises because, many years 
ago, the SPARK Examiner did not carry type information into verification 
conditions.  In those far-off days it wouldn't have known that A was >= 
0 even if the subype Natural was given.  Since about the mid 90s the 
Examiner makes full use of all the information deducible from type and 
subtype ranges.

[snip]

Peter