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

<PRE>
Queue (E, C): <b>trait</b>
  % FIFO operators
  <b>includes</b> <A HREF="Integer.html">Integer</A>
  <b>introduces</b> 
    empty: -&gt; C
    append: E, C -&gt; C
    count: E, C -&gt; Int
    __ \in __: E, C -&gt; Bool
    head: C -&gt; E
    tail: C -&gt; C
    len: C -&gt; Int
    isEmpty: C -&gt; Bool
  <b>asserts</b>
    C <b>generated</b> <b>by</b> empty, append
    <b>forall</b> q: C, e, e1: E
      count(e, empty) == 0;
      count(e, append(e1, q)) ==
        count(e, q) + (<b>if</b> e = e1 <b>then</b> 1 <b>else</b> 0);
      e \in q == count(e, q) &gt; 0;
      head(append(e, q)) ==
        <b>if</b> q = empty <b>then</b> e <b>else</b> head(q);
      tail(append(e, q)) ==
        <b>if</b> q = empty <b>then</b> empty
        <b>else</b> append(e, tail(q));
      len(empty) == 0;
      len(append(e, q)) == len(q) + 1;
      isEmpty(q) == q = empty
  <b>implies</b> 
    <A HREF="Container.html">Container</A> (append <b>for</b> insert)
    C <b>partitioned</b> <b>by</b> head, tail, isEmpty
    <b>forall</b> q: C
      len(q) &gt;= 0
    <b>converts</b> head, tail, len
      exempting head(empty), tail(empty)
</PRE>

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