Interface | Description |
---|---|
KeYRecoderExtension | |
SVWrapper |
Class | Description |
---|---|
Bigint |
RecodeR extension for JML's \bigint type.
|
CatchAllStatement | |
CatchSVWrapper | |
ClassFileDeclarationBuilder |
Make a ClassDeclaration out of a class file.
|
ClassFileDeclarationManager |
This class provides an infrastructure to read in multiple class files and to
manufacture ClassDeclarations out of them.
|
ClassInitializeMethodBuilder |
Each class is prepared before it is initialised.
|
ClassPreparationMethodBuilder |
Each class is prepared before it is initialised.
|
ConstantStringExpressionEvaluator | |
ConstructorNormalformBuilder |
Transforms the constructors of the given class to their
normalform.
|
ContextStatementBlock |
Statement block.
|
CreateBuilder |
If an allocation expression
new Class(...) |
CreateObjectBuilder |
If an allocation expression
new Class(...) |
DLEmbeddedExpression |
This class is used to parse function applications with JavaDL escapes within
set statements or similar situations.
|
EnumClassBuilder |
This transformation is made to transform any found
EnumDeclaration
into a corresponding EnumClassDeclaration . |
EnumClassDeclaration |
This class is used to describe an enum type by its equivalent class
declaration.
|
EscapeExpression |
Handles JML expressions that begin with an escape character '\'.
|
ExecCtxtSVWrapper | |
ExecutionContext | |
ExpressionSVWrapper | |
ExtendedIdentifier |
an extended identifier that accepts hash symbols in its name
but not as first character
|
Ghost | |
ImplicitFieldAdder |
The Java DL requires some implicit fields and methods, that are
available in each Java class.
|
ImplicitIdentifier |
subclasses the recoder Identifier in order to allow fields with special
characters.
|
InstanceAllocationMethodBuilder | |
JMLTransformer |
RecodeR transformation that parses JML comments, and attaches code-like
specifications (ghost fields, set statements, model methods) directly to the
RecodeR AST.
|
JMLTransformer.TypeDeclarationCollector | |
JumpLabelSVWrapper | |
KeYAnnotationUseSpecification | |
KeYCrossReferenceNameInfo |
This is a specialisation of the NameInfo interface which allows KeY to detect
multiple declaration of types.
|
KeYCrossReferenceServiceConfiguration | |
KeYCrossReferenceSourceFileRepository |
This class is used to handle source files within recoder.
|
LabelSVWrapper | |
LocalClassTransformation |
Local and anonymous classes may access variables from the creating context
if they are declared final and initialised.
|
LoopScopeBlock |
TODO
|
MergePointStatement | |
MethodBodyStatement |
A shortcut-statement for a method body.
|
MethodCallStatement |
The statement inserted by KeY if a method call is executed.
|
MethodSignatureSVWrapper | |
Model | |
NewArrayWrapper | |
NewWrapper | |
NoState | |
ObjectTypeIdentifier | |
PassiveExpression | |
PrepareObjectBuilder |
Creates the preparation method for pre-initilizing the object fields
with their default settings.
|
ProgramVariableSVWrapper | |
ProofCrossReferenceServiceConfiguration | |
ProofJavaProgramFactory | |
Real |
recoder extension for JML's \real type.
|
RecoderModelTransformer |
The Java DL requires some implicit fields, that are available in each
Java class.
|
RecoderModelTransformer.TransformerCache |
Cache of important data.
|
RecoderModelTransformer.TypeAndClassDeclarationCollector | |
RegisteredEscapeExpression |
This class handles all escape expressions in set-statements, that are registered
in JMLTranslator.jml2jdl
|
RKeYMetaConstruct | |
RKeYMetaConstructExpression | |
RKeYMetaConstructType | |
RMethodBodyStatement | |
RMethodCallStatement | |
SchemaCrossReferenceServiceConfiguration | |
SchemaCrossReferenceSourceInfo | |
SchemaJavaProgramFactory | |
SourceVisitorExtended |
Adds visitor methods for recoder extensions.
|
SpecialReferenceWrapper | |
StatementSVWrapper | |
TransactionStatement | |
TwoState | |
TypeSVWrapper | |
URLDataLocation |
This class implements a data location, that describes an arbitrary URL.
|