indexing
	description: "The objects available from the environment at time of execution"

class interface
	EXECUTION_ENVIRONMENT

feature -- Access

	command_line: ARGUMENTS
			-- Command line that was used to start current execution

	current_working_directory: STRING
			-- Directory of current execution

	default_shell: STRING
			-- Default shell

	get (s: STRING): STRING
			-- Value of s if it is an environment variable and has been set;
			-- void otherwise.
		require
			s_exists: s /= void

	home_directory_name: STRING
			-- Directory name corresponding to the home directory.
		require
			home_directory_supported: operating_environment.home_directory_supported

	root_directory_name: STRING
			-- Directory name corresponding to the root directory.
		require
			root_directory_supported: operating_environment.root_directory_supported
	
feature -- Status setting

	change_working_directory (path: STRING)
			-- Set the current directory to path

	put (value, key: STRING)
			-- Set the environment variable key to value.
		require
			key_exists: key /= void;
			key_meaningful: key.count > 0;
			value_exists: value /= void
		ensure
			variable_set: (return_code = 0) implies (value.is_equal (get (key)))

	system (s: STRING)
			-- Pass to the operating system a request to execute s.
			-- If s is empty, use the default shell as command.
		require
			s_exists: s /= void
	
feature -- Status

	return_code: INTEGER
			-- Status code set by last call to system or put
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);

end -- class EXECUTION_ENVIRONMENT