; ---------- SORTS --------------------

TYPE
   X = STR;
   Stack = X-list;
ENDTYPE


; ---------- STATE --------------------
STATE  S : Stack;


; ---------- FUNCTIONS ----------------

FUNC push(x:X,s:Stack):Stack
RETURN cons(x,s);
  
FUNC top(s:Stack):X
PRE s != <>
RETURN head(s);

FUNC pop(s:Stack):Stack
PRE s != <>
RETURN tail(s);


; ---------- EVENTS -------------------

FUNC INIT():
STATE S <- <>;
  
FUNC PUSH(x:X):
STATE S <- push(x,S);
  
FUNC POP():X 
PRE  S != <>
RETURN head(S)
STATE S <- tail(S);
  
FUNC TOP():X
PRE  S != <>
RETURN head(S);