Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.declaration |
Elements of the Java syntax tree representing declarations.
|
de.uka.ilkd.key.java.declaration.modifier |
This package collects all Java modifiers.
|
de.uka.ilkd.key.java.expression |
Elements of the Java syntax tree representing expressions.
|
de.uka.ilkd.key.java.expression.literal |
This package contains representations for the various Java literal types.
|
de.uka.ilkd.key.java.expression.operator |
Elements of the Java syntax tree representing operators and operator-like
expressions.
|
de.uka.ilkd.key.java.expression.operator.adt | |
de.uka.ilkd.key.java.reference |
Elements of the Java syntax tree representing implicit or explicit (named)
references to other program elements.
|
de.uka.ilkd.key.java.statement |
Elements of the Java syntax tree representing pure statements.
|
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
Modifier and Type | Class and Description |
---|---|
class |
CcatchBreakLabelParameterDeclaration
A "\Break label" parameter declaration of a ccatch clause.
|
class |
CcatchBreakParameterDeclaration
A "\Break" parameter declaration of a ccatch clause.
|
class |
CcatchBreakWildcardParameterDeclaration
A "\Break *" parameter declaration of a ccatch clause.
|
class |
CcatchContinueLabelParameterDeclaration
A "\Continue label" parameter declaration of a ccatch clause.
|
class |
CcatchContinueParameterDeclaration
A "\Continue" parameter declaration of a ccatch clause.
|
class |
CcatchContinueWildcardParameterDeclaration
A "\Continue *" parameter declaration of a ccatch clause.
|
class |
CcatchNonstandardParameterDeclaration
A "non-standard" parameter declaration of a Ccatch clause, e.g., "\Return".
|
class |
CcatchReturnParameterDeclaration
A "\Return" parameter declaration of a ccatch clause.
|
class |
CcatchReturnValParameterDeclaration
A "\Return int v" parameter declaration of a ccatch clause.
|
class |
Comment |
class |
CompilationUnit
A node representing a single source file containing
TypeDeclaration s and an optional PackageSpecification
and an optional set of Import s. |
class |
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.
|
class |
Import
Import.
|
class |
JavaNonTerminalProgramElement
Top level implementation of a Java
NonTerminalProgramElement . |
class |
JavaProgramElement
Top level implementation of a Java
ProgramElement . |
class |
PackageSpecification
Package specification.
|
class |
SingleLineComment
Any non-SingleLineComment is a multi line comment.
|
class |
StatementBlock
Statement block.
|
Modifier and Type | Class and Description |
---|---|
class |
ArrayDeclaration
KeY used to model arrays using only the
ArrayType . |
class |
ClassDeclaration
There are several types of class declarations:
package-less outer classes
getClassContainer() == null
getStatementContainer() == null
getName() != null
ordinary outer classes
getClassContainer() instanceof Package
getStatementContainer() == null
getName() != null
member classes
getClassContainer() instanceof ClassDeclaration
getStatementContainer() == null
getName() != null
local class
getClassContainer() == null
getStatementContainer() != null
getName() != null
local anonymous class
getClassContainer() == null
getStatementContainer() instanceof expression.New
getName() == null
Anonymous local classes have exactly one supertype and no
subtypes.
|
class |
ClassInitializer |
class |
ConstructorDeclaration
The getTypeReference method returns null - constructors do not have
explicite return types.
|
class |
EnumClassDeclaration
This class is used for wrapping an enum into a standard class type.
|
class |
Extends
Extends.
|
class |
FieldDeclaration
Field declaration.
|
class |
FieldSpecification |
class |
Implements
Implements.
|
class |
ImplicitFieldSpecification |
class |
InheritanceSpecification
Inheritance specification.
|
class |
InterfaceDeclaration
Interface declaration.
|
class |
JavaDeclaration
Java declaration.
|
class |
LocalVariableDeclaration
Local variable declaration.
|
class |
MethodDeclaration
Method declaration.
|
class |
Modifier
Modifier.
|
class |
ParameterDeclaration
Formal parameters require a VariableSpecificationList of size() <= 1
(size() == 0 for abstract methods) without initializer (for Java).
|
class |
SuperArrayDeclaration
At the moment the mere purpose of this Class is to provide an encapsulation
for the length attribute.
|
class |
Throws
Throws.
|
class |
TypeDeclaration
Type declaration.
|
class |
VariableDeclaration
Variable declaration.
|
class |
VariableSpecification
Variable specification that defines a variable name.
|
Modifier and Type | Class and Description |
---|---|
class |
Abstract
Abstract.
|
class |
AnnotationUseSpecification |
class |
Final
Final.
|
class |
Ghost
The JML modifier "ghost".
|
class |
Model
The JML modifier "model".
|
class |
Native
Native.
|
class |
NoState
The JML modifier "no_state".
|
class |
Private
Private.
|
class |
Protected
Protected.
|
class |
Public
Public.
|
class |
Static
Static.
|
class |
StrictFp
Strict fp.
|
class |
Synchronized
Synchronized.
|
class |
Transient
Transient.
|
class |
TwoState
The JML modifier "two_state".
|
class |
VisibilityModifier
Visibility modifier.
|
class |
Volatile
Volatile.
|
Modifier and Type | Class and Description |
---|---|
class |
ArrayInitializer
An ArrayInitializer is a valid expression exclusively for initializing
ArrayTypes.
|
class |
Assignment
An assignment is an operator with side-effects.
|
class |
Literal
Literal.
|
class |
Operator
Operator base class.
|
class |
ParenthesizedExpression
Redundant Parentheses.
|
class |
PassiveExpression
Marks an active statement as inactive.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractIntegerLiteral
This class is a superclass for integer literals (Int, Long, Char).
|
class |
BooleanLiteral
Boolean literal.
|
class |
CharLiteral
Char literal.
|
class |
DoubleLiteral
Double literal.
|
class |
EmptyMapLiteral |
class |
EmptySeqLiteral |
class |
EmptySetLiteral |
class |
FloatLiteral
Float literal.
|
class |
FreeLiteral |
class |
IntLiteral
Int literal.
|
class |
LongLiteral
Long literal.
|
class |
NullLiteral
Null literal.
|
class |
RealLiteral
JML \real literal.
|
class |
StringLiteral |
Modifier and Type | Class and Description |
---|---|
class |
BinaryAnd
Binary and.
|
class |
BinaryAndAssignment
Binary and assignment.
|
class |
BinaryNot
Binary not.
|
class |
BinaryOperator
Operator of arity 2
|
class |
BinaryOr
Binary or.
|
class |
BinaryOrAssignment
Binary or assignment.
|
class |
BinaryXOr
Binary X or.
|
class |
BinaryXOrAssignment
Binary X or assignment.
|
class |
ComparativeOperator
Comparative operator.
|
class |
Conditional
The most weird ternary C operator ?:
|
class |
CopyAssignment
Copy assignment.
|
class |
Divide
Divide.
|
class |
DivideAssignment
Divide assignment.
|
class |
DLEmbeddedExpression |
class |
Equals
Equals.
|
class |
ExactInstanceof
Instanceof.
|
class |
GreaterOrEquals
Greater or equals.
|
class |
GreaterThan
Greater than.
|
class |
Instanceof
Instanceof.
|
class |
Intersect |
class |
LessOrEquals
Less or equals.
|
class |
LessThan
Less than.
|
class |
LogicalAnd
Logical and.
|
class |
LogicalNot
Logical not.
|
class |
LogicalOr
Logical or.
|
class |
Minus
Minus.
|
class |
MinusAssignment
Minus assignment.
|
class |
Modulo
Modulo.
|
class |
ModuloAssignment
Modulo assignment.
|
class |
Negative
Negative.
|
class |
New
The object allocation operator.
|
class |
NewArray
The array allocation operator.
|
class |
NotEquals
Not equals.
|
class |
Plus
Addition or string concatenation operator "+".
|
class |
PlusAssignment
Addition or string concatenation assignment "+=".
|
class |
Positive
Positive.
|
class |
PostDecrement
Post decrement.
|
class |
PostIncrement
Post increment.
|
class |
PreDecrement
Pre decrement.
|
class |
PreIncrement
Pre increment.
|
class |
ShiftLeft
Shift left.
|
class |
ShiftLeftAssignment
Shift left assignment.
|
class |
ShiftRight
Shift right.
|
class |
ShiftRightAssignment
Shift right assignment.
|
class |
Times
Times.
|
class |
TimesAssignment
Times assignment.
|
class |
TypeCast
Type cast.
|
class |
TypeOperator
Type operator.
|
class |
UnsignedShiftRight
Unsigned shift right.
|
class |
UnsignedShiftRightAssignment
Unsigned shift right assignment.
|
Modifier and Type | Class and Description |
---|---|
class |
AllFields |
class |
AllObjects |
class |
SeqConcat |
class |
SeqGet
Represents a sequence getter function.
|
class |
SeqIndexOf
Represents a function giving the index of some element in a sequence (if it exists).
|
class |
SeqLength
Represents a function giving the length of a sequence.
|
class |
SeqReverse |
class |
SeqSingleton |
class |
SeqSub |
class |
SetMinus |
class |
SetUnion |
class |
Singleton |
Modifier and Type | Class and Description |
---|---|
class |
ArrayLengthReference
Array length reference.
|
class |
ArrayReference
Array reference.
|
class |
ExecutionContext |
class |
FieldReference |
class |
MetaClassReference
Meta class reference.
|
class |
MethodReference
Method reference.
|
class |
PackageReference
Package reference.
|
class |
SchematicFieldReference
Field reference.
|
class |
SchemaTypeReference |
class |
SpecialConstructorReference
Occurs in a constructor declaration as the first statement
as this(...) or super(...) reference.
|
class |
SuperConstructorReference
Super constructor reference.
|
class |
SuperReference
Super reference.
|
class |
ThisConstructorReference
This constructor reference.
|
class |
ThisReference
A reference to the current object.
|
class |
TypeRef |
class |
TypeReferenceImp
TypeReferences reference
Type s by name. |
class |
VariableReference |
Modifier and Type | Class and Description |
---|---|
class |
Assert |
class |
BranchImp
Branch.
|
class |
BranchStatement
Branch statement.
|
class |
Break
Break.
|
class |
Case
Case.
|
class |
Catch
Catch.
|
class |
CatchAllStatement |
class |
Ccatch
Ccatch.
|
class |
Continue
Continue.
|
class |
Default
Default.
|
class |
Do
Do.
|
class |
Else
Else.
|
class |
EmptyStatement
Empty statement.
|
class |
EnhancedFor
The new enhanced form of a for-loop.
|
class |
Exec
Exec.
|
class |
ExpressionJumpStatement
Expression jump statement.
|
class |
Finally
Finally.
|
class |
For
For.
|
class |
ForUpdates |
class |
Guard |
class |
If
If.
|
class |
JavaStatement
Default implementation for non-terminal Java statements.
|
class |
JumpStatement
Jump statement.
|
class |
LabeledStatement
Labeled statement.
|
class |
LabelJumpStatement
Label jump statement.
|
class |
LoopInit |
class |
LoopScopeBlock
Loop scope block.
|
class |
LoopStatement
Loop statement.
|
class |
MergePointStatement
A statement indicating a merge point.
|
class |
MethodBodyStatement
A shortcut-statement for a method body, i.e.
|
class |
MethodFrame
The statement inserted by KeY if a method call is executed.
|
class |
Return
Return.
|
class |
Switch
Switch.
|
class |
SynchronizedBlock
Synchronized block.
|
class |
Then
Then.
|
class |
Throw
Throw.
|
class |
TransactionStatement |
class |
Try
Try.
|
class |
While
While.
|
Modifier and Type | Class and Description |
---|---|
class |
ArrayLength |
class |
ArrayPostDecl
Replaces a local variable declaration
#t #v[]; with
#t[] #v; |
class |
ConstructorCall
The constructor call meta construct is used to handle a allocation expression
like
new Class(...) . |
class |
CreateObject
If an allocation expression
new Class(...) occurs, a new object
has to be created, in KeY this is quite similar to take it out of a list of
objects and setting the implicit flag <created> to
true as well as setting all fields of the object to their
default values. |
class |
DoBreak
This class performs a labeled break.
|
class |
EnhancedForElimination
This class defines a meta operator to resolve an enhanced for loop - by transformation to a
"normal" loop.
|
class |
EvaluateArgs
TODO
|
class |
ExpandMethodBody
Replaces the MethodBodyStatement shortcut with the full body, performs prefix
adjustments in the body (execution context).
|
class |
ForInitUnfoldTransformer
Pulls the initializor out of a for-loop.
|
class |
ForToWhile
converts a for-loop to a while loop.
|
class |
InitArray
Split an array creation expression with explicit array initializer,
creating a creation expression with dimension expression and a list
of assignments (-> Java language specification, 15.10)
|
class |
InitArrayCreation
Split an array creation expression with explicit array initializer, creating
a creation expression with dimension expression and a list of assignments (->
Java language specification, 15.10)
This meta construct delivers the creation expression
|
class |
IsStatic
Creates a true or false literal if the given program element is or is not a
static variable reference.
|
class |
MethodCall
Symbolically executes a method invocation
|
class |
MultipleVarDecl
Replaces a declaration of multiple variables by two variable declarations
where the first one declares a single variable and the second one the
remaining variables.
|
class |
PostWork
creates an assignment instantiationOf(#newObjectsV).
|
class |
ProgramTransformer
ProgramTransformers are used to describe schematic transformations
that cannot be expressed by the taclet language itself.
|
class |
ReattachLoopInvariant
Construct for re-attaching a loop invariant that otherwise would get lost
after a transformation, for instance, the loop scope-based unwinding rule.
|
class |
SpecialConstructorCall
The constructor call meta construct is used to handle a allocation expression
like
new Class(...) . |
class |
StaticInitialisation |
class |
SwitchToIf
This class is used to perform program transformations needed for the symbolic
execution of a switch-case statement.
|
class |
TypeOf |
class |
Unpack |
class |
UnwindLoop
This class is used to perform program transformations needed for the symbolic
execution of a loop.
|
Copyright © 2003-2019 The KeY-Project.