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

<PRE>
Deque (E, C): <b>trait</b>
  % Double ended queue operators
  <b>includes</b> <A HREF="Integer.html">Integer</A>
  <b>introduces</b>
    empty: -&gt; C
    __ \precat __: E, C -&gt; C
    __ \postcat __: C, E -&gt; C
    count: E, C -&gt; Int
    __ \in __: E, C -&gt; Bool
    head, last: C -&gt; E
    tail, init: C -&gt; C
    len: C -&gt; Int
    isEmpty: C -&gt; Bool
  <b>asserts</b>
    C <b>generated</b> <b>by</b> empty, \postcat
    <b>forall</b> e, e1, e2: E, d: C
      count(e, empty) == 0;
      count(e, e1 \precat d) ==
        count(e, d) + (<b>if</b> e = e1 <b>then</b> 1 <b>else</b> 0);
      e \in d == count(e, d) &gt; 0;
      e \precat empty == empty \postcat e;
      (e1 \precat d) \postcat e2 == e1 \precat (d \postcat e2);
      head(e \precat d) == e;
      last(d \postcat e) == e;
      tail(e \precat d) == d;
      init(d \postcat e) == d;
      len(empty) == 0;
      len(d \postcat e) == len(d) + 1;
      isEmpty(d) == d = empty
  <b>implies</b>
    <A HREF="Stack.html">Stack</A> (head <b>for</b> top, tail <b>for</b> pop,
           \precat <b>for</b> push, len <b>for</b> size),
    <A HREF="Queue.html">Queue</A> (\precat <b>for</b> append, last <b>for</b> head, 
           init <b>for</b> tail)
    C <b>generated</b> <b>by</b> empty, \precat
    C <b>partitioned</b> <b>by</b> len, head, tail
    C <b>partitioned</b> <b>by</b> len, last, init
    <b>forall</b> d: C
      d \neq empty
        =&gt; (head(d) \precat tail(d) = d
            /\ init(d) \postcat last(d) = d)
    <b>converts</b> head, last, tail, init, len
      exempting head(empty), last(empty),
        tail(empty), init(empty)
</PRE>

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