indexing
description: "Connexion oriented socket."
status: "See notice at end of class"
date: "$Date$"
revision: "$Revision$"
class interface
STREAM_SOCKET
create
feature
create_from_descriptor (fd: INTEGER)
fd
SOCKET
ensure SOCKET
family_valid: family = address.family
opened_all: is_open_write and is_open_read
feature
retrieved: ANY
Retrieve_exception
SOCKET
require IO_MEDIUM
exists: exists
is_open_read: is_open_read
support_storable: support_storable
ensure IO_MEDIUM
result_exists: Result /= void
feature
address_in_use: BOOLEAN
SOCKET_RESOURCES
address_not_readable: BOOLEAN
SOCKET_RESOURCES
already_bound: BOOLEAN
SOCKET_RESOURCES
bad_socket_handle: BOOLEAN
SOCKET_RESOURCES
connect_in_progress: BOOLEAN
SOCKET_RESOURCES
connection_refused: BOOLEAN
SOCKET_RESOURCES
dtable_full: BOOLEAN
SOCKET_RESOURCES
error: STRING
SOCKET_RESOURCES
error_number: INTEGER
SOCKET_RESOURCES
expired_socket: BOOLEAN
SOCKET_RESOURCES
invalid_address: BOOLEAN
SOCKET_RESOURCES
invalid_socket_handle: BOOLEAN
SOCKET_RESOURCES
is_plain_text: BOOLEAN
IO_MEDIUM
is_valid_peer_address (addr: SOCKET_ADDRESS): BOOLEAN
addr
SOCKET
require SOCKET
address_exists: addr /= void
last_character: CHARACTER
read_character
IO_MEDIUM
last_double: DOUBLE
read_double
IO_MEDIUM
last_integer: INTEGER
read_integer
IO_MEDIUM
last_real: REAL
read_real
IO_MEDIUM
last_string: STRING
IO_MEDIUM
network: BOOLEAN
SOCKET_RESOURCES
no_buffers: BOOLEAN
SOCKET_RESOURCES
no_permission: BOOLEAN
SOCKET_RESOURCES
not_connected: BOOLEAN
SOCKET_RESOURCES
protected_address: BOOLEAN
SOCKET_RESOURCES
protocol_not_supported: BOOLEAN
SOCKET_RESOURCES
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
zero_option: BOOLEAN
SOCKET_RESOURCES
feature
basic_store (object: ANY)
object
SOCKET
require IO_MEDIUM
object_not_void: object /= void
exists: exists
is_open_write: is_open_write
support_storable: support_storable
general_store (object: ANY)
object
SOCKET
require IO_MEDIUM
object_not_void: object /= void
exists: exists
is_open_write: is_open_write
support_storable: support_storable
independent_store (object: ANY)
object
SOCKET
require IO_MEDIUM
object_not_void: object /= void
exists: exists
is_open_write: is_open_write
support_storable: support_storable
feature
dispose
IO_MEDIUM
feature
name: STRING
SOCKET
require IO_MEDIUM
True
require else SOCKET
socket_exists: exists
feature
lastchar: CHARACTER
read_character
IO_MEDIUM
lastdouble: DOUBLE
read_double
IO_MEDIUM
lastint: INTEGER
read_integer
IO_MEDIUM
lastreal: REAL
read_real
IO_MEDIUM
laststring: STRING
IO_MEDIUM
feature
accept
accepted
require
socket_exists: exists
accepted: like Current
listen (queue: INTEGER)
queue
require
socket_exists: exists
feature
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
connect
SOCKET
require SOCKET
socket_exists: exists
valid_peer_address: peer_address /= void
descriptor: INTEGER
SOCKET
descriptor_available: BOOLEAN
SOCKET
family: INTEGER
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
udptcp
SOCKET
set_address (addr: like address)
addr
SOCKET
require SOCKET
same_type: addr.family = family
ensure SOCKET
address_set: 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
SOCKET
feature
c_msgdontroute: INTEGER
SOCKET_RESOURCES
c_oobmsg: INTEGER
SOCKET_RESOURCES
c_peekmsg: INTEGER
SOCKET_RESOURCES
feature
last_boolean: BOOLEAN
SOCKET
read (size: INTEGER): 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
SOCKETreadint
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_line
SOCKETreadline
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_real
last_real
SOCKETreadreal
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
read_stream (nb_char: INTEGER)
nb_char
last_string
SOCKETreadstream
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
readbool
last_boolean
SOCKETread_boolean
SOCKET
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
readchar
last_character
SOCKETread_character
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
readdouble
last_double
SOCKETread_double
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
readint
last_integer
SOCKETread_integer
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
readline
SOCKETread_line
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
readreal
last_real
SOCKETread_real
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
readstream (nb_char: INTEGER)
nb_char
last_string
SOCKETread_stream
SOCKET
require IO_MEDIUM
is_readable: readable
require else SOCKET
socket_exists: exists
opened_for_read: is_open_read
receive (size, flags: INTEGER): PACKET
size
SOCKET
require SOCKET
socket_exists: exists
opened_for_read: is_open_read
feature
exists: BOOLEAN
SOCKET
extendible: BOOLEAN
SOCKET
is_executable: BOOLEAN
SOCKET
require IO_MEDIUM
handle_exists: exists
is_open_read: BOOLEAN
SOCKET
is_open_write: BOOLEAN
SOCKET
is_readable: BOOLEAN
SOCKET
require IO_MEDIUM
handle_exists: exists
is_writable: BOOLEAN
SOCKET
require IO_MEDIUM
handle_exists: exists
new_line
SOCKETput_new_line
SOCKET
require IO_MEDIUM
extendible: extendible
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
put_boolean (b: BOOLEAN)
b
SOCKETputbool
SOCKET
require IO_MEDIUM
extendible: extendible
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
put_character (c: CHARACTER)
c
SOCKETputchar
SOCKET
require IO_MEDIUM
extendible: extendible
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
put_double (d: DOUBLE)
d
SOCKETputdouble
SOCKET
require IO_MEDIUM
extendible: extendible
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
put_integer (i: INTEGER)
i
SOCKETputint
SOCKET
require IO_MEDIUM
extendible: extendible
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
put_new_line
SOCKETnew_line
SOCKET
require IO_MEDIUM
extendible: extendible
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
put_real (r: REAL)
r
SOCKETputreal
SOCKET
require IO_MEDIUM
extendible: extendible
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
put_string (s: STRING)
s
SOCKETputstring
SOCKET
require IO_MEDIUM
extendible: extendible
non_void: s /= void
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
putbool (b: BOOLEAN)
b
SOCKETput_boolean
SOCKET
require IO_MEDIUM
extendible: extendible
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
putchar (c: CHARACTER)
c
SOCKETput_character
SOCKET
require IO_MEDIUM
extendible: extendible
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
putdouble (d: DOUBLE)
d
SOCKETput_double
SOCKET
require IO_MEDIUM
extendible: extendible
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
putint (i: INTEGER)
i
SOCKETput_integer
SOCKET
require IO_MEDIUM
extendible: extendible
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
putreal (r: REAL)
r
SOCKETput_real
SOCKET
require IO_MEDIUM
extendible: extendible
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
putstring (s: STRING)
s
SOCKETput_string
SOCKET
require IO_MEDIUM
extendible: extendible
non_void: s /= void
require else SOCKET
socket_exists: exists
opened_for_write: is_open_write
readable: BOOLEAN
SOCKET
require IO_MEDIUM
handle_exists: exists
send (a_packet: PACKET; flags: INTEGER)
a_packet
SOCKET
require SOCKET
socket_exists: exists
opened_for_write: is_open_write
valid_packet: a_packet /= void
write (a_packet: PACKET)
a_packet
SOCKET
require SOCKET
socket_exists: exists
opened_for_write: is_open_write
feature
debug_enabled: BOOLEAN
SOCKET
require SOCKET
socket_exists: exists
disable_debug
SOCKET
require SOCKET
socket_exists: exists
do_not_route
SOCKET
require SOCKET
socket_exists: exists
enable_debug
SOCKET
require SOCKET
socket_exists: exists
group_id: INTEGER
SOCKET
require SOCKET
socket_exists: exists
group_set: is_group_id
is_blocking: BOOLEAN
SOCKET
is_group_id: BOOLEAN
SOCKET
require SOCKET
socket_exists: exists
is_process_id: BOOLEAN
SOCKET
require SOCKET
socket_exists: exists
is_socket_stream: BOOLEAN
SOCKET
require SOCKET
socket_exists: exists
process_id: INTEGER
SOCKET
require SOCKET
socket_exists: exists
process_set: is_process_id
receive_buf_size: INTEGER
SOCKET
require SOCKET
socket_exists: exists
route
SOCKET
require SOCKET
socket_exists: exists
route_enabled: BOOLEAN
SOCKET
require SOCKET
socket_exists: exists
send_buf_size: INTEGER
SOCKET
require SOCKET
socket_exists: exists
set_blocking
SOCKET
require SOCKET
socket_exists: exists
ensure SOCKET
is_blocking
set_non_blocking
SOCKET
require SOCKET
socket_exists: exists
ensure SOCKET
not is_blocking
set_owner (own: INTEGER)
SOCKET
require SOCKET
socket_exists: exists
valid_owner: own /= 0 and own /= - 1
ensure SOCKET
set_id: own < - 1 implies own = group_id or else own > 0 implies own = process_id
set_receive_buf_size (s: INTEGER)
SOCKET
require SOCKET
socket_exists: exists
ensure SOCKET
size_set: s = receive_buf_size
set_send_buf_size (s: INTEGER)
s
SOCKET
require SOCKET
socket_exists: exists
ensure SOCKET
size_set: s = send_buf_size
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- STREAM_SOCKET