home *** CD-ROM | disk | FTP | other *** search
/ The C Users' Group Library 1994 August / wc-cdrom-cusersgrouplibrary-1994-08.iso / listings / v_08_07 / 8n07071b < prev    next >
Text File  |  1990-06-19  |  591b  |  34 lines
  1. \end{verbatim}
  2. Stack : (T:Type) -> Type is
  3. uses
  4.     Boolean
  5. ops
  6.     push : T -> nil
  7.     pre
  8.         isfull.not
  9.     post
  10.         isempty.not
  11.     done
  12.  
  13.     pop : nil -> T
  14.     pre
  15.         isempty.not
  16.     post
  17.         isfull.not
  18.     done
  19.  
  20.     isempty : nil -> Boolean
  21.  
  22.     isfull : nil -> Boolean
  23. const
  24.     s0 : Stack(T)
  25. eqn  # this is a comment
  26.     # push and pop are inverse to each other
  27.     'pop( 'push( s, x)) iseq (s, x) 
  28.     'push( 'pop( s)) iseq s
  29.     # there is a unique empty stack value
  30.     'isempty( s0) iseq TRUE
  31.     'isempty( s) => s iseq s0
  32. done
  33.  
  34.