Re: subtypes and preconditions

["Jeffrey R. Carter" <spam.not.jrcarter@acm.not.spam.org>]

Peter Amey wrote:
> 
> 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.

Right. The 2 forms are equivalent when doing proofs. Yet I keep seeing examples 
that use preconditions rather than subtypes. For example, Barnes (2003) gives 
the example of Divide (p 70):

procedure Divide (M, N : in Integer; Q, R : out Integer);
--# derives Q, R from M, N;
--# pre (M >= 0) and (N > 0);
--# post (M = Q * N + R) and (R < N) and (R >= 0);

rather than

procedure Divide (Dividend : in  Natural; Divisor   : in  Positive;
                   Quotient : out Natural; Remainder : out Natural);
--# derives Quotient, Remainder from Dividend, Divisor;
--# post Dividend = Quotient * Divisor + Remainder and Remainder < Divisor;

The "R >= 0" in the assertion also becomes unnecessary with appropriate subtypes.

Similarly, he has (pp 77-78)

procedure GCD (M, N : in Integer; G : out Integer);
--# derives G from M, N;
--# pre M >= 0 and N > 0
--# post G > 0 and (M rem G = 0) and (N rem G = 0);

rather than

procedure GCD (M : in Natural; N : in Positive; G : out Positive);
--# derives G from M, N;
--# post M rem G = 0 and N rem G = 0;

-- 
Jeff Carter
"You empty-headed animal-food-trough wiper."
Monty Python & the Holy Grail
04