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;