content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.net;
  
  public class InetAddress extends java.lang.Object implements java.io.Serializable
  {
     final static int IPv4 = 1;
     final static int IPv6 = 2;
     static boolean preferIPv6Address;
     final java.net.InetAddress$InetAddressHolder holder;
     static java.net.InetAddress[] unknown_array;
     static java.net.InetAddressImpl impl;
     final static boolean $assertionsDisabled;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isMulticastAddress();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isAnyLocalAddress();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isLoopbackAddress();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isLinkLocalAddress();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isSiteLocalAddress();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isMCGlobal();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isMCNodeLocal();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isMCLinkLocal();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isMCSiteLocal();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isMCOrgLocal();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public boolean isReachable(int arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public boolean isReachable(java.net.NetworkInterface arg0, int arg1, int arg2) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getHostName();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getCanonicalHostName();
  
     /*@ requires true; ensures true; assignable \everything; */
     public byte[] getAddress();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getHostAddress();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int hashCode();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean equals(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toString();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.net.UnknownHostException e) true; */
     public static java.net.InetAddress getByAddress(java.lang.String arg0, byte[] arg1) throws java.net.UnknownHostException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.net.UnknownHostException e) true; */
     public static java.net.InetAddress getByName(java.lang.String arg0) throws java.net.UnknownHostException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.net.UnknownHostException e) true; */
     public static java.net.InetAddress[] getAllByName(java.lang.String arg0) throws java.net.UnknownHostException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.net.InetAddress getLoopbackAddress();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.net.UnknownHostException e) true; */
     public static java.net.InetAddress getByAddress(byte[] arg0) throws java.net.UnknownHostException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.net.UnknownHostException e) true; */
     public static java.net.InetAddress getLocalHost() throws java.net.UnknownHostException;
  }
  