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

<PRE>
BagBasics (E, C): <b>trait</b>
  % Essential bag operators
  <b>includes</b> <A HREF="Integer.html">Integer</A>
  <b>introduces</b>
    {}: -&gt; C
    insert: E, C -&gt; C
    count: E, C -&gt; Int
  <b>asserts</b>
    C <b>generated</b> <b>by</b> {}, insert
    C <b>partitioned</b> <b>by</b> count
    <b>forall</b> b: C, e, e1, e2: E
      count(e, {}) == 0;
      count(e1, insert(e2, b)) ==
        count(e1, b) + (<b>if</b> e1 = e2 <b>then</b> 1 <b>else</b> 0)
  <b>implies</b>
    <A HREF="InsertGenerated.html">InsertGenerated</A> ({} <b>for</b> empty)
    <b>forall</b> e: E, b: C
      insert(e, b) \neq {};
      count(e, b) &gt;= 0
    <b>converts</b> count
</PRE>

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