JML

java.lang
Class Package

java.lang.Object
  extended byjava.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
Constructor Detail

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

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

JML

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.