class interface IP_ADDRESS creation make -- Create or reset IP address. ensure reset: b1 = 0 and b2 = 0 and b3 = 0 and b4 = 0 feature(s) from IP_ADDRESS -- Reset make -- Create or reset IP address. ensure reset: b1 = 0 and b2 = 0 and b3 = 0 and b4 = 0 feature(s) from IP_ADDRESS -- Reset reset -- Create or reset IP address. ensure reset: b1 = 0 and b2 = 0 and b3 = 0 and b4 = 0 feature(s) from IP_ADDRESS -- Address b1: INTEGER -- Address components. feature(s) from IP_ADDRESS -- Address b2: INTEGER -- Address components. feature(s) from IP_ADDRESS -- Address b3: INTEGER -- Address components. feature(s) from IP_ADDRESS -- Address b4: INTEGER -- Address components. last_result: BOOLEAN -- Result of side-effect procedure(s). feature(s) from IP_ADDRESS -- Status to_string: STRING -- Standard decimal representation. -- ("127.0.0.1") ensure is_copy: Result /= Void feature(s) from IP_ADDRESS -- Change set (v1, v2, v3, v4: INTEGER) -- Set address from components. require valid_values: -- see invariant set_string (str: STRING) -- Set from string representation ("127.0.0.1"). require ok: str /= Void feature(s) from IP_ADDRESS -- Name resolution resolve_by_name (nm: STRING) -- Find TCP/IP address from Fully Qualified Domain Name by -- asking the Domain Name Service (DNS). This is a blocking call. require ok: nm /= Void; -- may take several seconds blocking: ensure done: -- last_result implies address set feature(s) from IP_ADDRESS -- GENERAL out: STRING -- Standard string representation. is_equal (other: like Current): BOOLEAN -- Equality. require other_not_void: other /= Void ensure consistent: standard_is_equal(other) implies Result; symmetric: Result implies other.is_equal(Current) copy (other: like Current) -- Copy address. require other_not_void: other /= Void ensure is_equal: is_equal(other) invariant address_ok: b1 >= 0 and b1 <= 255 and b2 >= 0 and b2 <= 255 and b3 >= 0 and b3 <= 255 and b4 >= 0 and b4 <= 255; end of IP_ADDRESS