de.uka.ilkd.key.java (KeY API Documentation)

Interface Summary
Interface	Description
Declaration	Declaration.
Expression	Expression taken from COMPOST and changed to achieve an immutable structure
ExpressionContainer	Expression container.
JavaReader
Label
LoopInitializer	Loop initializer.
ModelElement	A semantical part of the software model.
NamedModelElement	A model element that carries a name.
NamedProgramElement	Named program element.
NonTerminalProgramElement	Non terminal program element.
ParameterContainer	Describes program elements that contain `ParameterDeclaration`s.
ProgramElement	A part of the program syntax that carries semantics in the model.
ProgramVariableName
Reference	References are uses of names, variables or members.
SchemaJavaReader
ScopeDefiningElement	The property of a non terminal program element to define a scope.
Services.ITermProgramVariableCollectorFactory
SourceElement	A source element is a piece of syntax.
Statement	Statement.
StatementContainer	Statement container.
TerminalProgramElement	Terminal program element.
TypeScope	The property of a non terminal program element to define a scope for types.
VariableScope	The property of a non terminal program element to define a scope for variables.

Class Summary
Class	Description
Comment
CompilationUnit	A node representing a single source file containing `TypeDeclaration`s and an optional `PackageSpecification` and an optional set of `Import`s.
ConstantExpressionEvaluator
Context	this class stores recoder related contextinformation used to parse in program parts in which non-declared variables are used
ContextStatementBlock	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.
CreateArrayMethodBuilder	This class creates the `<createArray>` method for array creation and in particular its helper method `<createArrayHelper>`.
Dimension
Import	Import.
JavaInfo	an instance serves as representation of a Java model underlying a DL formula.
JavaInfo.Filter	inner class used to filter certain types of program elements
JavaNonTerminalProgramElement	Top level implementation of a Java `NonTerminalProgramElement`.
JavaProgramElement	Top level implementation of a Java `ProgramElement`.
JavaProgramElement.NameAbstractionTableDisabled	this class is used by method call.
JavaReduxFileCollection	This is a special `FileCollection` which allows to retrieve the internally stored java boot sources and to iterate over them.
JavaSourceElement	Top level implementation of a Java `SourceElement`.
JavaTools	Miscellaneous static methods related to Java blocks or statements in KeY.
KeYJavaASTFactory	The KeYASTFactory helps building KeY Java AST structures.
KeYProgModelInfo
KeYRecoderMapping
NameAbstractionTable	This class is used for the equals modulo renaming method in SourceElement.
PackageSpecification	Package specification.
ParentIsInterfaceDeclaration
Position	The position of a source element, given by its line and column number.
PositionInfo	represents a group of three Positions: relativePosition, startPosition, endPosition
PrettyPrinter	A configurable pretty printer for Java source elements originally from COMPOST.
ProgramPrefixUtil
ProgramPrefixUtil.ProgramPrefixInfo
Recoder2KeY	This class is the bridge between recoder ast data structures and KeY data structures.
Recoder2KeYConverter	Objects of this class can be used to transform an AST returned by the recoder library to the corresponding yet immutable KeY data structures.
Recoder2KeYTypeConverter	provide means to convert recoder types to the corresponding KeY type structures.
SchemaRecoder2KeY
SchemaRecoder2KeYConverter	This is an extension of the usual `Recoder2KeYConverter` that supports schema variables.
ServiceCaches	Instances of this class provides all caches used by an individual `Proof` or more precise by its `Services`.
Services	this is a collection of common services to the KeY prover.
SingleLineComment	Any non-SingleLineComment is a multi line comment.
SourceData	This class keeps track of the next element to match, which is provided by calling method `SourceData.getSource()`.
StatementBlock	Statement block.
TypeConverter
TypeNameTranslator

Exception Summary
Exception	Description
ConvertException	This exception class is mainly thrown by Recoder2KeY and its companions.
ParseExceptionInFile	This exception extends recoder's `ParseException` by a filename.
PosConvertException	A convert exception enriched with a location within a file/source.
UnknownJavaTypeException

Package de.uka.ilkd.key.java Description

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 Recoder2KeY or 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 SourceElement is a syntactical entity and not necessary a ModelElement, such as a Comment.

A ProgramElement is a SourceElement and a de.uka.ilkd.key.ModelElement. It is aware of its parent in the syntax tree, while a pure SourceElement is not considered as a member of the AST even though it is represented in the sources.

ProgramElements are further classified into TerminalProgramElements and NonTerminalProgramElements. While TerminalProgramElement is just a tag class, NonTerminalProgramElements know their AST children (while it is possible that they do not have any). A complete source file occurs as a CompilationUnit.

JavaSourceElement and JavaProgramElement are abstract classes defining standard implementations that already know their de.uka.ilkd.key.java.JavaProgramFactory.

Expressions and Statements

Expression and Statement are self-explanatory. A LoopInitializer is a special Statement valid as initializer of For loops. LoopInitializer is subtyped by ExpressionStatement and LocalVariableDeclaration).

Concrete classes and further abstractions are bundled in the de.uka.ilkd.key.java.expression and 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 TypeDeclarationContainer, ExpressionContainer, StatementContainer, ParameterContainer, NamedProgramElement and TypeReferenceContainer. A An ExpressionContainer contains Expressions, a StatementContainer contains Statements, a ParameterContainer (either a MethodDeclaration or a Catch statement) contains ParameterDeclarations. A NamedProgramElement is a subtype of NamedModelElement. A TypeReferenceContainer contains one or several names, but these are names of types that are referred to explicitely by a TypeReference.

References

A Reference is an explicite use of an entity. Most of these References are NameReferences and as such NamedProgramElements, e.g. the TypeReference. Subtypes of References are bundled in the de.uka.ilkd.key.java.reference package.

Modifiers and Declarations

Modifiers are (exclusively) used in the context of Declarations. Modifiers occur explicitly, since they occur as syntactical tokens that might be indented and commented. Declarations are either declarations of types or other entities such as MemberDeclaration or VariableDeclaration. Concrete Modifiers and Declarations are bundled in the de.uka.ilkd.key.java.declaration.modifier and de.uka.ilkd.key.java.declaration packages.