note description: "Collections with membership multilicity" author: "JSO, Jackie Wang" date: "$Date$" revision: "$Revision$" class interface BAG [G -> attached ANY] create make_empty, make_from_array, make_from_tuple_array feature -- Constructor make_empty make_from_array (a: ARRAY [G]) ensure # Current = a.count make_from_tuple_array (a: ARRAY [TUPLE [g: G; i: INTEGER_32]]) require across a as cur all cur.item.i > 0 end feature -- Iteration cursor new_cursor: ITERATION_CURSOR [PAIR [G, INTEGER_32]] -- Fresh cursor associated with current structure feature -- Conversion as_function: FUN [G, INTEGER_32] -- Return current bag as a function from items -- to number of occurrences. ensure all_bag_items_covered: across Current as cur all Current [cur.item.first] = Result [cur.item.first] end only_bag_items_covered: across Result as cur all Current [cur.item.first] = Result [cur.item.first] end as_set: SET [G] -- Return the domain of curret bag ensure Result ~ as_function.domain as_array: ARRAY [G] -- Return current bag as an array of items. ensure current_bag_unchanged: Current ~ old Current.deep_twin same_count: Result.count = # Current feature -- Status queries count alias "#": INTEGER_32 ensure Result = as_array.count occurrences alias "[]" (g: G): INTEGER_32 assign override -- Number of 'g' in current bag. ensure non_negative_occurrences: Result >= 0 case_of_nonmember: not has (g) implies Result = 0 case_of_member: has (g) implies Result > 0 and Result = as_function [g] is_empty: BOOLEAN ensure Result = (# Current = 0) has (g: G): BOOLEAN ensure Result = as_array.has (g) Result = as_function.domain.has (g) Result = (Current [g] > 0) is_subbag_of alias "|<:" (other: like Current): BOOLEAN ensure Result = across as_function as cur all cur.item.second <= other [cur.item.first] end feature -- Commands override (i: INTEGER_32; g: G) -- Change quantity of 'g' to 'i' in current bag ensure Current ~ old Current.deep_twin.overriden (i, g) extend (g: G; i: INTEGER_32) -- Add 'g' of quantity 'i' into current bag. ensure Current ~ old Current.deep_twin.extended (g, i) extend_by (g: G) -- Add 'g' of quantity 1 into current bag. ensure Current ~ old Current.deep_twin.extended_by (g) union (other: like Current) -- Add 'other' into current bag. ensure Current ~ old Current.deep_twin.unioned (other) subtract (g: G; i: INTEGER_32) -- Subtract 'g' of quantity 'i' from current bag. require Current [g] >= i ensure Current ~ old Current.deep_twin.subtracted (g, i) subtract_by (g: G) -- Subtract 'g' of quantity 1 from current bag. require Current [g] >= 1 ensure Current ~ old Current.deep_twin.subtracted_by (g) difference (other: like Current) -- Subtract 'other' from current bag. require other |<: Current ensure Current ~ old Current.deep_twin.differenced (other) feature -- Specification Queries overriden (i: INTEGER_32; g: G): like Current -- Return a representation of current bag with -- quantity of 'g' to 'i' ensure current_bag_unchanged: Current ~ old Current.deep_twin across Result as cur all (cur.item.first ~ g implies Result [cur.item.first] = i) and (cur.item.first /~ g implies Result [cur.item.first] = Current [cur.item.first]) end extended (g: G; i: INTEGER_32): like Current -- Return a representation of current bag with -- 'g' of quantity 'i' added. ensure current_bag_unchanged: Current ~ old Current.deep_twin across Result as cur all (cur.item.first ~ g implies Result [cur.item.first] = Current [cur.item.first] + i) and (cur.item.first /~ g implies Result [cur.item.first] = Current [cur.item.first]) end extended_by alias "+" (g: G): like Current -- Return a representation of current bag with -- 'g' of quantity 1 added. ensure current_bag_unchanged: Current ~ old Current.deep_twin across Result as cur all (cur.item.first ~ g implies Result [cur.item.first] = Current [cur.item.first] + 1) and (cur.item.first /~ g implies Result [cur.item.first] = Current [cur.item.first]) end unioned alias "|\/|" (other: like Current): like Current -- Return a representation of current bag with -- 'other' added. ensure current_bag_unchanged: Current ~ old Current.deep_twin across Result as cur all (other.has (cur.item.first) implies Result [cur.item.first] = Current [cur.item.first] + other [cur.item.first]) and (not other.has (cur.item.first) implies Result [cur.item.first] = Current [cur.item.first]) end subtracted (g: G; i: INTEGER_32): like Current -- Return a representation of current bag with -- 'g' of quantity 'i' subtracted. require Current [g] >= i ensure current_bag_unchanged: Current ~ old Current.deep_twin across Result as cur all (cur.item.first ~ g implies Result [cur.item.first] = Current [cur.item.first] - i) and (cur.item.first /~ g implies Result [cur.item.first] = Current [cur.item.first]) end subtracted_by alias "-" (g: G): like Current -- Return a representation of current bag with -- 'g' of quantity 1 subtracted. require Current [g] >= 1 ensure current_bag_unchanged: Current ~ old Current.deep_twin across Result as cur all (cur.item.first ~ g implies Result [cur.item.first] = Current [cur.item.first] - 1) and (cur.item.first /~ g implies Result [cur.item.first] = Current [cur.item.first]) end differenced alias "|\" (other: like Current): like Current -- Return a representation of current bag with -- 'other' subtracted. require other |<: Current ensure current_bag_unchanged: Current ~ old Current.deep_twin across Result as cur all (other.has (cur.item.first) implies Result [cur.item.first] = Current [cur.item.first] - other [cur.item.first]) and (not other.has (cur.item.first) implies Result [cur.item.first] = Current [cur.item.first]) end feature -- Quantifiers hold_count (exp: PREDICATE [PAIR [G, INTEGER_32]]): INTEGER_32 -- How many items satisfying exp are in Current? ensure current_bag_unchanged: Current ~ old Current.deep_twin maximum_result: 0 <= Result and Result <= count 0 <= Result and Result <= # as_function.domain comprehension alias "|" (exp: PREDICATE [PAIR [G, INTEGER_32]]): like Current -- Largest subset of the current fun whose elements satisfy exp ensure current_bag_unchanged: Current ~ old Current.deep_twin is_subset: Result |<: Current all_satisfying_exp: Result.hold_count (exp) = # Result.as_set consistent_satisfying_items: Current.hold_count (exp) = # Result.as_set feature -- Equality is_equal (other: like Current): BOOLEAN -- Is other attached to an object considered -- equal to current object? ensure then Result = (Current |<: other and other |<: Current) Result = (as_function ~ other.as_function) feature -- Output out: STRING_8 -- Return a string representation of current bag ensure then Result ~ as_function.out debug_output: STRING_8 -- Return a string representation of current bag -- for debugging ensure then Result ~ out invariant bag_not_containing_zero_occurrence_item: across Current as pair all pair.item.second > 0 end end -- class BAG
Generated by ISE EiffelStudio