Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
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.ldt |
This package contains the "language data types" (LDTs) of KeY.
|
Modifier and Type | Method and Description |
---|---|
static boolean |
TypeConverter.isArithmeticOperator(Operator op) |
protected void |
PrettyPrinter.printOperator(Operator x,
java.lang.String symbol) |
Modifier and Type | Class and Description |
---|---|
class |
Assignment
An assignment is an operator with side-effects.
|
class |
ParenthesizedExpression
Redundant Parentheses.
|
class |
PassiveExpression
Marks an active statement as inactive.
|
Modifier and Type | Method and Description |
---|---|
static boolean |
Operator.precedes(Operator a,
Operator b) |
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 | Method and Description |
---|---|
Function |
DoubleLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
CharListLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
FreeLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
MapLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
RealLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
BooleanLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
PermissionLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
LocSetLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
IntegerLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec)
returns the function symbol for the given operation
null if no function is found for the given operator
|
Function |
HeapLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
FloatLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
SeqLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
abstract Function |
LDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec)
returns the function symbol for the given operation
|
boolean |
DoubleLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
CharListLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
FreeLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
MapLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
RealLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
BooleanLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
PermissionLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
LocSetLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
IntegerLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
HeapLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
FloatLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
SeqLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
abstract boolean |
LDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given java
operator and the logic subterms
|
boolean |
DoubleLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
CharListLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
FreeLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
MapLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
RealLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
BooleanLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
PermissionLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
LocSetLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
IntegerLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
HeapLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
FloatLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
SeqLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
abstract boolean |
LDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given
unary java operator and the logic subterms
|
boolean |
DoubleLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
CharListLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
FreeLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
MapLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
RealLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
BooleanLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
PermissionLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
LocSetLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
IntegerLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
HeapLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
FloatLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
SeqLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
abstract boolean |
LDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given
binary java operator and the logic subterms
|
Copyright © 2003-2019 The KeY-Project.