generic
	type Item is private;
package Stacks is

	type Stack( Capacity: Positive ) is tagged limited private;

	function Size( S: Stack ) return Natural;

	procedure Empty( S: in out Stack );

	procedure Push( S: in out Stack; I: in Item );
	pragma Precondition( Size(S) < S.Capacity );
	pragma Postcondition( Size(S) > 0 and Top(S) = I );

	procedure Pop( S: in out Stack );
	pragma Precondition( Size(S) > 0 );
	pragma Postcondition( Size(S) < S.Capacity );

	function Top( S: Stack ) return Item;
	pragma Precondition( 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;

end Stacks;