+
Point of view
All features
class SERVER_SOCKET_INPUT_OUTPUT_STREAM
- server /= Void
- socket /= Void
- index >= in_buffer.lower or else beginning_of_stream and then index = in_buffer.lower - 1
-
init_by_heirs: is_made
- filter = Void
Features
{}
{}
{}
{}
{}
{}
{}
{}
{}
{}
{}
{}
{}
{}
{}
require
- is_connected
- can_disconnect
- is_connected
- can_disconnect
- is_connected
- can_disconnect
- is_connected
- can_disconnect
ensure
socket_disconnected (a_socket:
SOCKET)
effective procedure
{}
require
- a_socket = socket
- not is_connected
require
ensure
- Result implies not end_of_input
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
filtered_read_line_in (buffer:
STRING)
effective procedure
require
- is_connected
- buffer /= Void
require
- is_connected
- buffer /= Void
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 True
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
require
-
called_by_heirs_constructors_only: not is_made
-
create_socket_first: socket /= Void
ensure
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
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