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 final class URL extends java.lang.Object implements java.io.Serializable
  {
     final static long serialVersionUID = -7627629688361524110L;
     java.net.InetAddress hostAddress;
     java.net.URLStreamHandler handler;
     static java.net.URLStreamHandlerFactory factory;
     static java.util.Hashtable handlers;
  
  
     /*@ requires true; ensures true; assignable \everything; signals (java.net.MalformedURLException e) true; */
     public URL(java.lang.String arg0, java.lang.String arg1, int arg2, java.lang.String arg3) throws java.net.MalformedURLException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.net.MalformedURLException e) true; */
     public URL(java.lang.String arg0, java.lang.String arg1, java.lang.String arg2) throws java.net.MalformedURLException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.net.MalformedURLException e) true; */
     public URL(java.lang.String arg0, java.lang.String arg1, int arg2, java.lang.String arg3, java.net.URLStreamHandler arg4) throws java.net.MalformedURLException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.net.MalformedURLException e) true; */
     public URL(java.lang.String arg0) throws java.net.MalformedURLException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.net.MalformedURLException e) true; */
     public URL(java.net.URL arg0, java.lang.String arg1) throws java.net.MalformedURLException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.net.MalformedURLException e) true; */
     public URL(java.net.URL arg0, java.lang.String arg1, java.net.URLStreamHandler arg2) throws java.net.MalformedURLException;
  
     /*@ requires true; ensures true; assignable \everything; */
     protected void set(java.lang.String arg0, java.lang.String arg1, int arg2, java.lang.String arg3, java.lang.String arg4);
  
     /*@ requires true; ensures true; assignable \everything; */
     protected void set(java.lang.String arg0, java.lang.String arg1, int arg2, java.lang.String arg3, java.lang.String arg4, java.lang.String arg5, java.lang.String arg6, java.lang.String arg7);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getQuery();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getPath();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getUserInfo();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getAuthority();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int getPort();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int getDefaultPort();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getProtocol();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getHost();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getFile();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String getRef();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean equals(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int hashCode();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean sameFile(java.net.URL arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toString();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toExternalForm();
  
     /*@ requires true; ensures true; assignable \everything; signals (java.net.URISyntaxException e) true; */
     public java.net.URI toURI() throws java.net.URISyntaxException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public java.net.URLConnection openConnection() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public java.net.URLConnection openConnection(java.net.Proxy arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public final java.io.InputStream openStream() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public final java.lang.Object getContent() throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; signals (java.io.IOException e) true; */
     public final java.lang.Object getContent(java.lang.Class[] arg0) throws java.io.IOException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public static void setURLStreamHandlerFactory(java.net.URLStreamHandlerFactory arg0);
  }
  