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!news2.google.com!news4.google.com!news.glorb.com!newsfeeder.wxs.nl!newsfeed01.sul.t-online.de!t-online.de!newsfeed.arcor.de!news.arcor.de!not-for-mail
Date: Tue, 21 Mar 2006 20:00:01 +0100
From: Georg Bauhaus <bauhaus@futureapps.de>
Organization: future apps GmbH
User-Agent: Debian Thunderbird 1.0.2 (X11/20051002)
X-Accept-Language: en-us, en
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: subtypes and preconditions
References: <dvmas1$kj8$1@sunnews.cern.ch> <skFTf.835639$x96.281917@attbi_s72>
 <489s9rFhkfqdU1@individual.net> <eWWTf.876049$xm3.694350@attbi_s21>
In-Reply-To: <eWWTf.876049$xm3.694350@attbi_s21>
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Message-ID: <44204d2a$0$7753$9b4e6d93@newsread4.arcor-online.net>
NNTP-Posting-Date: 21 Mar 2006 19:59:54 MET
NNTP-Posting-Host: b2efb803.newsread4.arcor-online.net
X-Trace: 
 DXC==CW@P8\G24[\6[GEd:nl>[:ejgIfPPldTjW\KbG]kaMXeDdmR4DE3R\Ya76CUZ3K4UljUVjRQ60?RVmnOeiOY3@^g[50F7T5IOR
X-Complaints-To: usenet-abuse@arcor.de
Xref: g2news1.google.com comp.lang.ada:3527
Date: 2006-03-21T19:59:54+01:00
List-Id: <comp.lang.ada>

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