+
Point of view
All features
class WAITPID_INPUT
Features
{}
{}
{}
{}
{}
{}
{}
{}
is True
constant attribute
is False
constant attribute
require
- is_connected
- can_disconnect
- is_connected
- can_disconnect
ensure
require
- is_connected
- valid_last_character
is False
constant attribute
require
- 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
filtered_has_stream_pointer:
BOOLEAN
is False
constant attribute
require
- is_connected
- can_read_character
filtered_unread_character
effective procedure
require
- is_connected
- can_unread_character
require
- is_connected
- valid_last_character
basic_exec_waitpid_init (obj: WAITPID_INPUT)
{}
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
is_equal (other: WAITPID_INPUT):
BOOLEAN
effective function
require
ensure
-
commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)
ensure
-
assertion_check_only: Result
current_is_not_an_expanded_type:
BOOLEAN
effective function
{}