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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,af40877501f46910
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news1.google.com!postnews.google.com!i31g2000yqm.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK understand me very well... me neither
Date: Sat, 14 Aug 2010 12:08:43 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <fd3450c4-e218-467c-b531-69a3f927681a@i31g2000yqm.googlegroups.com>
References: <op.vhd7rsl2ule2fv@garhos> <op.vhev1mcoule2fv@garhos>
 <2308d0a0-8fdb-41a0-b2dc-6b30a2bf2f18@v41g2000yqv.googlegroups.com>
 <op.vhfsrxj6xmjfy8@garhos>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1281812924 13575 127.0.0.1 (14 Aug 2010 19:08:44
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Sat, 14 Aug 2010 19:08:44 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: i31g2000yqm.googlegroups.com; posting-host=80.177.171.182;
 posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
 Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
 3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:13295
Date: 2010-08-14T12:08:43-07:00
List-Id: <comp.lang.ada>

On 14 Aug, 17:44, Yannick Duch=EAne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> Le Sat, 14 Aug 2010 18:04:23 +0200, Phil Thornley =A0
> <phil.jpthorn...@gmail.com> a =E9crit:
[...]
> > For this particular example, I don't understand why you haven't used
> > the obvious precondition:
> > --# pre A * B in Integer;
>
> Because I did not knew this was feasible.
OK - that seems a pretty good reason :-)

[...]
> > In a well-designed program, the subtype constraints should match the
> > usage of the variables of the subtypes
>
> Agree, except that I could not see a way to restrict here.

For a general purpose function such as this the author can't define
sensible subtypes for the individual inputs because the condition that
the function relies on is itself a function of both of the inputs.
That's why there has to be a precondition.  The job of the author is
always to come up with the weakest precondition that does the job.

For the Multiply function the weakest possible precondition is the
condition that Multiply requires - that the product of the two actual
parameters is a valid Integer.

[...]
> Hope you are not too much tired with my beginner's questions.
Not a problem - and it's one of the functions of c.l.a to provide a
forum for such questions.  (You'll know when I get tired of answering
because I'll stop :-)

Cheers,

Phil