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

<PRE>
Container (E, C): <b>trait</b>
  % head and tail enumerate contents of a C
  <b>includes</b> <A HREF="InsertGenerated.html">InsertGenerated</A>, <A HREF="Integer.html">Integer</A>
  <b>introduces</b>
    isEmpty: C -&gt; Bool
    count: E, C -&gt; Int
    __ \in __: E, C -&gt; Bool
    head: C -&gt; E
    tail: C -&gt; C
  <b>asserts</b> 
    C <b>partitioned</b> <b>by</b> isEmpty, head, tail
    <b>forall</b> e, e1: E, c: C
      isEmpty(empty);
      ~isEmpty(insert(e, c));
      count(e, empty) == 0;
      count(e, insert(e1, c)) ==
        count(e, c) + (<b>if</b> e = e1 <b>then</b> 1 <b>else</b> 0);
      e \in c == count(e, c) &gt; 0;
      ~isEmpty(c) =&gt;
        count(e, insert(head(c), tail(c)))
          = count(e, c)
  <b>implies</b>
    <b>forall</b> c: C
      ~isEmpty(c) =&gt; count(head(c), c) &gt; 0;
    <b>converts</b> isEmpty, count, \in
</PRE>

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