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.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC 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.204.151.133 with SMTP id c5mr974295bkw.8.1322140479198;
        Thu, 24 Nov 2011 05:14:39 -0800 (PST)
Path: 
 dq5ni46095bkb.0!nntp.google.com!news1.google.com!volia.net!news2.volia.net!feed-A.news.volia.net!news.musoftware.de!wum.musoftware.de!de-l.enfer-du-nord.net!feeder1.enfer-du-nord.net!gegeweb.org!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: Generic-Package Elaboration Question / Possible GNAT Bug.
Date: Thu, 24 Nov 2011 14:14:17 +0100
Organization: cbb software GmbH
Message-ID: <8x9yu4nouq37.16b919ashpomb$.dlg@40tude.net>
References: 
 <7bf9bc32-850a-40c6-9ae2-5254fe220533@f29g2000yqa.googlegroups.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> <jah2np$7fp$1@munin.nbi.dk>
 <1ecuhb030iugz.4q1hfjx371xa.dlg@40tude.net>
 <4ecc393d$0$7625$9b4e6d93@newsspool1.arcor-online.net>
 <124aq618dmove.884jj64mzm6w$.dlg@40tude.net> <m2mxbn89qz.fsf@pushface.org>
 <1jxx617mf2cqf$.1j076axdq83mr$.dlg@40tude.net> <m2d3ci98l4.fsf@pushface.org>
 <1cjufyo57vlpg$.11kf45cs5vnb7.dlg@40tude.net> <m28vn67xke.fsf@pushface.org>
 <chddc4qlhlcy.1qfrvu7yd7hoa.dlg@40tude.net>
 <4ece213a$0$6629$9b4e6d93@newsspool2.arcor-online.net>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.user.speranza.aioe.org
Mime-Version: 1.0
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Xref: news1.google.com comp.lang.ada:19116
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Date: 2011-11-24T14:14:17+01:00
List-Id: <comp.lang.ada>

On Thu, 24 Nov 2011 11:49:30 +0100, Georg Bauhaus wrote:

> On 24.11.11 10:27, Dmitry A. Kazakov wrote:

>> If correctness cannot be proved
>> statically, then the requirement expressed by the precondition must be
>> considered as not satisfied.
> 
> We may state our assumptions and have them checked,

There is no such thing as assumption, there are only conditions for
whatever outcome of which, the program's behavior must be defined.

> Like when showing that for a stack object, the sequence
> (not Is_Full, Push, Pop) is a safe sequence,

It is not safe:

1. finalization and initialization may fail in Ada. The contracts of
element and index types propagate into the contracts of the container.

2. immutable stack has one Is_Full.

And it is the behavior, not the contract. The contract might imply behavior
(safety of this sequence under certain conditions), when provable. If not
provable, adding dynamic checks in all possible places trying Push and Pop
would be pointless. Not proven means: expect any outcome (any = anything
not excluded by a proof).

It is also pointless to use undecidable propositions for static proofs
(which is basically the idea behind dynamic checks). Garbage in, garbage
out.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de