indexing
description: "A network stream socket."
legal: "See notice at end of class."
status: "See notice at end of class."
date: "$Date: 2006-07-19 15:54:37 -0700 (Wed, 19 Jul 2006) $"
revision: "$Revision: 61492 $"
class interface
NETWORK_STREAM_SOCKET
create {NETWORK_STREAM_SOCKET}
create_from_descriptor (fd: INTEGER_32)
`fd'
NETWORK_SOCKET
require SOCKET
True
ensure SOCKET
family_valid: family = address.family
opened_all: is_open_write and is_open_read
ensure then NETWORK_SOCKET
timeout_set_to_default: timeout = default_timeout
create
make
ensure
timeout_set_to_default: timeout = default_timeout
make_client_by_port (a_peer_port: INTEGER_32; a_peer_host: STRING_8)
`a_peer_host'
`a_peer_port'
require
valid_peer_host: a_peer_host /= Void and then not a_peer_host.is_empty
valid_port: a_peer_port >= 0
make_server_by_port (a_port: INTEGER_32)
`a_port'
require
valid_port: a_port >= 0
feature
create_from_descriptor (fd: INTEGER_32)
`fd'
NETWORK_SOCKET
require SOCKET
True
ensure SOCKET
family_valid: family = address.family
opened_all: is_open_write and is_open_read
ensure then NETWORK_SOCKET
timeout_set_to_default: timeout = default_timeout
make
ensure
timeout_set_to_default: timeout = default_timeout
make_client_by_port (a_peer_port: INTEGER_32; a_peer_host: STRING_8)
`a_peer_host'
`a_peer_port'
require
valid_peer_host: a_peer_host /= Void and then not a_peer_host.is_empty
valid_port: a_peer_port >= 0
make_server_by_port (a_port: INTEGER_32)
`a_port'
require
valid_port: a_port >= 0
feature
generating_type: STRING_8
ANY
ensure ANY
generating_type_not_void: Result /= Void
generating_type_not_empty: not Result.is_empty
generator: STRING_8
ANY
ensure ANY
generator_not_void: Result /= Void
generator_not_empty: not Result.is_empty
retrieved: ANY
Retrieve_exception
SOCKET
require IO_MEDIUM
is_readable: readable
support_storable: support_storable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
support_storable: support_storable
ensure IO_MEDIUM
result_exists: Result /= Void
feature
frozen deep_equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
shallow_implies_deep: standard_equal (some, other) implies Result
both_or_none_void: (some = Void) implies (Result = (other = Void))
same_type: (Result and (some /= Void)) implies (other /= Void and then some.same_type (other))
symmetric: Result implies deep_equal (other, some)
frozen equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))
frozen is_deep_equal (other: NETWORK_STREAM_SOCKET): BOOLEAN
`Current'`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
shallow_implies_deep: standard_is_equal (other) implies Result
same_type: Result implies same_type (other)
symmetric: Result implies other.is_deep_equal (Current)
is_equal (other: NETWORK_STREAM_SOCKET): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
frozen standard_equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))
frozen standard_is_equal (other: NETWORK_STREAM_SOCKET): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
same_type: Result implies same_type (other)
symmetric: Result implies other.standard_is_equal (Current)
feature
address: NETWORK_SOCKET_ADDRESS
NETWORK_SOCKET
address_in_use: BOOLEAN
SOCKET_RESOURCES
address_not_readable: BOOLEAN
SOCKET_RESOURCES
already_bound: BOOLEAN
SOCKET_RESOURCES
bad_socket_handle: BOOLEAN
SOCKET_RESOURCES
bytes_read: INTEGER_32
read_to_managed_pointer
IO_MEDIUM
conforms_to (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
connect_in_progress: BOOLEAN
SOCKET_RESOURCES
connection_refused: BOOLEAN
SOCKET_RESOURCES
dtable_full: BOOLEAN
SOCKET_RESOURCES
error: STRING_8
SOCKET_RESOURCES
error_number: INTEGER_32
SOCKET_RESOURCES
expired_socket: BOOLEAN
SOCKET_RESOURCES
has_delay: BOOLEAN
require
socket_exists: exists
has_exception_state: BOOLEAN
timeout
NETWORK_SOCKET
invalid_address: BOOLEAN
SOCKET_RESOURCES
invalid_socket_handle: BOOLEAN
SOCKET_RESOURCES
is_linger_on: BOOLEAN
require
socket_exists: exists
is_out_of_band_inline: BOOLEAN
require
socket_exists: exists
is_plain_text: BOOLEAN
IO_MEDIUM
is_valid_peer_address (addr: like address): BOOLEAN
`addr'
NETWORK_SOCKET
require SOCKET
address_exists: addr /= Void
last_character: CHARACTER_8
read_character
IO_MEDIUM
last_double: REAL_64
read_double
IO_MEDIUM
last_integer: INTEGER_32
read_integer
IO_MEDIUM
last_integer_16: INTEGER_16
read_integer_16
IO_MEDIUM
last_integer_32: INTEGER_32
last_integer
IO_MEDIUM
last_integer_64: INTEGER_64
read_integer_64
IO_MEDIUM
last_integer_8: INTEGER_8
read_integer_8
IO_MEDIUM
last_natural: NATURAL_32
read_natural
IO_MEDIUM
last_natural_16: NATURAL_16
read_natural_16
IO_MEDIUM
last_natural_32: NATURAL_32
last_natural
IO_MEDIUM
last_natural_64: NATURAL_64
read_natural_64
IO_MEDIUM
last_natural_8: NATURAL_8
read_natural_8
IO_MEDIUM
last_real: REAL_32
read_real
IO_MEDIUM
last_string: ?STRING_8
IO_MEDIUM
linger_time: INTEGER_32
require
socket_exists: exists
maximum_seg_size: INTEGER_32
require
socket_exists: exists
network: BOOLEAN
SOCKET_RESOURCES
no_buffers: BOOLEAN
SOCKET_RESOURCES
no_permission: BOOLEAN
SOCKET_RESOURCES
not_connected: BOOLEAN
SOCKET_RESOURCES
port: INTEGER_32
NETWORK_SOCKET
require NETWORK_SOCKET
valid_socket: exists
protected_address: BOOLEAN
SOCKET_RESOURCES
protocol_not_supported: BOOLEAN
SOCKET_RESOURCES
ready_for_reading: BOOLEAN
timeout
NETWORK_SOCKET
ready_for_writing: BOOLEAN
timeout
NETWORK_SOCKET
reuse_address: BOOLEAN
NETWORK_SOCKET
require NETWORK_SOCKET
socket_exists: exists
same_type (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
definition: Result = (conforms_to (other) and other.conforms_to (Current))
socket_family_not_supported: BOOLEAN
SOCKET_RESOURCES
socket_in_use: BOOLEAN
SOCKET_RESOURCES
socket_ok: BOOLEAN
SOCKET_RESOURCES
socket_would_block: BOOLEAN
SOCKET_RESOURCES
support_storable: BOOLEAN is True
STREAM_SOCKET
timeout: INTEGER_32
NETWORK_SOCKET
zero_option: BOOLEAN
SOCKET_RESOURCES
feature
do_not_reuse_address
reuse_address
NETWORK_SOCKET
require NETWORK_SOCKET
socket_exists: exists
set_delay
require
socket_exists: exists
set_linger_off
require
socket_exists: exists
set_linger_on (time: INTEGER_32)
`time'
require
socket_exists: exists
set_nodelay
require
socket_exists: exists
set_out_of_band_inline
require
socket_exists: exists
set_out_of_band_not_inline
require
socket_exists: exists
set_reuse_address
reuse_address
NETWORK_SOCKET
require NETWORK_SOCKET
socket_exists: exists
set_timeout (n: INTEGER_32)
`n'
NETWORK_SOCKET
require NETWORK_SOCKET
non_negative: n >= 0
ensure NETWORK_SOCKET
timeout_set: timeout = n or timeout = default_timeout
feature
basic_store (object: ANY)
`object'
SOCKET
require IO_MEDIUM
object_not_void: object /= Void
extendible: extendible
support_storable: support_storable
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
support_storable: support_storable
general_store (object: ANY)
`object'
SOCKET
require IO_MEDIUM
object_not_void: object /= Void
extendible: extendible
support_storable: support_storable
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
support_storable: support_storable
independent_store (object: ANY)
`object'
SOCKET
require IO_MEDIUM
object_not_void: object /= Void
extendible: extendible
support_storable: support_storable
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
support_storable: support_storable
feature
dispose
IO_MEDIUM
feature
copy (other: NETWORK_STREAM_SOCKET)
`other'
ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
frozen deep_copy (other: NETWORK_STREAM_SOCKET)
copy`other'deep_twin
ANY
require ANY
other_not_void: other /= Void
ensure ANY
deep_equal: deep_equal (Current, other)
frozen deep_twin: NETWORK_STREAM_SOCKET
ANY
ensure ANY
deep_twin_not_void: Result /= Void
deep_equal: deep_equal (Current, Result)
frozen standard_copy (other: NETWORK_STREAM_SOCKET)
`other'
ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_standard_equal: standard_is_equal (other)
frozen standard_twin: NETWORK_STREAM_SOCKET
`other'
ANY
ensure ANY
standard_twin_not_void: Result /= Void
equal: standard_equal (Result, Current)
frozen twin: NETWORK_STREAM_SOCKET
`Current'
twincopycopy
ANY
ensure ANY
twin_not_void: Result /= Void
is_equal: Result.is_equal (Current)
feature
name: STRING_8
SOCKET
require IO_MEDIUM
True
require else SOCKET
socket_exists: exists
feature
frozen default: ?NETWORK_STREAM_SOCKET
ANY
frozen default_pointer: POINTER
`POINTER'
`p'default
`p'`POINTER'
ANY
default_rescue
ANY
frozen do_nothing
ANY
feature
lastchar: CHARACTER_8
read_character
IO_MEDIUM
lastdouble: REAL_64
read_double
IO_MEDIUM
lastint: INTEGER_32
read_integer
IO_MEDIUM
lastreal: REAL_32
read_real
IO_MEDIUM
laststring: ?STRING_8
IO_MEDIUM
feature
accept
accepted
STREAM_SOCKET
require STREAM_SOCKET
socket_exists: exists
accepted: NETWORK_STREAM_SOCKET
STREAM_SOCKET
listen (queue: INTEGER_32)
`queue'
STREAM_SOCKET
require STREAM_SOCKET
socket_exists: exists
feature
old_socket_address: SOCKET_ADDRESS
SOCKET
bind
address
SOCKET
require SOCKET
socket_exists: exists
valid_local_address: address /= Void
cleanup
SOCKET
close
SOCKET
require IO_MEDIUM
medium_is_open: not is_closed
require else SOCKET
socket_exists: exists
close_socket
SOCKET
require SOCKET
socket_exists: exists
is_open: is_open_read or is_open_write
ensure SOCKET
is_closed: is_closed
not_is_open: not is_open_read and not is_open_write
connect
SOCKET
require SOCKET
socket_exists: exists
valid_peer_address: peer_address /= Void
descriptor: INTEGER_32
SOCKET
descriptor_available: BOOLEAN
SOCKET
family: INTEGER_32
SOCKET
is_closed: BOOLEAN
SOCKET
make_socket
SOCKET
require SOCKET
valid_family: family >= 0
valid_type: type >= 0
valid_protocol: protocol >= 0
peer_address: like address
SOCKET
protocol: INTEGER_32
`udp'`tcp'
SOCKET
set_address (addr: like address)
`addr'
SOCKET
require SOCKET
same_type: addr.family = family
ensure SOCKET
address_set: address = addr
old_socket_set_peer_address (addr: like address)
`addr'
SOCKET
require SOCKET
address_exists: addr /= Void
address_valid: is_valid_peer_address (addr)
ensure SOCKET
address_set: peer_address = addr
set_peer_address (addr: like address)
`addr'
SOCKET
require SOCKET
address_exists: addr /= Void
address_valid: is_valid_peer_address (addr)
ensure SOCKET
address_set: peer_address = addr
type: INTEGER_32
SOCKET
feature
c_msgdontroute: INTEGER_32
SOCKET_RESOURCES
c_oobmsg: INTEGER_32
SOCKET_RESOURCES
c_peekmsg: INTEGER_32
SOCKET_RESOURCES
feature
last_boolean: BOOLEAN
SOCKET
read (size: INTEGER_32): PACKET
`size'
SOCKET
require SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_boolean
last_boolean
SOCKETreadbool
SOCKET
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_character
last_character
SOCKETreadchar
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_double
last_double
SOCKETreaddouble
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_integer
last_integer
SOCKETreadintread_integer_32
SOCKET
require IO_MEDIUM
is_readable: