generic
type Item is private;
Default_Value: in Item;
package Stacks is
Capacity: constant := 5;
type Stack is limited private;
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;