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,UTF8
Received: by 10.68.0.170 with SMTP id 10mr3856301pbf.2.1322045724557;
        Wed, 23 Nov 2011 02:55:24 -0800 (PST)
Path: 
 lh20ni8725pbb.0!nntp.google.com!news1.google.com!volia.net!news2.volia.net!feed-A.news.volia.net!news.musoftware.de!wum.musoftware.de!weretis.net!feeder4.news.weretis.net!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Wed, 23 Nov 2011 11:55:23 +0100
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6;
 rv:7.0.1) Gecko/20110929 Thunderbird/7.0.1
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>
 <wcc4nxzu5gf.fsf@shell01.TheWorld.com>
 <4295dc09-43de-4557-a095-fc108359f27f@y42g2000yqh.googlegroups.com>
 <fe29npj98k5s$.1vzwcva8q22hk.dlg@40tude.net>
 <a5d7119f-7bb7-41e4-8d76-ef08f2d958d9@g7g2000vbd.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>
 <op.v5drk4egule2fv@douda-yannick>
 <4eccb3d3$0$6627$9b4e6d93@newsspool2.arcor-online.net>
 <op.v5d718mfule2fv@douda-yannick>
In-Reply-To: <op.v5d718mfule2fv@douda-yannick>
Message-ID: <4eccd11b$0$6629$9b4e6d93@newsspool2.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 23 Nov 2011 11:55:23 CET
NNTP-Posting-Host: a216cc39.newsspool2.arcor-online.net
X-Trace: 
 DXC=_W>Ka[X2aLj]BlmkiiU@BiA9EHlD;3Ycb4Fo<]lROoRa8kF<OcfhCOk8V6?4Fa=5gkPCY\c7>ejVh1:G4`DH3cXljK=KKC><5eg
X-Complaints-To: usenet-abuse@arcor.de
Xref: news1.google.com comp.lang.ada:19076
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Date: 2011-11-23T11:55:23+01:00
List-Id: <comp.lang.ada>

On 23.11.11 10:45, Yannick Duchêne (Hibou57) wrote:
> Le Wed, 23 Nov 2011 09:50:26 +0100, Georg Bauhaus <rm.dash-bauhaus@futureapps.de> a écrit:
>> `put`, in DbC, may fail when it tries to establish
>> the state of variables so that the postcondition is
>> true, for example, because of a hardware error.
>> Can this be attributed to an incomplete precondition,
>> though?
> Obviously not, but an incomplete pre-condition (lack of `not D.has (x)` in the Pre or lack in the Post of an `old D.has (x)` associated with the count), is not an hardware error. Cannot compare things of different nature.
>
> But don't bother, just noticed it because it was funny, no need to discuss this detail in deep, this would offer no meaningful value to the topic.
>

This is the best opportunity for some detail:
The precondition does not mention "not has(x)".
The dictionary may well have an entry for x,
but you can still add it and the postcondition
will be true:

    #Name    #Age
    Miller   56

d.put(x => 56, key => "Jones)

    #Name    #Age
    Miller   56
    Jones    56

In fact, `put` can replace Miller's age with another
Miller's age  and still the state is as pre/post say.
If `put` should not replace, this needs to be stated.
And then it should raise an exception.  Just like
Ada's containers do, except that DbC exceptions typically
have more information about what went wrong.