generic
	type Item is private;
	Default_Value: in Item;
	--Capacity: in Positive := 5;

package Stacks is

	Capacity: constant := 5;

	type Stack is limited private; -- with Invariant => Capacity >= Size(Stack);

   	procedure Empty( S: out Stack ) with
   		Post => Size(S) = 0;

	function Size( S: Stack ) return Natural;

	procedure Push( S: in out Stack; I: in Item ) with
		Pre  => Size(S) < Capacity,
		Post => Size(S) = Size(S)'Old + 1 and Top(S) = I;

	procedure Pop( S: in out Stack ) with
		Pre  => Size(S) > 0 and Size(S) <= Capacity,
		Post => Size(S) = Size(S)'Old - 1;

	function Top( S: Stack ) return Item with
		Pre => Size(S) > 0 and Size(S) <= Capacity;

private

	type Item_Array is array( Positive range 1..Capacity ) of Item;

	type Stack is limited record
		Size: Natural;
		Data: Item_Array;
   		end record;

	function Size( S: Stack ) return Natural is (S.Size);

	function Top( S: Stack ) return Item is (S.Data(Size(S)));

end Stacks;