ChoiceBag (E, C): trait
  % A bag with a weakly-specified choose operator
  includes Bag
    choose: C -> E
    rest: C -> C
    isEmpty: C -> Bool
  asserts forall e, e1: E, b: C
    b \neq {} => choose(b) \in b;
    b \neq {} => rest(b) = delete(choose(b), b);
    isEmpty(b) == b = {}
    Container (choose for head, rest for tail,
               {} for empty)
    C partitioned by choose, rest, isEmpty
    forall e: E, b: C
      b \neq {} => b = insert(choose(b), rest(b))
[Table of Contents] [Index]