indexing
description: "A host address."
status: "See notice at end of class"
date: "$Date$"
revision: "$Revision$"
class interface
HOST_ADDRESS
create
make
make_local
make_from_name (a_name: STRING)
a_name
make_from_ip_number (an_ip_address: STRING)
feature
make
make_from_ip_number (an_ip_address: STRING)
make_from_name (a_name: STRING)
a_name
make_local
feature
address_host: SPECIAL [CHARACTER]
TO_SPECIAL
feature
count: INTEGER
feature
is_equal (other: like Current): BOOLEAN
require ANY
other_not_void: other /= void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
feature
from_c (ptr: POINTER)
feature
copy (other: like Current)
other
clone
require ANY
other_not_void: other /= void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
ensure then
new_result_count: count = other.count or else count = in_addr_size
feature
host_address: STRING
host_number: INTEGER
local_host_name: STRING
feature
set_address_from_name (a_name: STRING)
require
name_valid: a_name /= void and then not a_name.is_empty
set_host_address (host_id: STRING)
require
dotted_address_not_void: host_id /= void
set_in_address_any
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- HOST_ADDRESS