URI (JML and MultiJava documentation)

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 URI

java.lang.Object
  java.net.URI

All Implemented Interfaces:: Comparable, Serializable

public final class URI
extends Object
implements Comparable, Serializable

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

Author:: Denise Bacher, Katie Becker, Gary T. Leavens

Class Specifications

public invariant this.isOpaque() ==> this.userInfo == null&&this.host == null&&this.path == null&&this.query_ == null&&this.authority == null&&this.port == -1;
public represents needsBrackets <- ((this.host.indexOf(58) >= 0)&&!this.host.startsWith("[")&&!this.host.endsWith("]")&&(!this.isOpaque())&&(this.host != null));

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Specifications inherited from interface Comparable

instance public invariant ( \forall java.lang.Comparable x; x != null; x.compareTo(x) == 0);
instance public invariant ( \forall java.lang.Comparable x, y; x != null&&y != null&&this.definedComparison(x,y)&&this.definedComparison(y,x); this.sgn(x.compareTo(y)) == -this.sgn(y.compareTo(x)));
instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == n ==> this.sgn(x.compareTo(z)) == n));
instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); (this.sgn(x.compareTo(y)) == 0&&this.sgn(y.compareTo(z)) == n||this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == 0) ==> this.sgn(x.compareTo(z)) == n));
instance public invariant ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(x,z)&&this.definedComparison(y,z); this.sgn(x.compareTo(y)) == 0 ==> this.sgn(x.compareTo(z)) == this.sgn(y.compareTo(z)));

Model Field Summary

String authority


String fragment


String host


boolean needsBrackets


String path


int port


String query_


String scheme


String ssp


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

URI(String str)


URI(String scheme, String ssp, String fragment)


URI(String scheme, String userInfo, String host, int port, String path, String query_, String fragment)


URI(String scheme, String host, String path, String fragment)


URI(String scheme, String authority, String path, String query_, String fragment)


Model Method Summary

String asASCII(String str)


String fromASCII(String str)


String pathNormalize(String path)


Model methods inherited from class java.lang.Object

hashValue

Model methods inherited from interface java.lang.Comparable

definedComparison, sgn

Method Summary

int compareTo(non_null Object ob)


static URI create(String str)


boolean equals(nullable Object ob)


String getAuthority()


String getFragment()


String getHost()


String getPath()


int getPort()


String getQuery()


String getRawAuthority()


String getRawFragment()


String getRawPath()


String getRawQuery()


String getRawSchemeSpecificPart()


String getRawUserInfo()


String getScheme()


String getSchemeSpecificPart()


String getUserInfo()


int hashCode()


boolean isAbsolute()


boolean isOpaque()


URI normalize()


URI parseServerAuthority()


URI relativize(URI uri)


URI resolve(String str)


URI resolve(URI uri)


String toASCIIString()


String toString()


URL toURL()


Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Model Field Detail

scheme

public String scheme

ssp

public String ssp

fragment

public String fragment

userInfo

public String userInfo

host

public String host

path

public String path

query_

public String query_

authority

public String authority

port

public int port

needsBrackets

public boolean needsBrackets

Constructor Detail

URI

public URI(String str)
    throws URISyntaxException

Throws:: URISyntaxException

URI

public URI(String scheme,
           String userInfo,
           String host,
           int port,
           String path,
           String query_,
           String fragment)
    throws URISyntaxException

Throws:: URISyntaxException

Specifications:: public behavior
assignable scheme, userInfo, host, port, path, query_, fragment, ssp, authority;
ensures org.jmlspecs.models.JMLNullSafe.equals(this.scheme,scheme)&&org.jmlspecs.models.JMLNullSafe.equals(this.userInfo,userInfo)&&org.jmlspecs.models.JMLNullSafe.equals(this.host,host)&&this.port == port&&org.jmlspecs.models.JMLNullSafe.equals(this.path,path)&&org.jmlspecs.models.JMLNullSafe.equals(this.query_,query_)&&org.jmlspecs.models.JMLNullSafe.equals(this.fragment,fragment);
ensures this.authority == null&&this.ssp == null;
ensures (scheme == null) ==> host != null&&((host.startsWith("/")||host.equals("")));
signals_only java.net.URISyntaxException;

URI

public URI(String scheme,
           String authority,
           String path,
           String query_,
           String fragment)
    throws URISyntaxException

Throws:: URISyntaxException

Specifications:: public behavior
assignable scheme, userInfo, host, port, path, query_, fragment, ssp, authority;
ensures org.jmlspecs.models.JMLNullSafe.equals(this.scheme,scheme)&&org.jmlspecs.models.JMLNullSafe.equals(this.authority,authority)&&org.jmlspecs.models.JMLNullSafe.equals(this.path,path)&&org.jmlspecs.models.JMLNullSafe.equals(this.query_,query_)&&org.jmlspecs.models.JMLNullSafe.equals(this.fragment,fragment);
ensures this.userInfo == null&&this.host == null&&this.port == -1&&this.ssp == null;
ensures (scheme == null) ==> path != null&&((path.startsWith("/")||path.equals("")));
signals_only java.net.URISyntaxException;

URI

public URI(String scheme,
           String host,
           String path,
           String fragment)
    throws URISyntaxException

Throws:: URISyntaxException

Specifications:: public behavior
assignable scheme, userInfo, host, port, path, query_, fragment, ssp, authority;
ensures org.jmlspecs.models.JMLNullSafe.equals(this.scheme,scheme)&&org.jmlspecs.models.JMLNullSafe.equals(this.host,host)&&org.jmlspecs.models.JMLNullSafe.equals(this.path,path)&&org.jmlspecs.models.JMLNullSafe.equals(this.fragment,fragment);
ensures this.userInfo == null&&this.authority == null&&this.port == -1&&this.query_ == null&&this.ssp == null;
ensures (scheme == null) ==> path != null&&((path.startsWith("/")||path.equals("")));
signals_only java.net.URISyntaxException;

URI

public URI(String scheme,
           String ssp,
           String fragment)
    throws URISyntaxException

Throws:: URISyntaxException

Specifications:: public behavior
assignable scheme, userInfo, host, port, path, query_, fragment, ssp, authority;
ensures org.jmlspecs.models.JMLNullSafe.equals(this.scheme,scheme)&&org.jmlspecs.models.JMLNullSafe.equals(this.ssp,ssp)&&org.jmlspecs.models.JMLNullSafe.equals(this.fragment,fragment);
ensures this.userInfo == null&&this.host == null&&this.port == -1&&this.authority == null&&this.query_ == null&&this.ssp == null;
signals_only java.net.URISyntaxException;

Model Method Detail

pathNormalize

public String pathNormalize(String path)

Specifications: pure

asASCII

public String asASCII(String str)

Specifications: pure

fromASCII

public String fromASCII(String str)

Specifications: pure

Method Detail

create

public static URI create(String str)

Specifications: pure non_null: public behavior
requires str != null;
signals (java.lang.IllegalArgumentException) (* the given string violates RFC 2396 *);
signals_only java.lang.IllegalArgumentException;

parseServerAuthority

public URI parseServerAuthority()
                         throws URISyntaxException

Throws:: URISyntaxException

Specifications: pure: public normal_behavior
requires this.authority == null;
ensures \result .equals(this);
also: public behavior
requires (this.authority != null);
signals_only java.net.URISyntaxException;

normalize

public URI normalize()

Specifications:: requires this.isOpaque();
ensures \result == this;
also: requires !this.isOpaque();
ensures \result .path.equals(this.pathNormalize(this.path));

resolve

public URI resolve(URI uri)

Specifications: pure non_null

public normal_behavior
requires uri.isAbsolute()||this.isOpaque();
assignable \nothing;
ensures \result == uri;

also

public normal_behavior
requires uri.fragment != null&&(uri.path != null||uri.path.equals(""))&&uri.scheme == null&&uri.authority == null&&uri.query_ == null;
requires_redundantly !uri.isAbsolute();
ensures \result .fragment.equals(uri.fragment)&&\result .ssp.equals(this.ssp)&&\result .scheme.equals(this.scheme)&&\result .userInfo.equals(this.userInfo)&&\result .host.equals(this.host)&&\result .path.equals(this.path)&&\result .query_.equals(this.query_)&&\result .port == this.port&&\result .authority.equals(this.authority);

also

public normal_behavior
requires !(uri.isAbsolute()||this.isOpaque())&&!(uri.fragment != null&&(uri.path != null||uri.path.equals(""))&&uri.scheme == null&&uri.authority == null&&uri.query_ == null);

requires uri.authority != null;
ensures \result .scheme.equals(this.scheme)&&\result .query_.equals(uri.query_)&&\result .fragment.equals(uri.fragment)&&\result .authority.equals(uri.authority)&&\result .path.equals(uri.path);
also: requires uri.authority == null;

{|
ensures \result .scheme.equals(this.scheme)&&\result .query_.equals(uri.query_)&&\result .fragment.equals(uri.fragment)&&\result .authority.equals(this.authority);

also

{|
requires uri.path != null&&uri.path.length() > 0&&uri.path.charAt(0) == 47;
ensures \result .path.equals(uri.path);

also
old java.lang.String thispath = (this.path == null ? "" : this.path);
requires uri.path == null||uri.path.length() == 0||uri.path.charAt(0) != 47;
ensures \result .path.equals(this.pathNormalize((thispath.indexOf(47) != -1 ? "" : this.path.substring(0,this.path.lastIndexOf("/")))+uri.path));

|}

|}
|}

implies_that

requires this.isAbsolute()||uri.isAbsolute();
ensures \result .isAbsolute();

also

requires !(this.isAbsolute()||uri.isAbsolute());
ensures !\result .isAbsolute();

resolve

public URI resolve(String str)

Specifications: pure non_null: public behavior
ensures \result == this.resolve(java.net.URI.create(str));

relativize

public URI relativize(URI uri)

Specifications: pure: public normal_behavior
requires (this.isOpaque()||uri.isOpaque())||(!this.scheme.equals(uri.scheme)&&!this.authority.equals(uri.authority))||!uri.path.startsWith(this.path);
ensures \result == uri;
also: public normal_behavior
requires !(this.isOpaque()&&uri.isOpaque())&&(this.scheme.equals(uri.scheme)||this.authority.equals(uri.authority))&&uri.path.startsWith(this.path);
ensures \result .query_.equals(uri.query_)&&\result .fragment.equals(this.fragment)&&\result .path.equals(uri.path.substring(this.path.length()));

toURL

public URL toURL()
          throws MalformedURLException

Throws:: MalformedURLException

Specifications: pure: public normal_behavior
requires this.isAbsolute();
also: public behavior
signals_only java.net.MalformedURLException;

getScheme

public String getScheme()

Specifications: pure: public normal_behavior
requires this.scheme == null;
ensures \result == null;
also: public normal_behavior
requires this.scheme != null;
ensures \result != null&&\result .equals(this.scheme);

isAbsolute

public boolean isAbsolute()

Specifications: pure: public normal_behavior
ensures \result <==> this.scheme != null;

isOpaque

public boolean isOpaque()

Specifications: pure: public normal_behavior
ensures \result <==> this.scheme != null&&!this.ssp.startsWith("/");

getRawSchemeSpecificPart

public String getRawSchemeSpecificPart()

Specifications: pure: public normal_behavior
requires this.ssp != null;
ensures \result != null;

getSchemeSpecificPart

public String getSchemeSpecificPart()

Specifications: pure: public normal_behavior
ensures \result != null;

getRawAuthority

public String getRawAuthority()

Specifications: pure: public normal_behavior
requires this.authority == null;
ensures \result == null;
also: public normal_behavior
requires this.authority != null;
ensures \result != null;

getAuthority

public String getAuthority()

Specifications: pure: public normal_behavior
requires this.authority == null;
ensures \result == null;
also: public normal_behavior
requires this.authority != null;
ensures \result != null;

getRawUserInfo

public String getRawUserInfo()

Specifications: pure: public normal_behavior
requires this.userInfo == null;
ensures \result == null;
also: public normal_behavior
requires this.userInfo != null;
ensures \result != null;

getUserInfo

public String getUserInfo()

Specifications: pure: public normal_behavior
requires this.userInfo == null;
ensures \result == null;
also: public normal_behavior
requires this.userInfo != null;
ensures \result != null;

getHost

public String getHost()

Specifications: pure: public normal_behavior
requires this.host == null;
ensures \result == null;
also: public normal_behavior
requires this.host != null;
ensures \result != null&&\result .equals(this.host);

getPort

public int getPort()

Specifications: pure: public normal_behavior
ensures \result == this.port;

getRawPath

public String getRawPath()

Specifications: pure: public normal_behavior
requires this.path == null;
ensures \result == null;
also: public normal_behavior
requires this.path != null;
ensures \result != null&&\result .equals(this.path);

getPath

public String getPath()

Specifications: pure: public normal_behavior
requires this.path == null;
ensures \result == null;
also: public normal_behavior
requires this.path != null;
ensures \result != null;

getRawQuery

public String getRawQuery()

Specifications: pure: public normal_behavior
requires this.query_ == null;
ensures \result == null;
also: public normal_behavior
requires this.query_ != null;
ensures \result != null;

getQuery

public String getQuery()

Specifications: pure: public normal_behavior
requires this.query_ == null;
ensures \result == null;
also: public normal_behavior
requires this.query_ != null;
ensures \result != null;

getRawFragment

public String getRawFragment()

Specifications: pure: public normal_behavior
requires this.fragment == null;
ensures \result == null;
also: public normal_behavior
requires this.fragment != null;
ensures \result != null;

getFragment

public String getFragment()

Specifications: pure: public normal_behavior
requires this.fragment == null;
ensures \result == null;
also: public normal_behavior
requires this.fragment != null;
ensures \result != null;

equals

public boolean equals(nullable Object ob)

Overrides:: equals in class Object

Specifications: pure

also

public normal_behavior
requires !(ob instanceof java.net.URI);
ensures !\result ;

also

public normal_behavior
old java.net.URI uri = (java.net.URI)ob;
requires ob instanceof java.net.URI;

requires this.isOpaque();
ensures \result <==> uri.isOpaque()&&this.getRawSchemeSpecificPart().equals(uri.getRawSchemeSpecificPart());
also: requires !this.isOpaque();
ensures \result <==> this.getRawPath().equals(uri.getRawPath())&&(this.getRawQuery().equals(uri.getRawQuery())||(this.getRawQuery() == null&&uri.getRawQuery() == null));
|}

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 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;

compareTo

public int compareTo(non_null Object ob)

Specified by:: compareTo in interface Comparable

Specifications: (inherited)pure
Specifications inherited from overridden method compareTo(Object o) in interface Comparable:
pure: public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);
also: public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);

toString

public String toString()

Overrides:: toString in class Object

Specifications: pure non_null

also

old java.lang.String prefix = (this.scheme != null ? this.scheme : "");
old java.lang.String suffix = (this.fragment != null ? "#"+this.fragment : "");

requires this.isOpaque();
ensures \result .equals(prefix+this.ssp+suffix);
also: old java.lang.String pq = (this.path != null ? this.path : "")+(this.query_ != null ? "?"+this.query_ : "");
requires !this.isOpaque();

{|
requires this.host != null;
ensures \result .equals(prefix+"//"+(this.userInfo != null ? this.userInfo+"@" : "")+(this.needsBrackets ? "[" : "")+this.host+(this.needsBrackets ? "]" : "")+(this.port != -1 ? ":"+this.port : "")+pq+suffix);

also
requires this.host == null;
ensures \result .equals(prefix+(this.authority != null ? "//"+this.authority : "")+pq+suffix);

|}
|}

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;

toASCIIString

public String toASCIIString()

Specifications: pure: public behavior
ensures \result == this.asASCII(this.toString());

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.

Model Field Summary
`String`	`authority`
`String`	`fragment`
`String`	`host`
`boolean`	`needsBrackets`
`String`	`path`
`int`	`port`
`String`	`query_`
`String`	`scheme`
`String`	`ssp`
`String`	`userInfo`

Constructor Summary
`URI(String str)`
`URI(String scheme, String ssp, String fragment)`
`URI(String scheme, String userInfo, String host, int port, String path, String query_, String fragment)`
`URI(String scheme, String host, String path, String fragment)`
`URI(String scheme, String authority, String path, String query_, String fragment)`

Model Method Summary
`String`	`asASCII(String str)`
`String`	`fromASCII(String str)`
`String`	`pathNormalize(String path)`

Method Summary
`int`	`compareTo(non_null Object ob)`
`static URI`	`create(String str)`
`boolean`	`equals(nullable Object ob)`
`String`	`getAuthority()`
`String`	`getFragment()`
`String`	`getHost()`
`String`	`getPath()`
`int`	`getPort()`
`String`	`getQuery()`
`String`	`getRawAuthority()`
`String`	`getRawFragment()`
`String`	`getRawPath()`
`String`	`getRawQuery()`
`String`	`getRawSchemeSpecificPart()`
`String`	`getRawUserInfo()`
`String`	`getScheme()`
`String`	`getSchemeSpecificPart()`
`String`	`getUserInfo()`
`int`	`hashCode()`
`boolean`	`isAbsolute()`
`boolean`	`isOpaque()`
`URI`	`normalize()`
`URI`	`parseServerAuthority()`
`URI`	`relativize(URI uri)`
`URI`	`resolve(String str)`
`URI`	`resolve(URI uri)`
`String`	`toASCIIString()`
`String`	`toString()`
`URL`	`toURL()`

java.net Class URI

scheme

ssp

fragment

userInfo

host

path

query_

authority

port

needsBrackets

URI

URI

URI

URI

URI

pathNormalize

asASCII

fromASCII

create

parseServerAuthority

normalize

resolve

resolve

relativize

toURL

getScheme

isAbsolute

isOpaque

getRawSchemeSpecificPart

getSchemeSpecificPart

getRawAuthority

getAuthority

getRawUserInfo

getUserInfo

getHost

getPort

getRawPath

getPath

getRawQuery

getQuery

getRawFragment

getFragment

equals

hashCode

compareTo

toString

toASCIIString

java.net
Class URI