STACK AS AN ADT

A stack is an ordered collection of items of items into which new items may be inserted and from which items may be removed at one end called the top of stack. The representation of a stack as an abstract data type is straight forward. We use eltype to denote the type of the stack element and parameterize the stack data type with Eltype :
Abstract typedef<> STACK(eltype)
abstract empty(s)
STACK(eltype) s;
Post condition empty = = ( len(s)= =0);

abstract eltype pop(s)
STACK(eltype)s;
pre condition empty(s) = =FALSE;
post condition pop = = first(s)
s= = sub(s,1,len(s)-1);

abstract push(s,elt)
STACK(s,elt)
eltype elt;
post condition s = = +s;