[<A HREF="StackBasics.ps">PostScript</A>]

<PRE>
StackBasics (E, C): <b>trait</b>
  % Essential LIFO operators
  <b>includes</b> <A HREF="Integer.html">Integer</A>
  <b>introduces</b>
    empty: -&gt; C 
    push: E, C -&gt; C
    top: C -&gt; E
    pop: C -&gt; C
  <b>asserts</b>
    C <b>generated</b> <b>by</b> empty, push
    <b>forall</b> e: E, stk: C
      top(push(e, stk)) == e;
      pop(push(e, stk)) == stk;
  <b>implies</b> <b>converts</b> top, pop
    exempting top(empty), pop(empty)
</PRE>

[<A HREF="toc.html">Table of Contents</A>] [<A HREF="index.html">Index</A>]