with Ada.Containers.Vectors;
generic
   Size : Integer;
   type Elem is private;

   with procedure Print (E : in Elem);

package Stack is
   type Stack is tagged limited private;

   subtype Count_Type is Integer range 0 .. Size;
   subtype Index_Type is Count_Type range 1 .. Size;
   package Stack_Vectors is new Ada.Containers.Vectors
     (Index_Type   => Index_Type,
      Element_Type => Elem);

   -- Use of precondition ( only available in ada 2012 )
   -- Add an element in the stack
   procedure Push (This : in out Stack; E : in Elem) with
      Pre => not This.Is_Full;

   -- Use of precondition ( only available in ada 2012 )
   -- Retrieve an element in the stack
   function Pop (This : in out Stack) return Elem with
      Pre => not This.Is_Empty;

   -- Use of precondition ( only available in ada 2012 )
   -- Retrieve an element in the stack
   procedure Pop (This : in out Stack; E : out Elem) with
      Pre => not This.Is_Empty;

   -- Use of precondition ( only available in ada 2012 )
   -- Retrieve an element in the stack
   procedure Pop (This : in out Stack) with
      Pre => not This.Is_Empty;

   -- Use of precondition ( only available in ada 2012 )
   -- Retrieve one or more element in the stack until E is Found
   procedure Pop_Until (This : in out Stack; E : in Elem) with
      Pre => not This.Is_Empty;
   procedure Print_All (This : in Stack);
   function Length (This : in Stack) return Count_Type;
   function Is_Full (This : in out Stack) return Boolean;
   function Is_Empty (This : in out Stack) return Boolean;

private
   type Stack is tagged limited record
      Len : Count_Type := 0;
      V   : Stack_Vectors.Vector;
   end record;
end Stack;