| 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.
|