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