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

<PRE>
ChoiceBag (E, C): <b>trait</b>
  % A bag with a weakly-specified choose operator
  <b>includes</b> <A HREF="Bag.html">Bag</A>
  <b>introduces</b>
    choose: C -&gt; E
    rest: C -&gt; C
    isEmpty: C -&gt; Bool
  <b>asserts</b> <b>forall</b> e, e1: E, b: C
    b \neq {} =&gt; choose(b) \in b;
    b \neq {} =&gt; rest(b) = delete(choose(b), b);
    isEmpty(b) == b = {}
  <b>implies</b>
    <A HREF="Container.html">Container</A> (choose <b>for</b> head, rest <b>for</b> tail,
               {} <b>for</b> empty)
    C <b>partitioned</b> <b>by</b> choose, rest, isEmpty
    <b>forall</b> e: E, b: C
      b \neq {} =&gt; b = insert(choose(b), rest(b))
</PRE>

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