java.lang
Class Package

java.lang.Object
  java.lang.Package

public class Package

extends Object

JML's specification of java.lang.Package

Version:

$Revision: 1.15 $

Author:

Gary T. Leavens

Class Specifications

represents name <- this.getName(); represents spectitle <- this.getSpecificationTitle(); represents specversion <- this.getSpecificationVersion(); represents specvendor <- this.getSpecificationVendor(); represents impltitle <- this.getImplementationTitle(); represents implversion <- this.getImplementationVersion(); represents implvendor <- this.getImplementationVendor();

Specifications inherited from class Object

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

Model Field Summary
String	impltitle
String	implvendor
String	implversion
String	name
URL	sealbase
String	spectitle
String	specvendor
String	specversion

 

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
(package private)	Package(String name, String spectitle, String specversion, String specvendor, String impltitle, String implversion, String implvendor, URL sealbase)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
String	getImplementationTitle()
String	getImplementationVendor()
String	getImplementationVersion()
String	getName()
(package private) static Package	getPackage(non_null Class c)
static Package	getPackage(non_null String name)
static Package[]	getPackages()
String	getSpecificationTitle()
String	getSpecificationVendor()
String	getSpecificationVersion()
(package private) static Package	getSystemPackage(non_null String name)
(package private) static Package[]	getSystemPackages()
int	hashCode()
boolean	isCompatibleWith(String desired)
boolean	isSealed()
boolean	isSealed(URL url)
String	toString()

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

name

public String name

spectitle

public String spectitle

specversion

public String specversion

specvendor

public String specvendor

impltitle

public String impltitle

implversion

public String implversion

implvendor

public String implvendor

sealbase

public URL sealbase

Package

Package(String name,
        String spectitle,
        String specversion,
        String specvendor,
        String impltitle,
        String implversion,
        String implvendor,
        URL sealbase)

Specifications: pure

normal_behavior
assignable objectState;
assignable this.name;
assignable this.spectitle, this.specversion, this.specvendor;
assignable this.impltitle, this.implversion, this.implvendor;
assignable this.sealbase;
ensures this.name == name;
ensures this.spectitle == spectitle&&this.specversion == specversion&&this.specvendor == specvendor;
ensures this.impltitle == impltitle&&this.implversion == implversion&&this.implvendor == implvendor;
ensures this.sealbase == sealbase;

getName

public String getName()

Specifications: pure

public normal_behavior
ensures this.name == null ==> \result == null;
ensures this.name != null ==> \result != null&&this.name.equals(\result );

getSpecificationTitle

public String getSpecificationTitle()

Specifications: pure

public normal_behavior
ensures this.spectitle == null ==> \result == null;
ensures this.spectitle != null ==> \result != null&&this.spectitle.equals(\result );

getSpecificationVersion

public String getSpecificationVersion()

Specifications: pure

public normal_behavior
ensures this.specversion == null ==> \result == null;
ensures this.specversion != null ==> \result != null&&this.specversion.equals(\result );

getSpecificationVendor

public String getSpecificationVendor()

Specifications: pure

public normal_behavior
ensures this.specvendor == null ==> \result == null;
ensures this.specvendor != null ==> \result != null&&this.specvendor.equals(\result );

getImplementationTitle

public String getImplementationTitle()

Specifications: pure

public normal_behavior
ensures this.impltitle == null ==> \result == null;
ensures this.impltitle != null ==> \result != null&&this.impltitle.equals(\result );

getImplementationVersion

public String getImplementationVersion()

Specifications: pure

public normal_behavior
ensures this.implversion == null ==> \result == null;
ensures this.implversion != null ==> \result != null&&this.implversion.equals(\result );

getImplementationVendor

public String getImplementationVendor()

Specifications: pure

public normal_behavior
ensures this.implvendor == null ==> \result == null;
ensures this.implvendor != null ==> \result != null&&this.implvendor.equals(\result );

isSealed

public boolean isSealed()

Specifications: pure

public normal_behavior
ensures \result <==> this.sealbase != null;

isSealed

public boolean isSealed(URL url)

Specifications: pure

public normal_behavior
requires url != null;
ensures \result <==> this.sealbase != null&&this.sealbase.equals(url);

     also

public exceptional_behavior
requires url == null;
signals_only java.lang.NullPointerException;

isCompatibleWith

public boolean isCompatibleWith(String desired)
                         throws NumberFormatException

Throws:

NumberFormatException

Specifications: pure

ensures desired.equals(this.getSpecificationVersion()) ==> \result ;

getPackage

public static Package getPackage(non_null String name)

Specifications: pure

ensures \result != null ==> \result .getName().equals(name.replace('/','.'));
ensures getPackage("java.lang") != null;
ensures getPackage("java/lang") != null;
ensures getPackage("java") == null;
ensures getPackage("lang") == null;
ensures getPackage("") == null;
ensures getPackage("ZZZZZ") == null;

getPackages

public static Package[] getPackages()

Specifications: pure non_null

ensures \result != null&&( \forall int i; 0 <= i&&i < \result .length; getPackage(\result [i].getName()) != null);
ensures ( \forall java.lang.String s; s != null; (( \exists int i; 0 <= i&&i < \result .length; getPackage(s) == \result [i]) <==> getPackage(s) != null));
ensures ( \exists int i; 0 <= i&&i < \result .length; \result [i] == getPackage("java.lang"));

getPackage

static Package getPackage(non_null Class c)

Specifications: pure

hashCode

public int hashCode()

Overrides:

hashCode in class Object

Specifications: pure

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;

toString

public String toString()

Overrides:

toString in class Object

Specifications: pure non_null

     also

ensures \result .startsWith("package "+this.getName());

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;

getSystemPackage

static Package getSystemPackage(non_null String name)

Specifications: pure

getSystemPackages

static Package[] getSystemPackages()

Specifications: pure non_null