| de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
The classes in the subpackages are mainly taken from the Recoder
framework and made immutable. They are transformed into this data
structure from a Recoder structure by {@link
de.uka.ilkd.key.java.Recoder2KeY} or {@link
de.uka.ilkd.key.SchemaRecoder2KeY}. However, in some details both
data structures might differ more.
The following explanations are adapted from the
documentation of the Recoder framework.
- Source and Program Elements
-
A {@link de.uka.ilkd.key.java.SourceElement} is a syntactical entity and not
necessary a {@link de.uka.ilkd.key.java.ModelElement}, such as a {@link de.uka.ilkd.key.java.Comment}.
A {@link de.uka.ilkd.key.java.ProgramElement} is a {@link de.uka.ilkd.key.java.SourceElement}
and a {@link de.uka.ilkd.key.ModelElement}. It is aware of its parent in the syntax
tree, while a pure {@link de.uka.ilkd.key.java.SourceElement} is not considered as a
member of the AST even though it is represented in the sources.
{@link de.uka.ilkd.key.java.ProgramElement}s are further
classified into {@link de.uka.ilkd.key.java.TerminalProgramElement}s and
{@link de.uka.ilkd.key.java.NonTerminalProgramElement}s. While {@link de.uka.ilkd.key.java.TerminalProgramElement}
is just a tag class, {@link de.uka.ilkd.key.java.NonTerminalProgramElement}s know
their AST children (while it is possible that they do not have any).
A complete source file occurs as a {@link de.uka.ilkd.key.java.CompilationUnit}.
{@link de.uka.ilkd.key.java.JavaSourceElement} and
{@link de.uka.ilkd.key.java.JavaProgramElement} are abstract classes defining
standard implementations that already know their
{@link de.uka.ilkd.key.java.JavaProgramFactory}.
- Expressions and Statements
-
{@link de.uka.ilkd.key.java.Expression} and {@link de.uka.ilkd.key.java.Statement} are
self-explanatory. A {@link de.uka.ilkd.key.java.LoopInitializer} is a special
{@link de.uka.ilkd.key.java.Statement} valid as initializer of
{@link de.uka.ilkd.key.java.statement.For} loops.
{@link de.uka.ilkd.key.java.LoopInitializer} is subtyped by
{@link de.uka.ilkd.key.java.expression.ExpressionStatement} and
{@link de.uka.ilkd.key.java.declaration.LocalVariableDeclaration}).
Concrete classes and further abstractions are bundled in the
{@link de.uka.ilkd.key.java.expression} and {@link de.uka.ilkd.key.java.statement} packages.
- Syntax Tree Parents
-
There are a couple of abstractions dealing with properties of being a
parent node.
These are {@link de.uka.ilkd.key.java.declaration.TypeDeclarationContainer},
{@link de.uka.ilkd.key.java.ExpressionContainer},
{@link de.uka.ilkd.key.java.StatementContainer},
{@link de.uka.ilkd.key.java.ParameterContainer},
{@link de.uka.ilkd.key.java.NamedProgramElement} and
{@link de.uka.ilkd.key.java.reference.TypeReferenceContainer}. A
An {@link de.uka.ilkd.key.java.ExpressionContainer} contains
{@link de.uka.ilkd.key.java.Expression}s, a
{@link de.uka.ilkd.key.java.StatementContainer} contains
{@link de.uka.ilkd.key.java.Statement}s, a
{@link de.uka.ilkd.key.java.ParameterContainer}
(either a {@link de.uka.ilkd.key.java.declaration.MethodDeclaration} or a
{@link de.uka.ilkd.key.java.statement.Catch} statement) contains
{@link de.uka.ilkd.key.java.declaration.ParameterDeclaration}s.
A {@link de.uka.ilkd.key.java.NamedProgramElement} is a subtype of
{@link de.uka.ilkd.key.NamedModelElement}.
A {@link de.uka.ilkd.key.java.reference.TypeReferenceContainer} contains one or
several names, but these are names of types that are referred to explicitely
by a {@link de.uka.ilkd.key.java.reference.TypeReference}.
- References
-
A {@link de.uka.ilkd.key.java.Reference} is an explicite use of an entity. Most of
these {@link de.uka.ilkd.key.java.Reference}s are
{@link de.uka.ilkd.key.java.reference.NameReference}s
and as such {@link de.uka.ilkd.key.java.NamedProgramElement}s, e.g. the
{@link de.uka.ilkd.key.java.reference.TypeReference}.
Subtypes of {@link de.uka.ilkd.key.java.Reference}s are bundled in the
{@link de.uka.ilkd.key.java.reference} package.
- Modifiers and Declarations
-
{@link de.uka.ilkd.key.java.declaration.Modifier}s are (exclusively) used in the
context of {@link de.uka.ilkd.key.java.Declaration}s.
{@link de.uka.ilkd.key.java.declaration.Modifier}s occur explictely, since they occur
as syntactical tokens that might be indented and commented.
{@link de.uka.ilkd.key.java.Declaration}s are either
declarations of types or other entities such as
{@link de.uka.ilkd.key.java.declaration.MemberDeclaration} or
{@link de.uka.ilkd.key.java.declaration.VariableDeclaration}. Concrete
{@link de.uka.ilkd.key.java.declaration.Modifier}s and
{@link de.uka.ilkd.key.java.Declaration}s are
bundled in the {@link de.uka.ilkd.key.java.declaration.modifier} and
{@link de.uka.ilkd.key.java.declaration} packages.
|
| Java Source File Name | Type | Comment |
| Comment.java | Class | |
| CompilationUnit.java | Class | A node representing a single source file containing
TypeDeclaration s and an optional
PackageSpecification and an optional set of
Import s. |
| ConstantExpressionEvaluator.java | Class | |
| Context.java | Class | |
| ContextStatementBlock.java | Class | In the DL-formulae description of Taclets the program part can have
the following form < pi alpha;...; omega > Phi where pi is a prefix
consisting of open brackets, try's and so on and omega is the rest
of the program. |
| ConvertException.java | Class | |
| CreateArrayMethodBuilder.java | Class | This class creates the <createArray> method for array
creation and in particular its helper method
<createArrayHelper>. |
| CreateTransientArrayMethodBuilder.java | Class | This class creates the <createArray> method for
array creation and in particular its helper method
<createArrayHelper>. |
| Declaration.java | Interface | Declaration. |
| Dimension.java | Class | |
| Expression.java | Interface | |
| ExpressionContainer.java | Interface | Expression container. |
| Import.java | Class | Import. |
| JavaInfo.java | Class | an instance serves as representation of a Java model underlying a DL
formula. |
| JavaNonTerminalProgramElement.java | Class | Top level implementation of a Java
NonTerminalProgramElement . |
| JavaProgramElement.java | Class | Top level implementation of a Java
ProgramElement . |
| JavaReader.java | Interface | |
| JavaSourceElement.java | Class | Top level implementation of a Java
SourceElement . |
| KeYJavaASTFactory.java | Class | The KeYASTFactory helps building KeY Java AST structures. |
| KeYProgModelInfo.java | Class | |
| KeYRecoderMapping.java | Class | |
| Label.java | Interface | |
| LoopInitializer.java | Interface | Loop initializer. |
| ModelElement.java | Interface | A semantical part of the software model. |
| NameAbstractionTable.java | Class | This class is used for the equals modulo renaming method in
SourceElement. |
| NamedModelElement.java | Interface | A model element that carries a name. |
| NamedProgramElement.java | Interface | Named program element. |
| NonTerminalProgramElement.java | Interface | Non terminal program element. |
| PackageSpecification.java | Class | Package specification. |
| ParameterContainer.java | Interface | Describes program elements that contain
recoder.java.declaration.ParameterDeclaration s. |
| ParentIsInterfaceDeclaration.java | Class | |
| PosConvertException.java | Class | |
| Position.java | Class | The position of a source element, given by its line and column
number. |
| PositionInfo.java | Class | |
| PrettyPrinter.java | Class | A configurable pretty printer for Java source elements originally from COMPOST.
author:
AL
author:
CHANGED FOR KeY. |
| ProgramElement.java | Interface | A part of the program syntax that carries semantics in the model. |
| ProgramVariableName.java | Interface | |
| Recoder2KeY.java | Class | |
| RecoderExample.java | Class | this class is an example how to work with a java AST. |
| Reference.java | Interface | References are uses of names, variables or members. |
| SchemaJavaReader.java | Interface | |
| SchemaRecoder2KeY.java | Class | |
| ScopeDefiningElement.java | Interface | The property of a non terminal program element to define a scope. |
| Services.java | Class | this is a collection of common services to the KeY prover. |
| SingleLineComment.java | Class | Any non-SingleLineComment is a multi line comment. |
| SourceData.java | Class | This class keeps track of the next element to match, which is provided by
calling method
SourceData.getSource() . |
| SourceElement.java | Interface | A source element is a piece of syntax. |
| Statement.java | Interface | Statement. |
| StatementBlock.java | Class | Statement block. |
| StatementContainer.java | Interface | Statement container. |
| StringConverter.java | Class | |
| TerminalProgramElement.java | Interface | Terminal program element. |
| TestContextStatementBlock.java | Class | |
| TestJavaCardDLJavaExtensions.java | Class | |
| TestJavaInfo.java | Class | |
| TestKeYRecoderMapping.java | Class | |
| TestRecoder2KeY.java | Class | |
| TestTypeConverter.java | Class | |
| TypeConverter.java | Class | |
| TypeNameTranslator.java | Class | |
| TypeScope.java | Interface | The property of a non terminal program element to define a scope for
types. |
| VarAndType.java | Class | |
| VariableScope.java | Interface | The property of a non terminal program element to define a scope for
variables. |