indexing
	description: "EIFFEL_SYSTEM - access to information about Eiffel classes"

class interface
	EIFFEL_SYSTEM

feature -- Checks

	checks_on: BOOLEAN
			-- current state of invariant checks

	set_checks_off

	set_checks_on
	
feature -- Invariants

	invariants_on: BOOLEAN
			-- current state of invariant checks

	set_invariants_off

	set_invariants_on
	
feature -- Loop invariants

	loop_invariants_on: BOOLEAN
			-- current state of loop invariant checks

	set_loop_invariants_off

	set_loop_invariants_on
	
feature -- Loop variants

	loop_variants_on: BOOLEAN
			-- current state of loop variant checks

	set_loop_variants_off

	set_loop_variants_on
	
feature -- Postconditions

	postconditions_on: BOOLEAN
			-- current state of postcondition checks

	set_postconditions_off

	set_postconditions_on
	
feature -- Preconditions

	preconditions_on: BOOLEAN
			-- current state of precondition checks

	set_preconditions_off

	set_preconditions_on
	
feature -- classes

	type_by_name (type_name: STRING): EIFFEL_TYPE
			-- retrieve by type name
		require
			type_name_not_void: type_name /= void

	type_for_object (object: ANY): EIFFEL_TYPE
		require
			object_not_void: object /= void;
			known_type: is_known_type (object.generating_type)
		ensure
			result_not_void: Result /= void
	
feature -- queries

	all_types: ARRAY [EIFFEL_TYPE]
			-- all classes that can be examined in this system

	is_known_type (type_name: STRING): BOOLEAN
			-- can this type be examined in the current system
		require
			type_name_not_void: type_name /= void
	
end -- class EIFFEL_SYSTEM