[PostScript]
BagBasics (E, C): trait
  % Essential bag operators
  includes Integer
  introduces
    {}: -> C
    insert: E, C -> C
    count: E, C -> Int
  asserts
    C generated by {}, insert
    C partitioned by count
    forall b: C, e, e1, e2: E
      count(e, {}) == 0;
      count(e1, insert(e2, b)) ==
        count(e1, b) + (if e1 = e2 then 1 else 0)
  implies
    InsertGenerated ({} for empty)
    forall e: E, b: C
      insert(e, b) \neq {};
      count(e, b) >= 0
    converts count
[Table of Contents] [Index]