[PostScript] 
ChoiceSet (E, C): trait
  % A set with a weakly-specified choose operator
  includes Set
  introduces
    choose: C -> E
    rest: C -> C
    isEmpty: C -> Bool
  asserts forall e, e1: E, s: C
    s \neq {} => choose(s) \in s;
    s \neq {} => rest(s) = delete(choose(s), s);
    isEmpty(s) == s = {}
  implies
    C partitioned by choose, rest, isEmpty
    forall e: E, s: C
      s \neq {} => s = insert(choose(s), rest(s))
[Table of Contents] [Index]