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;