jml2b.structure.java
Class Package

java.lang.Object
  jml2b.util.Profiler
      jml2b.structure.java.ParsedItem
          jml2b.structure.java.NamedNode
              jml2b.structure.java.Package

All Implemented Interfaces:

jml.JmlDeclParserTokenTypes, java.io.Serializable

public class Package

extends NamedNode

implements java.io.Serializable

class representing packages. It is the class from where all the known information is accessible.

Author:

A. Requet

See Also:

Serialized Form

Field Summary

java.lang.String	name Short name of the package.
Package	parent The parent package.

Fields inherited from class jml2b.structure.java.NamedNode

garbage, nameIndex

Fields inherited from interface jml.JmlDeclParserTokenTypes

ABRUPT_BEHAVIOR, ACCESSIBLE, ACCESSIBLE_KEYWORD, ACCESSIBLE_REDUNDANTLY, ACCESSIBLE_SEQ, ADDITIVE_ASSIGNMENT_OP, ADDITIVE_OP, AFFIRM_KEYWORD, ALSO, AND, ARRAY_DECLARATOR, ASGNABLE_SEQ, ASSERT, ASSERT_REDUNDANTLY, ASSIGN, ASSIGNABLE, ASSIGNABLE_KEYWORD, ASSIGNABLE_REDUNDANTLY, ASSUME, ASSUME_KEYWORD, ASSUME_REDUNDANTLY, AXIOM, BACKWARD_IMPLIES, BADCHAR, BAND, BAND_ASSIGN, BEHAVIOR, BITWISE_ASSIGNMENT_OP, BITWISE_OP, BNOT, BOR, BOR_ASSIGN, BREAKS, BREAKS_KEYWORD, BREAKS_REDUNDANTLY, BREAKS_SEQ, BSR, BSR_ASSIGN, BXOR, BXOR_ASSIGN, CALLABLE, CALLABLE_KEYWORD, CALLABLE_REDUNDANTLY, CALLABLE_SEQ, CASE, CAST, CHAR_LITERAL, CHOOSE, CHOOSE_IF, COLON, COMMA, CONJOINABLE_SPEC, CONSTRAINT, CONSTRAINT_KEYWORD, CONSTRAINT_REDUNDANTLY, CONSTRUCTOR, CONT_SEQ, CONTINUES, CONTINUES_KEYWORD, CONTINUES_REDUNDANTLY, DEC, DECREASES, DECREASES_REDUNDANTLY, DECREASING, DECREASING_KEYWORD, DECREASING_REDUNDANTLY, DEPENDS, DEPENDS_KEYWORD, DEPENDS_REDUNDANTLY, DIM_EXPRS, DIMS, DINFORMALLY, DIV, DIV_ASSIGN, DIV_SEQ, DIVERGES, DIVERGES_KEYWORD, DIVERGES_REDUNDANTLY, DOC_ATSIGN, DOC_ATSIGN_KEYWORD, DOC_AUTHOR, DOC_COMMENT, DOC_COMMENT_START, DOC_DEPRECATED, DOC_EXCEPTION, DOC_JML_SPECS, DOC_NL_WS, DOC_NON_EMPTY_TEXTLINE, DOC_NON_NL_WS, DOC_PARAM, DOC_RETURN, DOC_SEE, DOC_SERIAL, DOC_SERIALDATA, DOC_SERIALFIELD, DOC_SINCE, DOC_THROWS, DOC_UNKNOWN_KEYWORD, DOC_VERSION, DOT, DOT_DOT, ELSE, ENS_SEQ, ENSURES, ENSURES_KEYWORD, ENSURES_REDUNDANTLY, EOF, EQUAL, EQUALITY_OP, EQUIV, EQUIVALENCE_OP, ESC, EXAMPLE, EXCEPTIONAL_BEHAVIOR, EXCEPTIONAL_EXAMPLE, EXPONENT, EXSURES, EXSURES_REDUNDANTLY, EXT_ALSO, EXT_AND, FLOAT_SUFFIX, FOR, FOR_EXAMPLE, FOR_INIT, FOR_TEST, FOR_UPDATER, FORALL, GE, GHOST, GT, HENCE_BY, HENCE_BY_KEYWORD, HENCE_BY_REDUNDANTLY, HEX_DIGIT, IDENT, IGNORED_AT_IN_COMMENT, IMPLICATION_OP, IMPLIES_THAT, INC, INFORMAL_DESCRIPTION, INIT, INITIALIZER, INITIALLY, INSTANCE, INSTANCE_INIT, INVARIANT, INVARIANT_KEYWORD, INVARIANT_REDUNDANTLY, IS_SUBTYPE_OF, JAVA_BUILTIN_TYPE, JAVA_MODIFIER, JML_BACKSLASH_SEQUENCE, JML_MODIFIER, L_ARROW, LABEL, LABEL_KEYWORD, LAND, LBRACK, LCURLY, LCURLY_VBAR, LE, LET, LETOLD_KEYWORD, LIMPLIES, LITERAL_abstract, LITERAL_assert, LITERAL_boolean, LITERAL_break, LITERAL_byte, LITERAL_case, LITERAL_catch, LITERAL_char, LITERAL_class, LITERAL_const, LITERAL_continue, LITERAL_default, LITERAL_do, LITERAL_double, LITERAL_else, LITERAL_extends, LITERAL_false, LITERAL_final, LITERAL_finally, LITERAL_float, LITERAL_for, LITERAL_if, LITERAL_implements, LITERAL_import, LITERAL_instanceof, LITERAL_int, LITERAL_interface, LITERAL_long, LITERAL_native, LITERAL_new, LITERAL_null, LITERAL_package, LITERAL_private, LITERAL_protected, LITERAL_public, LITERAL_return, LITERAL_short, LITERAL_static, LITERAL_strictfp, LITERAL_super, LITERAL_switch, LITERAL_synchronized, LITERAL_this, LITERAL_throw, LITERAL_throws, LITERAL_transient, LITERAL_true, LITERAL_try, LITERAL_void, LITERAL_volatile, LITERAL_while, LNOT, LOGICAL_OP, LOOP_ASGNABLE_SEQ, LOOP_ASSIGNABLE_KEYWORD, LOOP_EXSURES, LOOP_INV_SEQ, LOOP_INVARIANT, LOOP_INVARIANT_REDUNDANTLY, LOOP_MODIFIES, LOOP_SIG_SEQ, LOR, LPAREN, LT, MAINTAINING, MAINTAINING_KEYWORD, MAINTAINING_REDUNDANTLY, MEASURED_BY, MEASURED_BY_KEYWORD, MEASURED_BY_REDUNDANTLY, METH, MINUS, MINUS_ASSIGN, ML_COMMENT, MOD, MOD_ASSIGN, MODEL, MODEL_PROGRAM, MODIFIABLE, MODIFIABLE_REDUNDANTLY, MODIFIER_SET, MODIFIES, MODIFIES_REDUNDANTLY, MONITORED, MONITORED_BY, MULTIPLICATIVE_ASSIGNMENT_OP, MULTIPLICATIVE_OP, NESTED_CLASS, NL_WS, NON_NL_WS, NON_NULL, NORMAL_BEHAVIOR, NORMAL_EXAMPLE, NOT_EQUAL, NOT_EQUIV, NOWARN_LABEL, NOWARN_LABEL_LIST, NULL_TREE_LOOKAHEAD, NUM_FLOAT, NUM_INT, OLD, OR, PARAM, PLUS, PLUS_ASSIGN, POST, POST_DEC, POST_INC, POST_INCREMENT_OP, POST_REDUNDANTLY, PRE, PRE_INCREMENT_OP, PRE_REDUNDANTLY, PRIVACY_MODIFIER, PURE, QUANT_VARS, QUANTIFIED_EXPR, QUANTIFIER_TOKEN, QUESTION, R_ARROW, RBRACK, RCURLY, READABLE_IF, REFINE, RELATIONAL_OP, REPLACE, REPRESENTS, REPRESENTS_KEYWORD, REPRESENTS_REDUNDANTLY, REQUIRES, REQUIRES_KEYWORD, REQUIRES_REDUNDANTLY, RETURNS, RETURNS_KEYWORD, RETURNS_REDUNDANTLY, RETURNS_SEQ, RPAREN, SEMI, SET, SET_COMPR, SHIFT_ASSIGNMENT_OP, SHIFT_OP, SIG_SEQ, SIGNALS, SIGNALS_KEYWORD, SIGNALS_REDUNDANTLY, SL, SL_ASSIGN, SL_COMMENT, SPEC_CASE, SPEC_PROTECTED, SPEC_PUBLIC, SPEC_SL_COMMENT, SPEC_STATEMENT, SR, SR_ASSIGN, STAR, STAR_ASSIGN, STAR_ELEMS, STATIC_INITIALIZER, STRING_LITERAL, SUBCLASSING_CONTRACT, T_ELEMTYPE, T_EVERYTHING, T_EXISTS, T_FIELDS_OF, T_FORALL, T_FRESH, T_INVARIANT_FOR, T_IS_INITIALIZED, T_LBLNEG, T_LBLPOS, T_LOCKSET, T_MAX, T_MIN, T_NONNULLELEMENTS, T_NOT_MODIFIED, T_NOT_SPECIFIED, T_NOTHING, T_NUM_OF, T_OLD, T_OTHER, T_PRODUCT, T_REACH, T_RESULT, T_SUCH_THAT, T_SUM, T_TYPE, T_TYPEOF, T_TYPEOFALLTYPES, UNARY_NUMERIC_OP, UNINITIALIZED, UNREACHABLE, VAR_DECL, VBAR_RCURLY, VF_SEQ, VOCAB, WEAKLY, WHEN, WHEN_KEYWORD, WHEN_REDUNDANTLY, WS

Constructor Summary

Package(java.lang.String name)

Method Summary

void	addClass(AClass c)
void	addPackage(Package p)
static void	clearAll() Unload all the loaded packages.
Package	createAndCheckSubPackage(IJml2bConfiguration config, java.lang.String name) Check that the package name exists and create the subpackage if it does.
Package	createSubPackage(java.lang.String name)
AClass	getAndLoadClass(IJml2bConfiguration config, java.lang.String name) Return a reference to the class name.
Package	getAndLoadPackage(java.lang.String name)
AClass	getClass(java.lang.String name) Search for the given class inside this package.
int	getClassCount(boolean include_subpackages) Return the number of classes in this package.
java.util.Enumeration	getClasses()
java.lang.String	getDirectory() return the directory corresponding to this package.
java.lang.String	getFullyQualifiedName() Returns the fully qualified name of this package.
static Package	getJavaLang()
java.lang.String	getName()
Package	getPackage(java.lang.String name) Search for the given package inside this package.
Package	getParent()
static Package	getRoot()
java.util.Enumeration	getSubPackages()
static boolean	initFromFile(java.lang.String file_name) Inits the root package (java.lang, etc...) from the given serialized file.
boolean	keepPackageVisible()
static boolean	restoreDefaultPackages(Package root)
AClass	searchClass(java.lang.String s)
void	setKeepPackage(boolean val)

Methods inherited from class jml2b.structure.java.NamedNode

clearName, getBName, hasBName, newName

Methods inherited from class jml2b.structure.java.ParsedItem

change, change, getColumn, getJmlFile, getLine, save, setBox

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

name

public java.lang.String name

Short name of the package.

parent

public Package parent

The parent package.

Constructor Detail

Package

public Package(java.lang.String name)

Method Detail

getSubPackages

public java.util.Enumeration getSubPackages()

getClasses

public java.util.Enumeration getClasses()

getName

public java.lang.String getName()

Specified by:

getName in class NamedNode

getParent

public Package getParent()

keepPackageVisible

public boolean keepPackageVisible()

setKeepPackage

public void setKeepPackage(boolean val)

getClassCount

public int getClassCount(boolean include_subpackages)

Return the number of classes in this package. If include_subpackage is true, count the number of classes in the subpackages.

addPackage

public void addPackage(Package p)

addClass

public void addClass(AClass c)

getPackage

public Package getPackage(java.lang.String name)

Search for the given package inside this package. Note that name has to be the short name of the package (i.e. not the fully qualified name)

Returns:

the package with the given name, null if it is not found.

getClass

public AClass getClass(java.lang.String name)

Search for the given class inside this package. Note that name has to be the short name of the class (i.e. not the fully qualified name).

Returns:

the class with the given name, null if it is not found.

createAndCheckSubPackage

public Package createAndCheckSubPackage(IJml2bConfiguration config,
                                        java.lang.String name)

Check that the package name exists and create the subpackage if it does.

getAndLoadPackage

public Package getAndLoadPackage(java.lang.String name)

getAndLoadClass

public AClass getAndLoadClass(IJml2bConfiguration config,
                              java.lang.String name)
                       throws Jml2bException

Return a reference to the class name. This method will try to load the class if name cannot be found. return null If the class cannot be found neither in the loaded classes nor on the disk. Throws ClassLoadError if a candidate class was found on the disk, but could not be loaded

Throws:

Jml2bException

getFullyQualifiedName

public java.lang.String getFullyQualifiedName()

Returns the fully qualified name of this package.

getDirectory

public java.lang.String getDirectory()

return the directory corresponding to this package. return null if the package is the root package

getJavaLang

public static Package getJavaLang()

createSubPackage

public Package createSubPackage(java.lang.String name)

getRoot

public static Package getRoot()

initFromFile

public static boolean initFromFile(java.lang.String file_name)

Inits the root package (java.lang, etc...) from the given serialized file. return true on success, false otherwise.

restoreDefaultPackages

public static boolean restoreDefaultPackages(Package root)

clearAll

public static void clearAll()

Unload all the loaded packages.

searchClass

public AClass searchClass(java.lang.String s)