|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||
ClassInfo structure (see JVM2, 4.7).accum if
this is a keyword or literal token.
accum.
name declared in the type represented by this,
or added to the type by external methods, using the
strategy actor.
name declared in the type represented by this,
using the strategy actor.
name declared in the type represented by this,
using the strategy actor.
name declared in the type represented by this,
ignoring external methods, using the strategy
actor.
name declared in the type represented by this,
or added to the type by external methods, using the
strategy actor.
name declared in the type represented by this,
or added to the type by external methods, using the
strategy actor.
cUnit.
qName.
cUnit
if the symbol table has not been built.
qName.
cUnit
if the symbol table has not been built.
specVarDecls, and
spec header, specHeader, to the spec case,
specCase.
attr to the attribute
list of this field.
requires clause to the given
behaviorSpec, bs, and returns it.
field to the members
of its data group.
parentMap that are
already in this map.
member to the member set of group
if group is already in this map.
group if it is not already in this
map.
mdecl, to the
instrumented class.
mdecl, to
the surrogate class to be generated in the finalization step of
this translation.
mdecl, to the
instrumented type.
this parameter.
this parameter.
this parameter.
this parameter.
this is used in this
block.
this is used in this block.
this is used in this
block.
this is used in this
block.
previousContext is no longer being
used and that all block statements inside the switch body have
been checked.
String) to class
type singletons (of type CClassType).
JStatement arrays, each of
them representing a jml-compound-statement.
var, to the value for an angelic
undefinedness.
accum.
accum.
accum.
result.
result.
buffer.
binOp
typeDest
and source type typeSource in cast expression. the parm
strTypeDest is needed for in different class, the method "toString"
is difined differently.
typeSource
which is a \bigint or numerical type to destination number type
typeNumber which is a numerical type.cast expression. the parm
strTypeDest is needed for in different class, the method "toString"
is difined differently.
unaryOp
v
of type typeVar to typeDest.
binOp, to the given operands, v1 and v2.
unaryOp, to the given operand v1.
strExpr
of type typeExpr to typeSelf.
args to a method call for making a
dynamic call.
args.
i in 0..files.length this
asserts that Utils.relativePathTo(files[i]) equals
prefix + files[i].getName()
JmlAxiom instance parsed in the
class declaration buffered by this.
this.definition.
this.definition.
fieldInfo by
parsing the appropriate field signature extracted from the *.class file.
java.util.Iterator
interface but is specific to collections of
CMethod.CAnchorInitializer instance.
CAugmentationMap: CClass x CContextType ->
CMethodSet.CBinaryClassContext instance.
ClassInfo object.
CCORInitializer instance.
CBinaryClasses.
CClassContextType.createConstructorContext.
CDispatcherInitializer instance.
CFunctionAccessMethod instance.
CGFCollectionMap:
CCompilationUnit x String -> { CGFCollection }.FunctionalTestSuite.TestCase.cleanWorkingDir().
in and referring to the constant pool
cp.
java.lang.
CSourceFilteredDispatcherMethod instance.
type1@type2.expr
with respect to the quantified variable var.
expr with respect to the quantified variable
var.
expr.
expr.
cond is true.
cond is true.
cond is true.
clause, using the
definite assignment information from entryContext.
refinedType field of this
JmlTypeDeclaration object.
this.definition.
CClass and all its owners:
Type check the type variables of the class.
found is null.
self exactly match with the corresponding
parameter(s) of overriddenMeth, a method that it
overrides.
self
are consistent with overriddenMeth, a method that it
overrides.
this.definition.
type.
typeArguments (the
type checked versions are re-stored into the same array) and checks
whether the typeArguments are valid for the given
typeVariables.
clazz.
stmt) wrapped with
code to inherit superclass's assertions if any, and to signal
an assertion violation if it happens at runtime.
stmt,
wrapped with code to inherit supertypes's constraints.
stmt)
wrapped with code to inherit superclass's preconditions if any,
and to signal an assertion violation if it happens at
runtime.
stmt)
wrapped with code to inherit supertypes's constraints.
args, and returns true if all the
skeletons are successfully generated.
args, and returns true if all the test
classes are successfully generated.
completeClassInfo().
mdecl.
\bigint's or \real's.
\bigint's or \real's.
\bigint's or \real's.
\bigint's or \real's.
oper)
constraints.
constraint.
pred as a hisotry constraint.
JmlConstraint instance parsed in the
class declaration buffered by this.
static initializers.
key?
key?
other in the same position.
name
with formal parameter types, types, declared in
the class, clazz.
wildcard which must
have been type checked.
x += 3) depending on
the assignment operator.
ClassInfo.
qName.
name.
ClassInfo.
qName.
data.
JmlExpressionContext object as a child of
the given (CClassContextType) context, which is suitable for
checking this axiom clause.
data.
lowerBound.
fieldInfo.
methodInfo.
data.
oldTask along
with the command line options to determine what task to add to
the task queue after the given task completes.
oldTask.
oldTask, completes.
oldTask along
with the command line options to determine what task to add to
the task queue after the given task completes.
upperBound.
java.lang.Object class.
candidate method need to be made against the
accumulator by calls to resultFor().
#accumKeywords(List,String,List).equivChars String as equal.
field.
type.
type.
type.
type.
var, to the value for an demonic
undefinedness.
maybeSuper type is a supertype
of the maybeSub type.
maybeSuper
type.
var.