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.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.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.conditions | |
de.uka.ilkd.key.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
de.uka.ilkd.key.rule.match.legacy | |
de.uka.ilkd.key.rule.match.vm | |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.rule.metaconstruct.arith |
contains classes representing the special meta constructs of
Taclet s performing arithmetic operations. |
de.uka.ilkd.key.strategy.quantifierHeuristics | |
de.uka.ilkd.key.symbolic_execution.strategy.breakpoint |
Modifier and Type | Interface and Description |
---|---|
interface |
Declaration
Declaration.
|
interface |
Expression
Expression
taken from COMPOST and changed to achieve an immutable structure
|
interface |
ExpressionContainer
Expression container.
|
interface |
Label |
interface |
LoopInitializer
Loop initializer.
|
interface |
NamedProgramElement
Named program element.
|
interface |
NonTerminalProgramElement
Non terminal program element.
|
interface |
ParameterContainer
Describes program elements that contain
ParameterDeclaration s. |
interface |
ProgramElement
A part of the program syntax that carries semantics in the model.
|
interface |
ProgramVariableName |
interface |
Reference
References are uses of names, variables or members.
|
interface |
ScopeDefiningElement
The property of a non terminal program element to define a scope.
|
interface |
SourceElement
A source element is a piece of syntax.
|
interface |
Statement
Statement.
|
interface |
StatementContainer
Statement container.
|
interface |
TerminalProgramElement
Terminal program element.
|
interface |
TypeScope
The property of a non terminal program element to define a scope for
types.
|
interface |
VariableScope
The property of a non terminal program element to define a scope for
variables.
|
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 |
JavaSourceElement
Top level implementation of a Java
SourceElement . |
class |
PackageSpecification
Package specification.
|
class |
SingleLineComment
Any non-SingleLineComment is a multi line comment.
|
class |
StatementBlock
Statement block.
|
Modifier and Type | Interface and Description |
---|---|
interface |
MemberDeclaration
Member declaration.
|
interface |
TypeDeclarationContainer
Type declaration container.
|
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 | Interface and Description |
---|---|
interface |
ExpressionStatement
An ExpressionStatement is a statement that may appear as an expression.
|
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 | Interface and Description |
---|---|
interface |
ConstructorReference
Constructor reference.
|
interface |
IExecutionContext
extracted interface to allow schema variabes to stand for an
execution context
|
interface |
MemberReference
Member reference.
|
interface |
MethodName
Method name.
|
interface |
MethodOrConstructorReference |
interface |
NameReference
A NameReference references an entity by its explicite name.
|
interface |
PackageReferenceContainer
Element that contains a PackageReference.
|
interface |
ReferencePrefix
Reference prefix.
|
interface |
ReferenceSuffix
Reference suffix.
|
interface |
TypeReference
TypeReferences reference
Type s by name. |
interface |
TypeReferenceContainer
Type reference container.
|
interface |
TypeReferenceInfix
ReferencePrefix and -suffix that is admissible for outer type references.
|
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 | Interface and Description |
---|---|
interface |
Branch
Branch.
|
interface |
IForUpdates |
interface |
IGuard |
interface |
ILoopInit |
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 | Interface and Description |
---|---|
interface |
ProgramConstruct
A type that implement this interface can be used in all java
programs instead of an expression or statement.
|
interface |
ProgramPrefix
this interface is implemented by program elements that may be matched
by the inactive program prefix
|
interface |
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Modifier and Type | Class and Description |
---|---|
class |
ProgramElementName |
class |
TermImpl
The currently only class implementing the Term interface.
|
static class |
VariableNamer.IndProgramElementName
ProgramElementName carrying an additional index
|
Modifier and Type | Interface and Description |
---|---|
interface |
IObserverFunction |
interface |
IProgramMethod |
interface |
IProgramVariable |
interface |
Operator
All symbols acting as members of a term e.g.
|
interface |
ParsableVariable
This interface represents the variables that can be recognized
by one of the parsers.
|
interface |
QuantifiableVariable
This interface represents the variables that can be bound
(by quantifiers or other binding operators).
|
interface |
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
interface |
SortedOperator
Operator with well-defined argument and result sorts.
|
interface |
TermTransformer
TermTransformer perform complex term transformation which cannot be
(efficiently or at all) described by taclets.
|
interface |
UpdateableOperator
Operators implementing this interface may stand for
locations as well.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractSortedOperator
Abstract sorted operator class offering some common functionality.
|
class |
AbstractSV
Abstract base class for schema variables.
|
class |
AbstractTermTransformer
Abstract class factoring out commonalities of typical term transformer implementations.
|
class |
ElementaryUpdate
Class of operators for elementary updates, i.e., updates of the form
"x := t".
|
class |
Equality
This class defines the equality operator "=".
|
class |
FormulaSV
A schema variable that is used as placeholder for formulas.
|
class |
Function
Objects of this class represent function and predicate symbols.
|
class |
IfExThenElse
This singleton class implements a conditional operator
"\ifEx iv; (phi) \then (t1) \else (t2)", where iv is an integer logic
variable, phi is a formula, and where t1 and t2 are terms with the same sort.
|
class |
IfThenElse
This singleton class implements a general conditional operator
\if (phi) \then (t1) \else (t2).
|
class |
Junctor
Class of junctor operators, i.e., operators connecting
a given number of formula to create another formula.
|
class |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
class |
LogicVariable
The objects of this class represent logical variables,
used e.g.
|
class |
Modality
This class is used to represent a dynamic logic modality like
diamond and box (but also extensions of DL like
preserves and throughout are possible in the future).
|
class |
ModalOperatorSV
Schema variable matching modal operators.
|
class |
ObserverFunction
Objects of this class represent "observer" function or predicate symbols.
|
class |
ProgramConstant
This class represents currently only static final fields initialised with
a compile time constant.
|
class |
ProgramMethod
The program method represents a (pure) method in the logic.
|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
class |
ProgramVariable
The objects of this class represent program variables and program
constants (resulting from static final declarations in programs; TODO: it is
weird that constants are a special case of variables).
|
class |
Quantifier
The two objects of this class represent the universal and the existential
quantifier, respectively.
|
class |
SkolemTermSV
Schema variable that is instantiated with fresh Skolem constants.
|
class |
SortDependingFunction
The objects of this class represent families of function symbols, where
each family contains an instantiation of a template symbol for a particular
sort.
|
class |
SubstOp
Standard first-order substitution operator, resolving clashes but not
preventing (usually unsound) substitution of non-rigid terms across modal
operators.
|
class |
TermLabelSV
A schema variable which matches term labels
|
class |
TermSV
A schema variable that is used as placeholder for terms.
|
class |
Transformer
Functions with a restricted/special rule set only applicable for the top level
of the term transformer and not directly for its arguments, prohibiting any rule
applications to sub arguments as well as applications from outside such as update applications.
|
class |
UpdateApplication
Singleton class defining a binary operator {u}t that applies updates u to
terms, formulas, or other updates t.
|
class |
UpdateJunctor
Class of update junctor operators, i.e., operators connecting
a given number of updates to create another update.
|
class |
UpdateSV
A schema variable that is used as placeholder for updates.
|
class |
VariableSV
Schema variable that is instantiated with logical variables.
|
class |
WarySubstOp |
Modifier and Type | Interface and Description |
---|---|
interface |
ReplacementMap<S extends SVSubstitute,T>
A map to be used in an
OpReplacer . |
static class |
ReplacementMap.DefaultReplacementMap<S extends SVSubstitute,T>
The replacement map type to use if
TermLabelSettings.getUseOriginLabels() is false. |
static class |
ReplacementMap.NoIrrelevantLabelsReplacementMap<S extends SVSubstitute,T>
The replacement map type to use if
TermLabelSettings.getUseOriginLabels() is true. |
Modifier and Type | Method and Description |
---|---|
static <S extends SVSubstitute,T> |
ReplacementMap.create(TermFactory tf,
Proof proof)
Creates a new replacement map.
|
static <S extends SVSubstitute,T> |
ReplacementMap.create(TermFactory tf,
Proof proof,
java.util.Map<S,T> initialMappings)
Creates a new replacement map.
|
Constructor and Description |
---|
OpReplacer(java.util.Map<? extends SVSubstitute,? extends SVSubstitute> map,
TermFactory tf)
Creates an
OpReplacer . |
OpReplacer(java.util.Map<? extends SVSubstitute,? extends SVSubstitute> map,
TermFactory tf)
Creates an
OpReplacer . |
OpReplacer(java.util.Map<? extends SVSubstitute,? extends SVSubstitute> map,
TermFactory tf,
Proof proof)
Creates an
OpReplacer . |
OpReplacer(java.util.Map<? extends SVSubstitute,? extends SVSubstitute> map,
TermFactory tf,
Proof proof)
Creates an
OpReplacer . |
Modifier and Type | Interface and Description |
---|---|
interface |
AbstractProgramElement |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
VariableConditionAdapter.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
VariableCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
abstract boolean |
VariableConditionAdapter.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
MatchConditions |
TacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
Modifier and Type | Method and Description |
---|---|
MatchConditions |
FieldTypeToSortCondition.check(SchemaVariable var,
SVSubstitute svSubst,
MatchConditions matchCond,
Services services) |
MatchConditions |
DropEffectlessElementariesCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
NewJumpLabelCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
IsLabeledCondition.check(SchemaVariable sv,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
SimplifyIfThenElseUpdateCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
LoopVariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
StoreStmtInCondition.check(SchemaVariable sv,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
ObserverCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
HasLoopInvariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
LoopFreeInvariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
EqualUniqueCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
ApplyUpdateOnRigidCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
JavaTypeToSortCondition.check(SchemaVariable var,
SVSubstitute svSubst,
MatchConditions matchCond,
Services services) |
MatchConditions |
LoopInvariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
DropEffectlessStoresCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
StoreTermInCondition.check(SchemaVariable sv,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
SameObserverCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
boolean |
AlternativeVariableCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services)
check whether any of the two delegates apply
|
boolean |
ContainsAssignmentCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
boolean |
AbstractOrInterfaceType.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
MayExpandMethodCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
TypeComparisonCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
ArrayComponentTypeCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
DifferentInstantiationCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
ArrayTypeCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
IsThisReference.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
EnumTypeCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
StaticFieldCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
TermLabelCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
TypeCondition.check(SchemaVariable p_var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
LocalVariableCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
SubFormulaCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
MetaDisjointCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
DifferentFields.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
ConstantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
FinalReferenceCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
FreeLabelInVariableCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
StaticMethodCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
EnumConstantCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
ArrayLengthCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
StaticReferenceCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
abstract boolean |
TypeResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.GenericSortResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.NonGenericSortResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.ElementTypeResolverForSV.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.ContainerTypeResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
abstract Sort |
TypeResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.GenericSortResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.NonGenericSortResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.ElementTypeResolverForSV.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.ContainerTypeResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Modifier and Type | Class and Description |
---|---|
class |
ProgramList |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
LegacyTacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
abstract MatchConditions |
ElementMatcher.match(T op,
SVSubstitute subst,
MatchConditions mc,
Services services) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
VMTacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
Modifier and Type | Class and Description |
---|---|
class |
AddCast |
class |
ArrayBaseInstanceOf
Creates an Type::instance(..) term for the component type of the
array.
|
class |
ArrayLength |
class |
ArrayPostDecl
Replaces a local variable declaration
#t #v[]; with
#t[] #v; |
class |
ConstantValue
Replace a program variable that is a compile-time constant with the
value of the initializer
|
class |
ConstructorCall
The constructor call meta construct is used to handle a allocation expression
like
new Class(...) . |
class |
CreateBeforeLoopUpdate
Initializes the "before loop" update needed for the assignable clause.
|
class |
CreateFrameCond
Creates the frame condition (aka "assignable clause") for the given loop.
|
class |
CreateHeapAnonUpdate
Creates the anonymizing update for the heap.
|
class |
CreateLocalAnonUpdate
Expects a loop body and creates the anonymizing update
out_1:=anon_1||...||out_n:=anon_n , where anon_1, ..., anon_n are
the written variables in the loop body visible to the outside. |
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 |
CreateWellformedCond
Creates the wellformedness condition for the given anonymizing heap terms if
they apply for the current profile and modality type.
|
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 |
EnumConstantValue
resolve a program variable to an integer literal.
|
class |
EvaluateArgs
TODO
|
class |
ExpandMethodBody
Replaces the MethodBodyStatement shortcut with the full body, performs prefix
adjustments in the body (execution context).
|
class |
ExpandQueriesMetaConstruct
Uses the class
QueryExpand in order to insert query expansions in the term that the
meta construct is applied on. |
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 |
IntroAtPreDefsOp |
class |
IsStatic
Creates a true or false literal if the given program element is or is not a
static variable reference.
|
class |
MemberPVToField |
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 |
ObserverEqualityMetaConstruct
This meta contruct allows one to prove equality (equivalence) of two
observer terms if they belong to the same observer function symbol.
|
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.
|
Modifier and Type | Class and Description |
---|---|
class |
DivideLCRMonomials
Metaoperator for computing the result of dividing one monomial by another
|
class |
DivideMonomials
Metaoperator for computing the result of dividing one monomial by another
|
class |
MetaAdd |
class |
MetaArithBitMaskOp |
class |
MetaBinaryAnd |
class |
MetaBinaryOr |
class |
MetaBinaryXOr |
class |
MetaDiv |
class |
MetaEqual |
class |
MetaGeq |
class |
MetaGreater |
class |
MetaLeq |
class |
MetaLess |
class |
MetaMul |
class |
MetaPow
Computes the pow function for literals.
|
class |
MetaShift |
class |
MetaShiftLeft |
class |
MetaShiftRight |
class |
MetaSub |
Modifier and Type | Class and Description |
---|---|
class |
Metavariable
Deprecated.
|
Modifier and Type | Method and Description |
---|---|
java.util.Map<SVSubstitute,SVSubstitute> |
AbstractConditionalBreakpoint.getVariableNamingMap() |
java.util.Map<SVSubstitute,SVSubstitute> |
AbstractConditionalBreakpoint.getVariableNamingMap() |
Modifier and Type | Method and Description |
---|---|
void |
AbstractConditionalBreakpoint.setVariableNamingMap(java.util.Map<SVSubstitute,SVSubstitute> variableNamingMap) |
void |
AbstractConditionalBreakpoint.setVariableNamingMap(java.util.Map<SVSubstitute,SVSubstitute> variableNamingMap) |
Copyright © 2003-2019 The KeY-Project.