EiffelBase class
(HTML page generated by ISE Eiffel 4.2)
Eiffel Class
indexing
description: "``Active%'%' data structures, which at every stage have a possibly undefined ``current item%'%'. Basic access and modification operations apply to the current item.";
status: "See notice at end of class";
names: active, access;
access: membership;
contents: generic;
date: "$Date: 2007-03-30 11:10:11 -0800 (Fri, 30 Mar 2007) $";
revision: "$Revision: 95354 $"
deferred class ACTIVE [G]
inherit
BAG [G]
feature -- Access
item: G is
-- Current item
require
readable: readable
deferred
end;
feature -- Status report
readable: BOOLEAN is
-- Is there a current item that may be read?
deferred
end;
writable: BOOLEAN is
-- Is there a current item that may be modified?
deferred
end;
feature -- Element change
replace (v: G) is
-- Replace current item by v.
require
writable: writable
deferred
ensure
item_replaced: item = v
end;
feature -- Removal
remove is
-- Remove current item.
require
prunable: prunable;
writable: writable
deferred
end;
invariant
writable_constraint: writable implies readable;
empty_constraint: empty implies (notreadable) and (notwritable);
end -- class ACTIVE
|
