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

<PRE>
Stack (E, C): <b>trait</b>
  % Common LIFO operators
  <b>includes</b> <A HREF="StackBasics.html">StackBasics</A>, <A HREF="Integer.html">Integer</A>
  <b>introduces</b>
    count: E, C -&gt; Int
    __ \in __: E, C -&gt; Bool
    size: C -&gt; Int
    isEmpty: C -&gt; Bool
  <b>asserts</b>
    <b>forall</b> e: E, stk: C
      size(empty) == 0;
      size(push(e, stk)) == size(stk) + 1;
      isEmpty(stk) == stk = empty
  <b>implies</b> 
    <A HREF="Container.html">Container</A> (push <b>for</b> insert, top <b>for</b> head,
               pop <b>for</b> tail)
    C <b>partitioned</b> <b>by</b> top, pop, isEmpty
    <b>forall</b> stk: C
      size(stk) &gt;= 0
    <b>converts</b> top, pop, count, \in, size, isEmpty
      exempting top(empty), pop(empty)
</PRE>

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