class Queue

  instance variables
    vals : seq of Tree`node := [];

  operations

    public
    Enqueue : Tree`node ==> ()
    Enqueue (x) ==
      vals := vals ^ [x];

    public
    Dequeue : () ==> Tree`node
    Dequeue () ==
      def x = hd vals
      in ( vals := tl vals;
           return x)
    pre not isEmpty();

    pure public
    isEmpty : () ==> bool
    isEmpty () == 
      return(vals = [])

end Queue