indexing
description: "Facilities for inspecting global environment information."
status: "See notice at end of class"
keywords: "environment, application, global, system"
date: "$Date$"
revision: "$Revision$"
class interface
EV_ENVIRONMENT
create
frozen default_create
EV_ANY
ensure then EV_ANY
is_coupled: implementation /= void
is_initialized: is_initialized
default_create_called_set: default_create_called
is_in_default_state: is_in_default_state
feature
application: EV_APPLICATION
require
not_destroyed: not is_destroyed
ensure
bridge_ok: Result = implementation.application
data: ANY
EV_ANY
feature
set_data (some_data: like data)
some_datadata
EV_ANY
require EV_ANY
not_destroyed: not is_destroyed
ensure EV_ANY
data_assigned: data = some_data
feature
copy (other: like Current)
other
EV_ANY
require ANY
other_not_void: other /= void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
feature
destroy
Current
EV_ANY
ensure EV_ANY
is_destroyed: is_destroyed
feature
is_destroyed: BOOLEAN
Current
EV_ANY
ensure EV_ANY
bridge_ok: Result = implementation.is_destroyed
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
EV_ANY
is_initialized: is_initialized
is_coupled: implementation /= void and then implementation.interface = Current
default_create_called: default_create_called
end -- EV_ENVIRONMENT