-- This is the specification for an integer stack abstract data type.

pragma ada_2012;
package IntStackPkg is

	type StackType is limited private;

	Stack_Is_Empty, Stack_Is_Full : Exception;

	function IsEmpty (S : StackType) return Boolean;
	function IsFull  (S : StackType) return Boolean;

	procedure Push (I : Integer; S : in out StackType)
    with pre => not isfull(s);

	procedure Pop  (S : in out StackType)
    with pre => not isempty(s);

	function  Top  (S : StackType) return Integer
    with pre => not isempty(s);

private
	MaxSize : Constant Integer := 1000;

	type ElementArray is array(1 .. MaxSize) of Integer;

	type StackType is record
		Elements : ElementArray;
		TheTop : Integer := 0;
	end record;

end IntStackPkg;