indexing
description: "Generic sockets"
status: "See notice at end of class"
date: "$Date$"
revision: "$Revision$"
class interface
SOCKET
create
feature
create_from_descriptor (fd: INTEGER)
fd
ensure
family_valid: family = address.family
opened_all: is_open_write and is_open_read
feature
retrieved: ANY
Retrieve_exception
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
require
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
zero_option: BOOLEAN
SOCKET_RESOURCES
feature
basic_store (object: ANY)
object
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
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
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
require IO_MEDIUM
True
require else
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
address: SOCKET_ADDRESS
bind
address
require
socket_exists: exists
valid_local_address: address /= void
cleanup
close
require IO_MEDIUM
medium_is_open: not is_closed
require else
socket_exists: exists
connect
require
socket_exists: exists
valid_peer_address: peer_address /= void
descriptor: INTEGER
descriptor_available: BOOLEAN
family: INTEGER
is_closed: BOOLEAN
make_socket
require
valid_family: family >= 0
valid_type: type >= 0
valid_protocol: protocol >= 0
peer_address: like address
protocol: INTEGER
udptcp
set_address (addr: like address)
addr
require
same_type: addr.family = family
ensure
address_set: address = addr
set_peer_address (addr: like address)
addr
require
address_exists: addr /= void
address_valid: is_valid_peer_address (addr)
ensure
address_set: peer_address = addr
type: INTEGER
feature
c_msgdontroute: INTEGER
SOCKET_RESOURCES
c_oobmsg: INTEGER
SOCKET_RESOURCES
c_peekmsg: INTEGER
SOCKET_RESOURCES
feature
last_boolean: BOOLEAN
read (size: INTEGER): PACKET
size
require
socket_exists: exists
opened_for_read: is_open_read
read_boolean
last_boolean
SOCKETreadbool
require else
socket_exists: exists
opened_for_read: is_open_read
read_character
last_character
SOCKETreadchar
require IO_MEDIUM
is_readable: readable
require else
socket_exists: exists
opened_for_read: is_open_read
read_double
last_double
SOCKETreaddouble
require IO_MEDIUM
is_readable: readable
require else
socket_exists: exists
opened_for_read: is_open_read
read_integer
last_integer
SOCKETreadint
require IO_MEDIUM
is_readable: readable
require else
socket_exists: exists
opened_for_read: is_open_read
read_line
SOCKETreadline
require IO_MEDIUM
is_readable: readable
require else
socket_exists: exists
opened_for_read: is_open_read
read_real
last_real
SOCKETreadreal
require IO_MEDIUM
is_readable: readable
require else
socket_exists: exists
opened_for_read: is_open_read
read_stream (nb_char: INTEGER)
nb_char
last_string
SOCKETreadstream
require IO_MEDIUM
is_readable: readable
require else
socket_exists: exists
opened_for_read: is_open_read
readbool
last_boolean
SOCKETread_boolean
require else
socket_exists: exists
opened_for_read: is_open_read
readchar
last_character
SOCKETread_character
require IO_MEDIUM
is_readable: readable
require else
socket_exists: exists
opened_for_read: is_open_read
readdouble
last_double
SOCKETread_double
require IO_MEDIUM
is_readable: readable
require else
socket_exists: exists
opened_for_read: is_open_read
readint
last_integer
SOCKETread_integer
require IO_MEDIUM
is_readable: readable
require else
socket_exists: exists
opened_for_read: is_open_read
readline
SOCKETread_line
require IO_MEDIUM
is_readable: readable
require else
socket_exists: exists
opened_for_read: is_open_read
readreal
last_real
SOCKETread_real
require IO_MEDIUM
is_readable: readable
require else
socket_exists: exists
opened_for_read: is_open_read
readstream (nb_char: INTEGER)
nb_char
last_string
SOCKETread_stream
require IO_MEDIUM
is_readable: readable
require else
socket_exists: exists
opened_for_read: is_open_read
receive (size, flags: INTEGER): PACKET
size
require
socket_exists: exists
opened_for_read: is_open_read
feature
exists: BOOLEAN
extendible: BOOLEAN
is_executable: BOOLEAN
require IO_MEDIUM
handle_exists: exists
is_open_read: BOOLEAN
is_open_write: BOOLEAN
is_readable: BOOLEAN
require IO_MEDIUM
handle_exists: exists
is_writable: BOOLEAN
require IO_MEDIUM
handle_exists: exists
new_line
SOCKETput_new_line
require IO_MEDIUM
extendible: extendible
require else
socket_exists: exists
opened_for_write: is_open_write
put_boolean (b: BOOLEAN)
b
SOCKETputbool
require IO_MEDIUM
extendible: extendible
require else
socket_exists: exists
opened_for_write: is_open_write
put_character (c: CHARACTER)
c
SOCKETputchar
require IO_MEDIUM
extendible: extendible
require else
socket_exists: exists
opened_for_write: is_open_write
put_double (d: DOUBLE)
d
SOCKETputdouble
require IO_MEDIUM
extendible: extendible
require else
socket_exists: exists
opened_for_write: is_open_write
put_integer (i: INTEGER)
i
SOCKETputint
require IO_MEDIUM
extendible: extendible
require else
socket_exists: exists
opened_for_write: is_open_write
put_new_line
SOCKETnew_line
require IO_MEDIUM
extendible: extendible
require else
socket_exists: exists
opened_for_write: is_open_write
put_real (r: REAL)
r
SOCKETputreal
require IO_MEDIUM
extendible: extendible
require else
socket_exists: exists
opened_for_write: is_open_write
put_string (s: STRING)
s
SOCKETputstring
require IO_MEDIUM
extendible: extendible
non_void: s /= void
require else
socket_exists: exists
opened_for_write: is_open_write
putbool (b: BOOLEAN)
b
SOCKETput_boolean
require IO_MEDIUM
extendible: extendible
require else
socket_exists: exists
opened_for_write: is_open_write
putchar (c: CHARACTER)
c
SOCKETput_character
require IO_MEDIUM
extendible: extendible
require else
socket_exists: exists
opened_for_write: is_open_write
putdouble (d: DOUBLE)
d
SOCKETput_double
require IO_MEDIUM
extendible: extendible
require else
socket_exists: exists
opened_for_write: is_open_write
putint (i: INTEGER)
i
SOCKETput_integer
require IO_MEDIUM
extendible: extendible
require else
socket_exists: exists
opened_for_write: is_open_write
putreal (r: REAL)
r
SOCKETput_real
require IO_MEDIUM
extendible: extendible
require else
socket_exists: exists
opened_for_write: is_open_write
putstring (s: STRING)
s
SOCKETput_string
require IO_MEDIUM
extendible: extendible
non_void: s /= void
require else
socket_exists: exists
opened_for_write: is_open_write
readable: BOOLEAN
require IO_MEDIUM
handle_exists: exists
send (a_packet: PACKET; flags: INTEGER)
a_packet
require
socket_exists: exists
opened_for_write: is_open_write
valid_packet: a_packet /= void
write (a_packet: PACKET)
a_packet
require
socket_exists: exists
opened_for_write: is_open_write
feature
debug_enabled: BOOLEAN
require
socket_exists: exists
disable_debug
require
socket_exists: exists
do_not_route
require
socket_exists: exists
enable_debug
require
socket_exists: exists
group_id: INTEGER
require
socket_exists: exists
group_set: is_group_id
is_blocking: BOOLEAN
is_group_id: BOOLEAN
require
socket_exists: exists
is_process_id: BOOLEAN
require
socket_exists: exists
is_socket_stream: BOOLEAN
require
socket_exists: exists
process_id: INTEGER
require
socket_exists: exists
process_set: is_process_id
receive_buf_size: INTEGER
require
socket_exists: exists
route
require
socket_exists: exists
route_enabled: BOOLEAN
require
socket_exists: exists
send_buf_size: INTEGER
require
socket_exists: exists
set_blocking
require
socket_exists: exists
ensure
is_blocking
set_non_blocking
require
socket_exists: exists
ensure
not is_blocking
set_owner (own: INTEGER)
require
socket_exists: exists
valid_owner: own /= 0 and own /= - 1
ensure
set_id: own < - 1 implies own = group_id or else own > 0 implies own = process_id
set_receive_buf_size (s: INTEGER)
require
socket_exists: exists
ensure
size_set: s = receive_buf_size
set_send_buf_size (s: INTEGER)
s
require
socket_exists: exists
ensure
size_set: s = send_buf_size
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- SOCKET