indexing description: "Externals for managing the object id stack (see identified.e)" class interface IDENTIFIED_CONTROLLER feature -- Measurement object_id_stack_size: INTEGER -- Size of the object_id stack in chunks feature -- Status setting extend_object_id_stack (nb_chunks: INTEGER) -- Extend the object_id stack by nb_chunks chunks. require positive_nb: nb_chunks > 0 invariant -- from GENERAL reflexive_equality: standard_is_equal (Current); reflexive_conformance: conforms_to (Current); end -- class IDENTIFIED_CONTROLLER