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.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,ea5071f634c2ea8b
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.36.6 with SMTP id m6mr7819785pbj.4.1322134252885;
        Thu, 24 Nov 2011 03:30:52 -0800 (PST)
Path: 
 lh20ni12551pbb.0!nntp.google.com!news2.google.com!news3.google.com!feeder2.cambriumusenet.nl!feed.tweaknews.nl!62.179.104.142.MISMATCH!amsnews11.chello.com!eweka.nl!lightspeed.eweka.nl!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Thu, 24 Nov 2011 12:30:46 +0100
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6;
 rv:8.0) Gecko/20111105 Thunderbird/8.0
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Generic-Package Elaboration Question / Possible GNAT Bug.
References: 
 <7bf9bc32-850a-40c6-9ae2-5254fe220533@f29g2000yqa.googlegroups.com>
 <3snehoqgs8ia$.1nobjem6g6hx6$.dlg@40tude.net>
 <wcc1ut14o97.fsf@shell01.TheWorld.com>
 <128rdz2581345$.c4td19l7qp9z$.dlg@40tude.net> <jaecvt$4tp$1@dont-email.me>
 <16ipwvpdavifr$.17bxf7if7f6kh$.dlg@40tude.net>
 <4ecb78b1$0$6643$9b4e6d93@newsspool2.arcor-online.net>
 <1iofgbqznsviu$.phvidtvxlyj4$.dlg@40tude.net>
 <4ecbb96e$0$6581$9b4e6d93@newsspool3.arcor-online.net>
 <vagow98uvk3n$.198v2ms719j4e$.dlg@40tude.net>
 <4ecbdfdb$0$6629$9b4e6d93@newsspool2.arcor-online.net>
 <12hfiflyf7pr5$.l3pkpgoid8xt$.dlg@40tude.net>
 <4ecc35b8$0$7628$9b4e6d93@newsspool1.arcor-online.net>
 <x5dznkeses66.wzuo5z8f8gkd.dlg@40tude.net>
 <4eccd5d2$0$6637$9b4e6d93@newsspool2.arcor-online.net>
 <14p8llstxrtci$.18hb93fkpteuv$.dlg@40tude.net>
 <4ecd0652$0$6582$9b4e6d93@newsspool3.arcor-online.net>
 <1wyybnjde2yxq.1w37r5182t0xt.dlg@40tude.net>
 <4ecd9faf$0$6627$9b4e6d93@newsspool2.arcor-online.net>
 <1tpgi2c1lci4l.1lvazzk0xb93j.dlg@40tude.net>
In-Reply-To: <1tpgi2c1lci4l.1lvazzk0xb93j.dlg@40tude.net>
Message-ID: <4ece2aeb$0$6639$9b4e6d93@newsspool2.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 24 Nov 2011 12:30:51 CET
NNTP-Posting-Host: b607871a.newsspool2.arcor-online.net
X-Trace: 
 DXC=W^QH_eUfB]d^Y=RbYBPl4`A9EHlD;3Ycb4Fo<]lROoRa8kF<OcfhCOk_2XE;UOVIGoPCY\c7>ejVhlBkIO^noWbcLU=gIblI_2i
X-Complaints-To: usenet-abuse@arcor.de
Xref: news2.google.com comp.lang.ada:14599
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Date: 2011-11-24T12:30:51+01:00
List-Id: <comp.lang.ada>

On 24.11.11 11:52, Dmitry A. Kazakov wrote:

>> The typical example is a stack and its contract referring to
>> values available at runtime: from the contract, I learn that a stack
>> is initially empty and has a certain capacity.
>
> What is dynamic there?

Its initial capacity, as outlined in another post.
One may continue with current_number_of_items and such.

> It is not a precondition, sqrt (-1.0) is *defined* as Argument_Error
> propagation. I.e. the postcondition includes Argument_Error. The
> precondition is "X in Float."

As a precondition for { Sqrt'Result in Float_Type'Base } the LRM states
{ X in Float_Type'Base and X >= 0.0 }. The precondition of Sqrt in
some language that defines Argument_Error in Float_Type'Base is different.
Not wrong, possibly desirable, but different.


> A plane without fuel would crash regardless your ability to determine the
> level kerosene in its tanks.

Yes, but we do not know before fly-time whether or not there
is going to be enough fuel in the tanks. Flying loops consuming more,
hardware errors caused by people shooting at wings, etc., will not
stop the plane designers to state, using arithmetic expressions,
how much fuel it takes (precondition) to fly from A to B.