+
Point of view
All features
class SIMPLE_INPUT_OUTPUT_STREAM
Features
{}
{}
{}
{}
{}
{}
{}
{}
{}
{}
{}
require
- is_connected
- can_disconnect
- is_connected
- can_disconnect
- is_connected
- can_disconnect
- is_connected
- can_disconnect
ensure
require
- is_connected
- valid_last_character
require
- is_connected
- can_read_character
filtered_unread_character
effective procedure
require
- is_connected
- can_unread_character
require
- is_connected
- valid_last_character
require
- is_connected
- can_put_character(c)
require
- is_connected
- filtered_has_descriptor
- is_connected
- filtered_has_descriptor
- is_connected
- filtered_has_descriptor
- is_connected
- filtered_has_descriptor
is False
constant attribute
require
- is_connected
- filtered_has_stream_pointer
- is_connected
- filtered_has_stream_pointer
- is_connected
- filtered_has_stream_pointer
- is_connected
- filtered_has_stream_pointer
filtered_has_stream_pointer:
BOOLEAN
is False
constant attribute
is True
constant attribute
is True
constant attribute
require
ensure
- Result implies not end_of_input
is True
constant attribute
require
- is_connected
- not is_filtered and then can_read_character
ensure
require
- is_connected
- not is_filtered and then can_read_line
- buffer /= Void
require
- is_connected
- not is_filtered
- buffer /= Void
- limit > 0
require
- is_connected
- not is_filtered and then can_unread_character
ensure
require
- is_connected
- not end_of_input
- not is_filtered and then valid_last_character
ensure
filtered_read_line_in (buffer:
STRING)
effective procedure
frozen
effective function
ensure
-
not_void: Result /= Void
-
always_the_same: Result = url
skip_separators_using (separators:
STRING)
effective procedure
reach_and_skip (keyword:
STRING)
effective procedure
read_word_using (separators:
STRING)
effective procedure
require
- is_connected
- not is_filtered and then can_put_character(c)
ensure
-
yes_indeed_it_is_the_same_object: Result.to_pointer = to_pointer
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
append_file (file_name:
STRING)
effective procedure