MODEL  stack

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

   STATE  S : Stack;

   FUNC INIT():
   STATE S <- <>;

   FUNC PUSH(x:X):
   STATE S <-  <x:S>;

   FUNC POP():X
   PRE      S != <>
   RETURNS  hd(S)
   STATE    S <- tl(S);

   FUNC TOP():X
   PRE      S != <>
   RETURNS  hd(S);

  ENDMODEL