EiffelBase class
(HTML page generated by ISE Eiffel 4.2)
Eiffel Class
indexing
description: "Collection, where each element must be unique.";
status: "See notice at end of class";
names: set;
access: membership;
contents: generic;
date: "$Date: 2007-03-30 11:10:11 -0800 (Fri, 30 Mar 2007) $";
revision: "$Revision: 95354 $"
deferred class SET [G]
inherit
COLLECTION [G]
redefine
changeable_comparison_criterion
end
feature -- Measurement
count: INTEGER is
-- Number of items
deferred
end;
feature -- Element change
extend (v: G) is
-- Ensure that set includes v.
-- Was declared in SET as synonym of extend and put.
deferred
ensure
in_set_already: old has (v) implies (count = old count);
added_to_set: notold has (v) implies (count = old count + 1)
end;
put (v: G) is
-- Ensure that set includes v.
-- Was declared in SET as synonym of extend and put.
deferred
ensure
in_set_already: old has (v) implies (count = old count);
added_to_set: notold has (v) implies (count = old count + 1)
end;
feature -- Removal
prune (v: G) is
-- Remove v if present.
deferred
ensure
removed_count_change: old has (v) implies (count = old count - 1);
not_removed_no_count_change: notold has (v) implies (count = old count);
item_deleted: nothas (v)
end;
changeable_comparison_criterion: BOOLEAN is
-- May object_comparison be changed?
-- (Answer: only if set empty; otherwise insertions might
-- introduce duplicates, destroying the set property.)
do
Result := empty
ensure
only_on_empty: Result = empty
end;
end -- class SET
|
