jml2b.structure.java
Class AClass

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

All Implemented Interfaces:

jml.JmlDeclParserTokenTypes, Linkable, java.io.Serializable

Direct Known Subclasses:

Class, ClassFile

public abstract class AClass

extends NamedNode

implements Linkable

Author:

L. Burdy

See Also:

Serialized Form

Field Summary

Fields inherited from class jml2b.structure.java.NamedNode

garbage, nameIndex

Fields inherited from interface jml2b.link.Linkable

STATE_LINKED, STATE_LINKED_STATEMENTS, STATE_LINKED_TYPE_CHECKED, STATE_UNLINKED

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

AClass()

AClass(JmlFile jf, antlr.collections.AST tree)

Method Summary

java.util.Vector	addSuperFields(AClass c, java.util.Vector v) Adds the fields defined by super classes that are visibles from the given class to the given vector.
abstract AMethod	getConstructor(IJml2bConfiguration config, java.util.Vector param_types)
abstract AMethod	getDefaultConstructor()
abstract java.util.Enumeration	getDepends()
AField	getField(java.lang.String name) Returns the field with the given name
abstract AField	getField(java.lang.String name, AClass from)
abstract java.util.Enumeration	getFields()
abstract java.lang.String	getFullyQualifiedName()
abstract java.util.Enumeration	getImplements()
abstract java.util.Enumeration	getMemberInvariants()
abstract AMethod	getMethod(java.lang.String name, Parameters p)
abstract IModifiers	getModifiers()
abstract java.lang.String	getName()
abstract java.util.Vector	getOwnFields()
abstract Package	getPackage()
abstract java.util.Enumeration	getRepresents()
abstract java.util.Enumeration	getStaticFinalFieldsInvariant()
abstract Expression	getStaticFinalFieldsInvariants()
abstract java.util.Enumeration	getStaticInvariants()
Type	getSuper() Returns a type corresponding to the type of the super class.
AClass	getSuperClass() Returns the super class of the current class.
AMethod	getSuperDefaultConstructor() Returns the default constructor for the super class.
boolean	implementsInterface(AClass ith) Returns true if the current class implements the given interface.
abstract boolean	isInterface()
boolean	isObject() Returns true if the current class represents java.lang.Object.
boolean	isSubclassOf(AClass super_class) Returns true if and only if super_class is a super class of this or if this and super_class are the same classes.
AMethod	lookupMethod(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types) Search the given method in the class and superclass methods.
AMethod	lookupMethodClass(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate) Lookup the given method in the current class (which is not an interface).
abstract AMethod	lookupMethodCurrentClass(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate)
AMethod	lookupMethodInterface(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate) Lookup the given method in the current interface (which is not class).

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

Methods inherited from interface jml2b.link.Linkable

link, linkStatements

Constructor Detail

AClass

public AClass()

AClass

public AClass(JmlFile jf,
              antlr.collections.AST tree)

Method Detail

isObject

public boolean isObject()

Returns true if the current class represents java.lang.Object.

Returns:

boolean

getSuperClass

public AClass getSuperClass()

Returns the super class of the current class.

Returns:

Class the class of the current class. null if the current class does not have a super class.

isSubclassOf

public boolean isSubclassOf(AClass super_class)

Returns true if and only if super_class is a super class of this or if this and super_class are the same classes. Note that super_class is not required to be a direct super class of the current class.

Parameters:

super_class - the class that is compared to the current class.

Returns:

true if super_class is a super class for the current class.

implementsInterface

public boolean implementsInterface(AClass ith)

Returns true if the current class implements the given interface. The superclass is searched as well as the interfaces implemented by implemented interfaces

Parameters:

ith - the interface that is searched

Returns:

true if the current class or one if its super class or implemented interfaces implements ith.

getSuper

public Type getSuper()

Returns a type corresponding to the type of the super class.

Returns:

Type the type of the super class.

getField

public AField getField(java.lang.String name)

Returns the field with the given name

lookupMethod

public AMethod lookupMethod(IJml2bConfiguration config,
                            java.lang.String mth_name,
                            java.util.Vector param_types)
                     throws Jml2bException

Search the given method in the class and superclass methods.

Parameters:

config - the configurationt that should be used.

mth_name - the name of the searched method.

param_types - vector of Type elements corresponding to the signature of the searched method.

Returns:

Method the searched method, null if no such method exists.

Throws:

Jml2bException

getSuperDefaultConstructor

public AMethod getSuperDefaultConstructor()

Returns the default constructor for the super class.

Returns:

Method the default constructor for the super class. null if no such constructor exists or if the class does not have a super class.

getFullyQualifiedName

public abstract java.lang.String getFullyQualifiedName()

getName

public abstract java.lang.String getName()

Specified by:

getName in class NamedNode

isInterface

public abstract boolean isInterface()

getPackage

public abstract Package getPackage()

getStaticInvariants

public abstract java.util.Enumeration getStaticInvariants()

getModifiers

public abstract IModifiers getModifiers()

getRepresents

public abstract java.util.Enumeration getRepresents()

getStaticFinalFieldsInvariants

public abstract Expression getStaticFinalFieldsInvariants()

getStaticFinalFieldsInvariant

public abstract java.util.Enumeration getStaticFinalFieldsInvariant()

getFields

public abstract java.util.Enumeration getFields()

getDepends

public abstract java.util.Enumeration getDepends()

getMemberInvariants

public abstract java.util.Enumeration getMemberInvariants()

getDefaultConstructor

public abstract AMethod getDefaultConstructor()

getField

public abstract AField getField(java.lang.String name,
                                AClass from)

addSuperFields

public java.util.Vector addSuperFields(AClass c,
                                       java.util.Vector v)

Adds the fields defined by super classes that are visibles from the given class to the given vector.

Parameters:

c - the class from which the fields should be visibles

v - the destination vector.

Returns:

Vector the resulting vector.

getImplements

public abstract java.util.Enumeration getImplements()

getConstructor

public abstract AMethod getConstructor(IJml2bConfiguration config,
                                       java.util.Vector param_types)
                                throws Jml2bException

Throws:

Jml2bException

getMethod

public abstract AMethod getMethod(java.lang.String name,
                                  Parameters p)

lookupMethodInterface

public AMethod lookupMethodInterface(IJml2bConfiguration config,
                                     java.lang.String mth_name,
                                     java.util.Vector param_types,
                                     AMethod candidate)
                              throws Jml2bException

Lookup the given method in the current interface (which is not class). Searches for the method mth_name in the current class, as well as in the implemented interfaces.

Parameters:

config - the configuration that should be used.

mth_name - the name of the method

param_types - type of the parameters

candidate - the current candidate method. That is, the method that matches best the searched method.

Returns:

Method the new best candidate method.

Throws:

Jml2bException

lookupMethodClass

public AMethod lookupMethodClass(IJml2bConfiguration config,
                                 java.lang.String mth_name,
                                 java.util.Vector param_types,
                                 AMethod candidate)
                          throws Jml2bException

Lookup the given method in the current class (which is not an interface). The interface methods are not searched, since it is assumed that every interface method will be implemented by the class or one of its super classes.

Parameters:

config - the configuration that should be used.

mth_name - the name of the searched method.

param_types - vector of Type elements containing the signature of the searched method.

candidate - the current best candidate method.

Returns:

the new best candidate method.

Throws:

Jml2bException

lookupMethodCurrentClass

public abstract AMethod lookupMethodCurrentClass(IJml2bConfiguration config,
                                                 java.lang.String mth_name,
                                                 java.util.Vector param_types,
                                                 AMethod candidate)
                                          throws Jml2bException

Throws:

Jml2bException

getOwnFields

public abstract java.util.Vector getOwnFields()

Returns: