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,5e53057e86953953
X-Google-Attributes: gid103376,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news2.google.com!news.glorb.com!feeder.erje.net!newsfeed-fusi2.netcologne.de!newsreader2.netcologne.de!news.netcologne.de!newsfeed-hp2.netcologne.de!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Tue, 17 Jun 2008 12:39:35 +0200
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Thunderbird 2.0.0.14 (Macintosh/20080421)
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Question on initialization of packages
References: <y4adnXtddsFN7crV4p2dnAA@telenor.com>
 <1pok6brk3yyxf$.ct5gwnf4g97p$.dlg@40tude.net>
 <KredncLZKqYOHcrVRVnzvQA@telenor.com>
In-Reply-To: <KredncLZKqYOHcrVRVnzvQA@telenor.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <48579467$0$7538$9b4e6d93@newsspool1.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 17 Jun 2008 12:39:35 CEST
NNTP-Posting-Host: 5cf6704b.newsspool1.arcor-online.net
X-Trace: 
 DXC=n`F9niQeADoJ00P1S40fZgic==]BZ:afn4Fo<]lROoRa<`=YMgDjhgbO54QL<l^?C`nc\616M64>jLh>_cHTX3jm0AaaZ5[>29k
X-Complaints-To: usenet-abuse@arcor.de
Xref: g2news1.google.com comp.lang.ada:738
Date: 2008-06-17T12:39:35+02:00
List-Id: <comp.lang.ada>

Reinert Korsnes schrieb:
> Dmitry A. Kazakov wrote:

>>> Question: How can I be sure that "Send_Stack" is empty
>>> at the start of the program execution ?
>> Hmm, "sure" in which sense? To make it visible for the reader? To specify
>> in the contract of Stack that it is initially empty?
> 
> Yes, yes, to make it visible for the reader.

In any case, users can be enabled to ask whether or not the stack is
empty, as I'm sure you know. In the generic stack package,

   type Stack is ...;
   function Is_Empty(The_Stack: Stack) return Boolean;

Then, since we now have pragma Postcondition,
you could make the Stack controlled, override Initialize
and state the postcondition of being empty after initialization:

   type Stack is new Limited_Controlled with private;

   overriding
   procedure Initialize(Object: in out Stack);
   pragma Postcondition(Initialize, Is_Empty(Object));