Re: subtypes and preconditions

[Georg Bauhaus <bauhaus@futureapps.de>]

Jeffrey R. Carter wrote:

> 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;

WRT  M: Natural  versus  M: Integer >= 0, I think that in an
introductory example to reasoning about SPARK programs it
might in fact be good to leave out Ada subtypes' implications.

The reason is that you needn't know about the niceties of Ada's
subtypes in order to understand that M being >= 0 is important.
IOW, you already know what M >= 0 means, but you do not yet know
what M: Natural implies, unless you already know Ada.

_And_ you have to assume that Natural has not been redefined.
Redifining 0 is a lot more difficult :-)



Georg