generic
	type Item is private;

package Stacks is

	type Stack( Capacity: Positive ) is tagged limited private with
		Invariant => Size(Stack) <= Stack.Capacity;

	function Size( S: Stack ) return Natural;

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

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

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

private

	type Item_Array is array( Positive range <> ) of Item;

	type Stack( Capacity: Positive ) is tagged limited record
		Size: Natural := 0;
		Data: Item_Array(1..Capacity);
		end record;

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

end Stacks;