Re: Question on initialization of packages

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));