subtypes and preconditions (was: subtype of enumeration type)

[Peter Amey <peter.amey@praxis-cs.co.uk>]

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