Package | Description |
---|---|
de.uka.ilkd.key.java.declaration |
Elements of the Java syntax tree representing declarations.
|
de.uka.ilkd.key.java.expression |
Elements of the Java syntax tree representing expressions.
|
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.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
Modifier and Type | Class and Description |
---|---|
class |
FieldSpecification |
class |
ImplicitFieldSpecification |
class |
VariableSpecification
Variable specification that defines a variable name.
|
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 |
Operator
Operator base class.
|
class |
ParenthesizedExpression
Redundant Parentheses.
|
class |
PassiveExpression
Marks an active statement as inactive.
|
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 | Interface and Description |
---|---|
interface |
ConstructorReference
Constructor reference.
|
interface |
MemberReference
Member reference.
|
interface |
MethodOrConstructorReference |
interface |
TypeReference
TypeReferences reference
Type s by name. |
Modifier and Type | Class and Description |
---|---|
class |
ArrayReference
Array reference.
|
class |
FieldReference |
class |
MethodReference
Method 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 |
TypeRef |
class |
TypeReferenceImp
TypeReferences reference
Type s by name. |
Modifier and Type | Class and Description |
---|---|
class |
Assert |
class |
Case
Case.
|
class |
Do
Do.
|
class |
EnhancedFor
The new enhanced form of a for-loop.
|
class |
ExpressionJumpStatement
Expression jump statement.
|
class |
For
For.
|
class |
ForUpdates |
class |
If
If.
|
class |
LoopScopeBlock
Loop scope block.
|
class |
LoopStatement
Loop statement.
|
class |
MergePointStatement
A statement indicating a merge point.
|
class |
Return
Return.
|
class |
Switch
Switch.
|
class |
SynchronizedBlock
Synchronized block.
|
class |
Throw
Throw.
|
class |
While
While.
|
Modifier and Type | Interface and Description |
---|---|
interface |
ProgramConstruct
A type that implement this interface can be used in all java
programs instead of an expression or statement.
|
Modifier and Type | Class and Description |
---|---|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
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.