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,af40877501f46910
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news1.google.com!news1.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newsfeed.news.ucla.edu!usenet.stanford.edu!newsfeed.berkeley.edu!ucberkeley!newsgate.cuhk.edu.hk!news.netfront.net!not-for-mail
From: Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org>
Newsgroups: comp.lang.ada
Subject: Re: SPARK understand me very well... me neither
Date: Sat, 14 Aug 2010 14:50:08 -0700
Organization: Netfront http://www.netfront.net/
Message-ID: <i4732h$2let$1@adenine.netfront.net>
References: <op.vhd7rsl2ule2fv@garhos> <op.vhev1mcoule2fv@garhos>
 <2308d0a0-8fdb-41a0-b2dc-6b30a2bf2f18@v41g2000yqv.googlegroups.com>
 <op.vhfsrxj6xmjfy8@garhos>
 <fd3450c4-e218-467c-b531-69a3f927681a@i31g2000yqm.googlegroups.com>
 <op.vhf32fahule2fv@garhos>
NNTP-Posting-Host: 69.96.199.61
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
X-Trace: adenine.netfront.net 1281822610 87517 69.96.199.61 (14 Aug 2010
 21:50:10 GMT)
X-Complaints-To: news@netfront.net
NNTP-Posting-Date: Sat, 14 Aug 2010 21:50:10 +0000 (UTC)
User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US;
 rv:1.9.1.11) Gecko/20100713 Thunderbird/3.0.6
In-Reply-To: <op.vhf32fahule2fv@garhos>
Xref: g2news1.google.com comp.lang.ada:13306
Date: 2010-08-14T14:50:08-07:00
List-Id: <comp.lang.ada>

On 08/14/2010 01:48 PM, Yannick Duchêne (Hibou57) wrote:
> Le Sat, 14 Aug 2010 21:08:43 +0200, Phil Thornley
>>> > For this particular example, I don't understand why you haven't used
>>> > the obvious precondition:
>>> > --# pre A * B in Integer;
>
> But what seems important to me and I would to underline, was also that
> if I did not knew this was possible, this was because it was fr from my
> mind. And this was far from my mind, because looking at it as-is, I
> would have said “what does it prove ? what does it offer ?”. In short,
> this looks like a bad logical interface to me.

It doesn't prove anything, and it's not supposed to. It's a precondition. It 
says, "This precondition must be true for this operation to give correct 
results." It is the caller's duty to meet the precondition.

-- 
Jeff Carter
"To Err is human, to really screw up, you need C++!"
Stéphane Richard
63

--- news://freenews.netfront.net/ - complaints: news@netfront.net ---