Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

java.net
Class URL

java.lang.Object
  extended byjava.net.URL
All Implemented Interfaces:
Serializable
public final class URL
extends Object
implements Serializable

JML's specification of java.net.URL. [[[This specification is still incomplete.]]]

Author:
Katie Becker, Gary T. Leavens

Class Specifications

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
 String authority
           
static JMLDataGroup factory
           
 String file
           
 URLStreamHandler handler
           
 String host
           
 String path
           
 int port
           
 String protocol
           
 String query_
           
 String ref
           
 String scheme
           
 String userInfo
           
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Constructor Summary
URL(String spec)
           
URL(String protocol, String host, int port, String file)
           
URL(String protocol, String host, int port, String file, URLStreamHandler handler)
           
URL(String protocol, String host, String file)
           
URL(URL context, String spec)
           
URL(URL context, String spec, URLStreamHandler handler)
           
 
Model Method Summary
 String getPath(String file)
           
 String getQuery(String file)
           
 String getRef(String file)
           
 boolean hasEquivalentHosts(String host)
           
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 boolean equals(nullable Object obj)
           
 String getAuthority()
           
 Object getContent()
           
 Object getContent(Class[] classes)
           
 int getDefaultPort()
           
 String getFile()
           
 String getHost()
           
 String getPath()
           
 int getPort()
           
 String getProtocol()
           
 String getQuery()
           
 String getRef()
           
 String getUserInfo()
           
 int hashCode()
           
 URLConnection openConnection()
           
 InputStream openStream()
           
 boolean sameFile(URL other)
           
protected  void set(String protocol, String host, int port, String file, String ref)
           
protected  void set(String protocol, String host, int port, String authority, String userInfo, String path, String query_, String ref)
           
static void setURLStreamHandlerFactory(URLStreamHandlerFactory fac)
           
 String toExternalForm()
           
 String toString()
           
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
 

Model Field Detail

protocol

public String protocol

host

public String host

file

public String file

scheme

public String scheme

authority

public String authority

userInfo

public String userInfo

path

public String path

query_

public String query_

ref

public String ref

handler

public URLStreamHandler handler

port

public int port

factory

public static JMLDataGroup factory
Constructor Detail

URL

public URL(String protocol,
           String host,
           int port,
           String file)
    throws MalformedURLException
Throws:
MalformedURLException
Specifications: pure
public behavior
assignable protocol, host, file, port, handler, scheme, authority, userInfo, path, query_, ref;
ensures this.equals(new java.net.URL(protocol, host, port, file, null));
signals_only java.net.MalformedURLException;

URL

public URL(String protocol,
           String host,
           String file)
    throws MalformedURLException
Throws:
MalformedURLException
Specifications: pure
public behavior
assignable protocol, host, file, port, handler, scheme, authority, userInfo, path, query_, ref;
ensures this.equals(new java.net.URL(protocol, host, -1, file));
signals_only java.net.MalformedURLException;

URL

public URL(String protocol,
           String host,
           int port,
           String file,
           URLStreamHandler handler)
    throws MalformedURLException
Throws:
MalformedURLException
Specifications: pure
public behavior
assignable protocol, host, file, port, handler, scheme, authority, userInfo, path, query_, ref;
ensures this.protocol.equals(protocol.toLowerCase())&&this.port == port;
ensures (file == null) ==> this.file == null;
ensures (file != null) ==> (this.getQuery(file) != null ? this.file.equals(this.getPath(file)+"?"+this.getQuery(file)) : this.file.equals(this.getPath(file)));
ensures (host == null) ==> (this.authority == null&&(port == -1) ? this.authority.equals(host) : this.authority.equals(host+":"+port));
ensures (host != null&&host.indexOf(58) >= 0&&!host.startsWith("[")) ? this.host.equals("["+host+"]") : this.host == host;
ensures this.handler != null;
ensures (file == null) ? this.ref == null : this.ref.equals(this.getRef(file));
signals_only java.net.MalformedURLException, java.lang.SecurityException;

URL

public URL(String spec)
    throws MalformedURLException
Throws:
MalformedURLException
Specifications: pure
public behavior
assignable protocol, host, file, port, handler, scheme, authority, userInfo, path, query_, ref;
ensures this.equals(new java.net.URL(null, spec));
signals_only java.net.MalformedURLException;

URL

public URL(URL context,
           String spec)
    throws MalformedURLException
Throws:
MalformedURLException
Specifications: pure
public behavior
assignable protocol, host, file, port, handler, scheme, authority, userInfo, path, query_, ref;
ensures this.equals(new java.net.URL(context, spec, null));
signals_only java.net.MalformedURLException;

URL

public URL(URL context,
           String spec,
           URLStreamHandler handler)
    throws MalformedURLException
Throws:
MalformedURLException
Specifications: pure
public behavior
assignable protocol, host, file, port, handler, scheme, authority, userInfo, path, query_, ref;
ensures this.handler != null;
signals_only java.net.MalformedURLException, java.lang.SecurityException;
Model Method Detail

hasEquivalentHosts

public boolean hasEquivalentHosts(String host)
Specifications: pure
public normal_behavior
ensures \result <==> (host == null&&this.host == null)||(this.host.equals(host))||(* the host names resolve to the same IP addresses *);

getPath

public String getPath(String file)
Specifications: pure
public normal_behavior
requires file != null;
ensures \result != null;
ensures file.indexOf(35) < 0 ==> (file.lastIndexOf(63) != -1 ? \result .equals(file.substring(0,file.lastIndexOf(63))) : \result .equals(file));
ensures file.indexOf(35) >= 0 ==> (file.substring(0,file.indexOf(35)).lastIndexOf(63) != -1 ? \result .equals(file.substring(0,file.indexOf(35)).substring(0,file.lastIndexOf(63))) : \result .equals(file.substring(0,file.indexOf(35))));

getQuery

public String getQuery(String file)
Specifications: pure
public normal_behavior
requires file != null;
ensures file.indexOf(35) < 0 ==> (file.lastIndexOf(63) != -1 ? \result .equals(file.substring(file.lastIndexOf(63)+1)) : \result == null);
ensures file.indexOf(35) >= 0 ==> (file.substring(0,file.indexOf(35)).lastIndexOf(63) != -1 ? \result .equals(file.substring(0,file.indexOf(35)).substring(file.lastIndexOf(63)+1)) : \result == null);

getRef

public String getRef(String file)
Specifications: pure
public normal_behavior
requires file != null;
ensures (file.indexOf(35) < 0) ? \result == null : \result .equals(file.substring(file.indexOf(35)+1));
Method Detail

set

protected void set(String protocol,
                   String host,
                   int port,
                   String file,
                   String ref)
Specifications:
protected normal_behavior
assignable protocol, host, file, port, authority, path, query_, ref;
ensures this.protocol.equals(protocol)&&this.host.equals(host)&&this.port == port&&this.file.equals(file)&&this.ref.equals(ref);
ensures (port == -1) ? this.authority.equals(host) : this.authority.equals(host+":"+port);
ensures (file.lastIndexOf(63) != -1) ? this.query_.equals(file.substring(file.lastIndexOf(63)))&&this.path.equals(file.substring(0,file.lastIndexOf(63))) : this.path.equals(file);

set

protected void set(String protocol,
                   String host,
                   int port,
                   String authority,
                   String userInfo,
                   String path,
                   String query_,
                   String ref)
Specifications:
protected normal_behavior
assignable protocol, host, file, port, authority, userInfo, path, query_, ref;
ensures this.protocol.equals(protocol)&&this.host.equals(host)&&this.port == port&&this.authority.equals(authority)&&this.userInfo.equals(userInfo)&&this.path.equals(path)&&this.query_.equals(query_)&&this.ref.equals(ref);
ensures query_ == null ? this.file.equals(path) : this.file.equals(path+"?"+query_);

getQuery

public String getQuery()
Specifications: pure
public normal_behavior
ensures \result .equals(this.query_);

getPath

public String getPath()
Specifications: pure
public normal_behavior
ensures \result .equals(this.path);

getUserInfo

public String getUserInfo()
Specifications: pure
public normal_behavior
ensures \result .equals(this.userInfo);

getAuthority

public String getAuthority()
Specifications: pure
public normal_behavior
ensures \result .equals(this.authority);

getPort

public int getPort()
Specifications: pure
public normal_behavior
ensures \result == this.port;

getDefaultPort

public int getDefaultPort()
Specifications: pure
public normal_behavior
ensures \result == -1 <==> (* the URL scheme or the URLStreamHandler does not have a default port *);

getProtocol

public String getProtocol()
Specifications: pure
public normal_behavior
ensures \result .equals(this.protocol);

getHost

public String getHost()
Specifications: pure
public normal_behavior
ensures \result .equals(this.host);

getFile

public String getFile()
Specifications: pure
public normal_behavior
ensures \result .equals(this.file);

getRef

public String getRef()
Specifications: pure
public normal_behavior
ensures \result .equals(this.ref);

equals

public boolean equals(nullable Object obj)
Overrides:
equals in class Object
Specifications: pure
     also
public normal_behavior
requires obj instanceof java.net.URL;
ensures \result <==> org.jmlspecs.models.JMLNullSafe.equals(((java.net.URL)obj).protocol,this.protocol)&&this.hasEquivalentHosts(((java.net.URL)obj).host)&&((java.net.URL)obj).port == this.port&&org.jmlspecs.models.JMLNullSafe.equals(((java.net.URL)obj).file,this.file)&&org.jmlspecs.models.JMLNullSafe.equals(((java.net.URL)obj).ref,this.ref);
     also
public normal_behavior
requires !(obj instanceof java.net.URL);
ensures \result == false;
Specifications inherited from overridden method equals(Object obj) in class Object:
       pure
public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);
     also
public normal_behavior
requires this == obj;
ensures \result ;
     also
public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;
     also
diverges false;
ensures obj == null ==> !\result ;

hashCode

public int hashCode()
Overrides:
hashCode in class Object
Specifications: pure
     also
public normal_behavior
assignable \nothing;
Specifications inherited from overridden method in class Object:
public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);
     also
public code normal_behavior
assignable \nothing;

sameFile

public boolean sameFile(URL other)
Specifications: pure
public normal_behavior
ensures \result <==> this.protocol.equals(other.protocol)&&this.host.equals(other.host)&&this.port == other.port&&this.path.equals(other.path);

toString

public String toString()
Overrides:
toString in class Object
Specifications: pure
     also
public normal_behavior
ensures \result .equals(this.toExternalForm());
Specifications inherited from overridden method in class Object:
       non_null
public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);
     also
public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);
     also
public code model_program { ... }
    implies_that
assignable objectState;
ensures \result != null;

toExternalForm

public String toExternalForm()
Specifications: pure
public normal_behavior
ensures \result != null;

openConnection

public URLConnection openConnection()
                             throws IOException
Throws:
IOException
Specifications: pure
public behavior
ensures \result != null;
signals_only java.io.IOException;

openStream

public final InputStream openStream()
                             throws IOException
Throws:
IOException
Specifications: pure
public behavior
ensures \result .equals(this.openConnection().getInputStream());
signals_only java.io.IOException;

getContent

public final Object getContent()
                        throws IOException
Throws:
IOException
Specifications: pure
public behavior
ensures \result .equals(this.openConnection().getContent());
signals_only java.io.IOException;

getContent

public final Object getContent(Class[] classes)
                        throws IOException
Throws:
IOException
Specifications: pure
public behavior
ensures \result .equals(this.openConnection().getContent(classes));
signals_only java.io.IOException;

setURLStreamHandlerFactory

public static void setURLStreamHandlerFactory(URLStreamHandlerFactory fac)
Specifications:
public behavior
assignable factory;
ensures java.net.URL.factory.equals(fac);
signals_only java.lang.SecurityException;
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD
JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.