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.expression |
Elements of the Java syntax tree representing expressions.
|
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.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
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.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
de.uka.ilkd.key.rule.label | |
de.uka.ilkd.key.rule.match.vm.instructions | |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.strategy.definition | |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.slicing | |
de.uka.ilkd.key.symbolic_execution.util |
Modifier and Type | Field and Description |
---|---|
protected ImmutableArray<Import> |
CompilationUnit.imports
Imports.
|
protected ImmutableArray<TypeDeclaration> |
CompilationUnit.typeDeclarations
Type declarations.
|
Modifier and Type | Method and Description |
---|---|
static ImmutableArray<ProgramPrefix> |
StatementBlock.computePrefixElements(ImmutableArray<? extends Statement> b,
ProgramPrefix current)
computes the prefix elements for the given array of statment block
|
ImmutableArray<? extends Statement> |
StatementBlock.getBody()
Get body.
|
ImmutableArray<TypeDeclaration> |
CompilationUnit.getDeclarations()
Get declarations.
|
ImmutableArray<Import> |
CompilationUnit.getImports()
Get imports.
|
ImmutableArray<Modifier> |
Declaration.getModifiers()
Get the modifiers.
|
ImmutableArray<ProgramPrefix> |
StatementBlock.getPrefixElements() |
ImmutableArray<VariableSpecification> |
CcatchReturnValParameterDeclaration.getVariables() |
protected ImmutableArray<Modifier> |
PrettyPrinter.removeFinal(ImmutableArray<Modifier> ma) |
protected ImmutableArray<Modifier> |
PrettyPrinter.replacePrivateByPublic(ImmutableArray<Modifier> ma) |
Modifier and Type | Method and Description |
---|---|
static ImmutableArray<ProgramPrefix> |
StatementBlock.computePrefixElements(ImmutableArray<? extends Statement> b,
ProgramPrefix current)
computes the prefix elements for the given array of statment block
|
protected boolean |
PrettyPrinter.containsDefaultConstructor(ImmutableArray<MemberDeclaration> members) |
ImmutableList<KeYJavaType> |
JavaInfo.createSignature(ImmutableArray<? extends Expression> arguments)
retrieves the signature according to the given expressions
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ImmutableArray<Modifier> modifiers,
IProgramVariable variable,
Expression init,
KeYJavaType type)
Create a local variable declaration with an arbitrary number of
modifiers.
|
static ProgramElement |
KeYJavaASTFactory.declare(ImmutableArray<Modifier> modifiers,
IProgramVariable variable,
Expression init,
ProgramElementName typeName,
int dimensions,
ReferencePrefix typePrefix,
KeYJavaType baseType)
Create a local array variable declaration with an arbitrary number of
modifiers.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ImmutableArray<Modifier> modifiers,
IProgramVariable variable,
Expression init,
TypeReference typeRef)
Create a local variable declaration with an arbitrary number of
modifiers.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ImmutableArray<Modifier> modifiers,
TypeReference typeRef,
VariableSpecification specification)
Create a local variable declaration.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ImmutableArray<Modifier> modifiers,
TypeReference typeRef,
VariableSpecification[] specifications)
Create local variable declarations.
|
protected ImmutableList<Field> |
CreateArrayMethodBuilder.filterField(ImmutableArray<MemberDeclaration> list)
extracts all field specifications out of the given list.
|
protected int |
JavaNonTerminalProgramElement.getArrayPos(ImmutableArray<ProgramElement> arr,
ProgramElement el)
returns the index of element el in array arr
|
IProgramMethod |
JavaInfo.getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
ImmutableArray<? extends Type> signature,
KeYJavaType context) |
static MethodBodyStatement |
KeYJavaASTFactory.methodBody(ProgramVariable result,
ReferencePrefix reference,
IProgramMethod method,
ImmutableArray<Expression> arguments)
Create a method body shortcut.
|
static MethodReference |
KeYJavaASTFactory.methodCall(KeYJavaType type,
java.lang.String name,
ImmutableArray<? extends Expression> args)
Create a method call on a type.
|
static MethodReference |
KeYJavaASTFactory.methodCall(ReferencePrefix reference,
MethodName name,
ImmutableArray<? extends Expression> args)
Create a method call.
|
static MethodReference |
KeYJavaASTFactory.methodCall(ReferencePrefix reference,
java.lang.String name,
ImmutableArray<? extends Expression> args)
Create a method call.
|
protected ImmutableArray<Modifier> |
PrettyPrinter.removeFinal(ImmutableArray<Modifier> ma) |
protected ImmutableArray<Modifier> |
PrettyPrinter.replacePrivateByPublic(ImmutableArray<Modifier> ma) |
protected void |
PrettyPrinter.writeBlockList(ImmutableArray<? extends ProgramElement> list)
Write block list.
|
protected void |
PrettyPrinter.writeBlockList(int firstLF,
int levelChange,
int firstBlanks,
ImmutableArray<? extends ProgramElement> list)
Write a complete ArrayOf
|
protected void |
PrettyPrinter.writeCommaList(ImmutableArray<? extends ProgramElement> list)
Write comma list.
|
protected void |
PrettyPrinter.writeCommaList(int separationBlanks,
ImmutableArray<? extends ProgramElement> list)
Write comma list.
|
protected void |
PrettyPrinter.writeCommaList(int firstLF,
int levelChange,
int firstBlanks,
ImmutableArray<? extends ProgramElement> list)
Write a complete ArrayOf
|
protected void |
PrettyPrinter.writeImmutableArrayOfProgramElement(int firstLF,
int levelChange,
int firstBlanks,
java.lang.String separationSymbol,
int separationLF,
int separationBlanks,
ImmutableArray<? extends ProgramElement> list)
Write a complete ArrayOf
|
protected void |
PrettyPrinter.writeKeywordList(ImmutableArray<? extends ProgramElement> list)
Write keyword list.
|
protected void |
PrettyPrinter.writeKeywordList(int firstLF,
int levelChange,
int firstBlanks,
ImmutableArray<? extends ProgramElement> list)
Write a complete ArrayOf
|
protected void |
PrettyPrinter.writeLineList(ImmutableArray<? extends ProgramElement> list)
Write line list.
|
protected void |
PrettyPrinter.writeLineList(int firstLF,
int levelChange,
int firstBlanks,
ImmutableArray<? extends ProgramElement> list)
Write a complete ArrayOf
|
Constructor and Description |
---|
StatementBlock(ImmutableArray<? extends Statement> as) |
Modifier and Type | Field and Description |
---|---|
protected ImmutableArray<TypeReference> |
Throws.exceptions
Exceptions.
|
protected ImmutableArray<FieldSpecification> |
FieldDeclaration.fieldSpecs
Field specs.
|
protected ImmutableArray<MemberDeclaration> |
TypeDeclaration.members |
protected ImmutableArray<Modifier> |
JavaDeclaration.modArray
Modifiers.
|
protected ImmutableArray<ParameterDeclaration> |
MethodDeclaration.parameters |
protected ImmutableArray<TypeReference> |
InheritanceSpecification.supertypes
Supertypes.
|
protected ImmutableArray<VariableSpecification> |
ParameterDeclaration.varSpec
Var spec.
|
protected ImmutableArray<VariableSpecification> |
LocalVariableDeclaration.varSpecs
Var specs.
|
Constructor and Description |
---|
JavaDeclaration(ImmutableArray<Modifier> mods) |
LocalVariableDeclaration(ImmutableArray<Modifier> mods,
TypeReference typeRef,
VariableSpecification var)
Local variable declaration.
|
LocalVariableDeclaration(ImmutableArray<Modifier> mods,
TypeReference typeRef,
VariableSpecification[] vars)
Local variable declaration.
|
MethodDeclaration(Modifier[] modifiers,
TypeReference returnType,
ProgramElementName name,
ImmutableArray<ParameterDeclaration> parameters,
Throws exceptions,
StatementBlock body,
boolean parentIsInterfaceDeclaration)
Method declaration.
|
VariableDeclaration(ImmutableArray<Modifier> mods,
TypeReference typeRef,
boolean parentIsInterfaceDeclaration)
Variable declaration.
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableArray<Expression> |
ArrayInitializer.children |
protected ImmutableArray<Expression> |
Operator.children
Children.
|
Modifier and Type | Method and Description |
---|---|
ImmutableArray<Expression> |
ArrayInitializer.getArguments()
Get arguments.
|
ImmutableArray<Expression> |
Operator.getArguments()
return arguments
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableArray<? extends Expression> |
MethodReference.arguments
Arguments.
|
protected ImmutableArray<Expression> |
SpecialConstructorReference.arguments |
protected ImmutableArray<Expression> |
ArrayReference.inits
Inits.
|
Modifier and Type | Method and Description |
---|---|
ImmutableArray<? extends Expression> |
MethodReference.getArguments()
Get arguments.
|
ImmutableArray<Expression> |
SpecialConstructorReference.getArguments()
Get arguments.
|
ImmutableArray<? extends Expression> |
MethodOrConstructorReference.getArguments() |
ImmutableArray<Expression> |
ArrayReference.getDimensionExpressions()
Get dimension expressions.
|
Constructor and Description |
---|
MethodReference(ImmutableArray<? extends Expression> args,
MethodName n,
ReferencePrefix p) |
MethodReference(ImmutableArray<Expression> args,
MethodName n,
ReferencePrefix p,
PositionInfo pos) |
SpecialConstructorReference(ImmutableArray<Expression> arguments)
Special constructor reference.
|
SuperConstructorReference(ReferencePrefix accessPath,
ImmutableArray<Expression> arguments)
Super constructor reference.
|
ThisConstructorReference(ImmutableArray<Expression> arguments)
This constructor reference.
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableArray<Statement> |
Default.body
Body.
|
protected ImmutableArray<Statement> |
Case.body
Body.
|
protected ImmutableArray<Branch> |
Switch.branches
Branches.
|
Constructor and Description |
---|
Exec(StatementBlock body,
ImmutableArray<Branch> branches)
Exec.
|
ForUpdates(ImmutableArray<Expression> exprarr) |
LoopInit(ImmutableArray<LoopInitializer> exprarr) |
MethodBodyStatement(IProgramMethod method,
ReferencePrefix newContext,
IProgramVariable res,
ImmutableArray<Expression> args) |
MethodBodyStatement(IProgramMethod method,
ReferencePrefix newContext,
IProgramVariable res,
ImmutableArray<Expression> args,
boolean useSpecification) |
MethodBodyStatement(IProgramMethod method,
ReferencePrefix newContext,
IProgramVariable res,
ImmutableArray<Expression> args,
boolean useSpecification,
ProgramElement scope) |
MethodBodyStatement(IProgramMethod method,
ReferencePrefix newContext,
IProgramVariable res,
ImmutableArray<Expression> args,
ProgramElement scope) |
Try(StatementBlock body,
ImmutableArray<Branch> branches)
Try.
|
Modifier and Type | Method and Description |
---|---|
protected void |
CreatingASTVisitor.addChildren(ImmutableArray<ProgramElement> arr) |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<QuantifiableVariable> |
TermImpl.boundVars() |
ImmutableArray<QuantifiableVariable> |
Term.boundVars()
The logical variables bound by the top level operator.
|
ImmutableArray<TermLabel> |
TermImpl.getLabels() |
ImmutableArray<TermLabel> |
Term.getLabels()
returns list of labels attached to this term
|
ImmutableArray<ProgramPrefix> |
ProgramPrefix.getPrefixElements()
returns an array with all prefix elements starting at
this element
|
protected static ImmutableArray<QuantifiableVariable> |
ClashFreeSubst.getSingleArray(ImmutableArray<QuantifiableVariable>[] bv) |
ImmutableArray<Term> |
TermImpl.subs() |
ImmutableArray<Term> |
Term.subs()
The subterms.
|
ImmutableArray<QuantifiableVariable> |
BoundVariableTools.unifyBoundVariables(ImmutableArray<QuantifiableVariable>[] boundVarsPerSub,
Term[] subs,
int subtermsBegin,
int subtermsEnd,
TermServices services)
Ensure that for the subterms with indexes [
subtermsBegin ,
subtermsEnd ) the same variables are bound. |
ImmutableArray<QuantifiableVariable> |
TermImpl.varsBoundHere(int n) |
ImmutableArray<QuantifiableVariable> |
Term.varsBoundHere(int n)
The logical variables bound by the top level operator for the nth
subterm.
|
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.addLabel(Term term,
ImmutableArray<TermLabel> labels)
Adds labels to a term, removing any existing labels of the same type.
|
Term |
TermBuilder.addLabelToAllSubs(Term term,
ImmutableArray<TermLabel> labels)
Applies the labels to the term and almost every (direct or indirect) sub-term recursively.
|
Term |
TermBuilder.apply(Term update,
Term target,
ImmutableArray<TermLabel> labels) |
protected void |
ClashFreeSubst.applyOnSubterm(Term completeTerm,
int subtermIndex,
Term[] newSubterms,
ImmutableArray<QuantifiableVariable>[] newBoundVars)
Apply the substitution of the subterm
subtermIndex of
term/formula completeTerm . |
boolean |
BoundVariableTools.consistentVariableArrays(ImmutableArray<QuantifiableVariable> ar0,
ImmutableArray<QuantifiableVariable> ar1) |
boolean |
BoundVariableTools.consistentVariableArrays(ImmutableArray<QuantifiableVariable> ar0,
ImmutableArray<QuantifiableVariable> ar1) |
Term |
TermFactory.createTerm(Operator op,
ImmutableArray<Term> subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock) |
Term |
TermFactory.createTerm(Operator op,
ImmutableArray<Term> subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock) |
Term |
TermFactory.createTerm(Operator op,
ImmutableArray<Term> subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock,
ImmutableArray<TermLabel> labels)
Master method for term creation.
|
Term |
TermFactory.createTerm(Operator op,
ImmutableArray<Term> subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock,
ImmutableArray<TermLabel> labels)
Master method for term creation.
|
Term |
TermFactory.createTerm(Operator op,
ImmutableArray<Term> subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock,
ImmutableArray<TermLabel> labels)
Master method for term creation.
|
Term |
TermFactory.createTerm(Operator op,
ImmutableArray<TermLabel> labels) |
Term |
TermFactory.createTerm(Operator op,
Term[] subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock) |
Term |
TermFactory.createTerm(Operator op,
Term[] subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock,
ImmutableArray<TermLabel> labels) |
Term |
TermFactory.createTerm(Operator op,
Term[] subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock,
ImmutableArray<TermLabel> labels) |
Term |
TermFactory.createTerm(Operator op,
Term[] subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock,
TermLabel label) |
Term |
TermFactory.createTerm(Operator op,
Term[] subs,
ImmutableArray<TermLabel> labels) |
Term |
TermFactory.createTerm(Operator op,
Term sub,
ImmutableArray<TermLabel> labels) |
Term |
TermFactory.createTerm(Operator op,
Term sub1,
Term sub2,
ImmutableArray<TermLabel> labels) |
boolean |
BoundVariableTools.equalsModRenaming(ImmutableArray<QuantifiableVariable> vars0,
Term term0,
ImmutableArray<QuantifiableVariable> vars1,
Term term1,
TermServices services) |
boolean |
BoundVariableTools.equalsModRenaming(ImmutableArray<QuantifiableVariable> vars0,
Term term0,
ImmutableArray<QuantifiableVariable> vars1,
Term term1,
TermServices services) |
Term |
TermBuilder.func(Function f,
Term[] s,
ImmutableArray<QuantifiableVariable> boundVars) |
protected static ImmutableArray<QuantifiableVariable> |
ClashFreeSubst.getSingleArray(ImmutableArray<QuantifiableVariable>[] bv) |
Term |
TermBuilder.imp(Term t1,
Term t2,
ImmutableArray<TermLabel> labels) |
Term |
TermBuilder.label(Term term,
ImmutableArray<TermLabel> labels)
Applies labels to a term, removing any existing labels.
|
Term |
TermBuilder.prog(Modality mod,
JavaBlock jb,
Term t,
ImmutableArray<TermLabel> labels) |
Term[] |
BoundVariableTools.renameVariables(Term[] originalTerms,
ImmutableArray<QuantifiableVariable> oldBoundVars,
ImmutableArray<QuantifiableVariable> newBoundVars,
TermServices services) |
Term[] |
BoundVariableTools.renameVariables(Term[] originalTerms,
ImmutableArray<QuantifiableVariable> oldBoundVars,
ImmutableArray<QuantifiableVariable> newBoundVars,
TermServices services) |
Term |
BoundVariableTools.renameVariables(Term originalTerm,
ImmutableArray<QuantifiableVariable> oldBoundVars,
ImmutableArray<QuantifiableVariable> newBoundVars,
TermServices services)
Compare the arrays
oldBoundVars and
newBoundVars component-wise, and in case of differences
substitute variables from the former array with the ones of the latter
array (in originalTerm ) |
Term |
BoundVariableTools.renameVariables(Term originalTerm,
ImmutableArray<QuantifiableVariable> oldBoundVars,
ImmutableArray<QuantifiableVariable> newBoundVars,
TermServices services)
Compare the arrays
oldBoundVars and
newBoundVars component-wise, and in case of differences
substitute variables from the former array with the ones of the latter
array (in originalTerm ) |
boolean |
BoundVariableTools.resolveCollisions(ImmutableArray<QuantifiableVariable> oldVars,
QuantifiableVariable[] newVars,
ImmutableSet<QuantifiableVariable> criticalVars)
Replace all variables of
oldVars that also turn up in
criticalPairs with new variables (currently just with the
same name). |
boolean |
BoundVariableTools.resolveCollisions(Term originalTerm,
ImmutableSet<QuantifiableVariable> criticalVars,
ImmutableArray<QuantifiableVariable>[] newBoundVars,
Term[] newSubs,
TermServices services)
Ensure that none of the variables
criticalVars is bound by
the top-level operator of t (by bound renaming). |
protected boolean |
ClashFreeSubst.subTermChanges(ImmutableArray<QuantifiableVariable> boundVars,
Term subTerm)
returns true if
subTerm bound by
boundVars would change under application of this
substitution. |
ImmutableArray<QuantifiableVariable> |
BoundVariableTools.unifyBoundVariables(ImmutableArray<QuantifiableVariable>[] boundVarsPerSub,
Term[] subs,
int subtermsBegin,
int subtermsEnd,
TermServices services)
Ensure that for the subterms with indexes [
subtermsBegin ,
subtermsEnd ) the same variables are bound. |
Constructor and Description |
---|
TermImpl(Operator op,
ImmutableArray<Term> subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock)
Constructs a term for the given operator, with the given sub terms,
bounded variables and (if applicable) the code block on this term.
|
TermImpl(Operator op,
ImmutableArray<Term> subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock)
Constructs a term for the given operator, with the given sub terms,
bounded variables and (if applicable) the code block on this term.
|
Modifier and Type | Method and Description |
---|---|
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
protected ImmutableArray<TermLabel> |
TermLabelManager.performRefactoring(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
ImmutableList<TermLabelRefactoring> activeRefactorings)
Computes the new labels as part of the refactoring for the given
Term . |
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<Name,ChildTermLabelPolicy> |
TermLabelManager.computeActiveChildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificPolicies,
java.util.Map<Name,ChildTermLabelPolicy> ruleIndependentPolicies)
Computes active
ChildTermLabelPolicy instances which have to be executed during the given rule application. |
protected java.util.Map<Name,ChildTermLabelPolicy> |
TermLabelManager.computeActiveChildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificPolicies,
java.util.Map<Name,ChildTermLabelPolicy> ruleIndependentPolicies)
Computes active
ChildTermLabelPolicy instances which have to be executed during the given rule application. |
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
protected void |
TermLabelManager.performChildAndGrandchildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,ChildTermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild
ChildTermLabelPolicy instances. |
protected void |
TermLabelManager.performChildAndGrandchildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,ChildTermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild
ChildTermLabelPolicy instances. |
protected void |
TermLabelManager.performDirectChildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,ChildTermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given direct
ChildTermLabelPolicy instances. |
protected void |
TermLabelManager.performDirectChildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,ChildTermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given direct
ChildTermLabelPolicy instances. |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given
TermLabelPolicy instances. |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given
TermLabelPolicy instances. |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given
TermLabelPolicy instances. |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels,
TermLabel label)
Performs the given
TermLabelPolicy instances. |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels,
TermLabel label)
Performs the given
TermLabelPolicy instances. |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels,
TermLabel label)
Performs the given
TermLabelPolicy instances. |
protected void |
TermLabelManager.performUpdater(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableList<TermLabelUpdate> updater,
java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild
TermLabelUpdate instances. |
protected void |
TermLabelManager.performUpdater(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableList<TermLabelUpdate> updater,
java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild
TermLabelUpdate instances. |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<Sort> |
SortedOperator.argSorts() |
ImmutableArray<Sort> |
AbstractSortedOperator.argSorts() |
ImmutableArray<LoopInitializer> |
ProgramSV.getInits() |
ImmutableArray<Modifier> |
ProgramMethod.getModifiers() |
ImmutableArray<Modifier> |
ProgramSV.getModifiers() |
ImmutableArray<ParameterDeclaration> |
ProgramMethod.getParameters() |
ImmutableArray<ParameterDeclaration> |
IProgramMethod.getParameters() |
ImmutableArray<ParameterDeclaration> |
ProgramSV.getParameters() |
ImmutableArray<KeYJavaType> |
IObserverFunction.getParamTypes()
Returns the parameter types of this observer symbol.
|
ImmutableArray<KeYJavaType> |
IProgramMethod.getParamTypes() |
ImmutableArray<KeYJavaType> |
ProgramSV.getParamTypes() |
ImmutableArray<KeYJavaType> |
ObserverFunction.getParamTypes() |
ImmutableArray<Expression> |
ProgramSV.getUpdates() |
Modifier and Type | Method and Description |
---|---|
static Transformer |
Transformer.getTransformer(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
TermServices services)
Looks up the function namespace for a term transformer with the given
attributes, assuming it to be uniquely defined by its name.
|
Sort |
SubstOp.sort(ImmutableArray<Term> terms) |
Sort |
IfThenElse.sort(ImmutableArray<Term> terms) |
Sort |
AbstractSortedOperator.sort(ImmutableArray<Term> terms) |
Sort |
UpdateApplication.sort(ImmutableArray<Term> terms) |
Sort |
Operator.sort(ImmutableArray<Term> terms)
Determines the sort of the
Term if it would be created using this
Operator as top level operator and the given terms as sub terms. |
Sort |
IfExThenElse.sort(ImmutableArray<Term> terms) |
Constructor and Description |
---|
AbstractSortedOperator(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
boolean isRigid) |
AbstractSortedOperator(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean isRigid) |
AbstractSortedOperator(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean isRigid) |
AbstractSV(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
boolean isRigid,
boolean isStrict) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean unique) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean unique) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean unique,
boolean isSkolemConstant) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean unique,
boolean isSkolemConstant) |
ObserverFunction(java.lang.String baseName,
Sort sort,
KeYJavaType type,
Sort heapSort,
KeYJavaType container,
boolean isStatic,
ImmutableArray<KeYJavaType> paramTypes,
int heapCount,
int stateCount) |
Transformer(Name name,
Sort sort,
ImmutableArray<Sort> argSorts) |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<TermLabel> |
ExpressionBuilder.visitLabel(KeYParser.LabelContext ctx) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableArray<TermLabel> |
LogicPrinter.getVisibleTermLabels(Term t)
Determine the Set of labels that will be printed out for a specific
Term . |
protected ImmutableArray<TermLabel> |
SequentViewLogicPrinter.getVisibleTermLabels(Term t) |
Modifier and Type | Method and Description |
---|---|
void |
LogicPrinter.printQuantifierTerm(java.lang.String name,
ImmutableArray<QuantifiableVariable> vars,
Term phi,
int ass)
Print a quantified term.
|
Modifier and Type | Method and Description |
---|---|
ImmutableArray<QuantifiableVariable> |
OpReplacer.replace(ImmutableArray<QuantifiableVariable> vars)
Replaces in an ImmutableArray
|
Modifier and Type | Method and Description |
---|---|
ImmutableArray<QuantifiableVariable> |
OpReplacer.replace(ImmutableArray<QuantifiableVariable> vars)
Replaces in an ImmutableArray
|
Modifier and Type | Method and Description |
---|---|
ImmutableArray<ProgramElement> |
ProgramList.getList() |
ImmutableArray<TermLabel> |
SVInstantiations.UpdateLabelPair.getUpdateApplicationlabels() |
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
ImmutableArray<TermLabel> labels,
Services services) |
SVInstantiations |
SVInstantiations.addUpdate(Term update,
ImmutableArray<TermLabel> updateApplicationlabels)
adds an update to the update context
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
ImmutableArray<ProgramElement> pes,
Services services)
replaces the given pair in the instantiations.
|
Constructor and Description |
---|
ProgramList(ImmutableArray<ProgramElement> list) |
UpdateLabelPair(Term update,
ImmutableArray<TermLabel> updateApplicationlabels) |
Modifier and Type | Method and Description |
---|---|
boolean |
ChildTermLabelPolicy.addLabel(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
Term childTerm,
TermLabel label)
|
boolean |
ChildTermLabelPolicy.addLabel(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
Term childTerm,
TermLabel label)
|
boolean |
ChildTermLabelPolicy.isRuleApplicationSupported(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock)
Decides if the currently active
Rule application is supported or not. |
boolean |
ChildTermLabelPolicy.isRuleApplicationSupported(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock)
Decides if the currently active
Rule application is supported or not. |
TermLabel |
OriginTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label) |
TermLabel |
OriginTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label) |
TermLabel |
OriginTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label) |
TermLabel |
TermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
TermLabel |
TermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
TermLabel |
TermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
TermLabel |
PerpetualTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label) |
TermLabel |
PerpetualTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label) |
TermLabel |
PerpetualTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label) |
TermLabel |
StayOnOperatorTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
TermLabel |
StayOnOperatorTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
TermLabel |
StayOnOperatorTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
TermLabel |
StayOnFormulaTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
TermLabel |
StayOnFormulaTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
TermLabel |
StayOnFormulaTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
static FormulaTermLabel |
StayOnFormulaTermLabelPolicy.searchFormulaTermLabel(ImmutableArray<TermLabel> labels)
Searches the
FormulaTermLabel in the given TermLabel s. |
void |
TermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
TermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
FormulaTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
FormulaTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
LoopBodyTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
LoopBodyTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
BlockContractValidityTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
BlockContractValidityTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
SymbolicExecutionTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
SymbolicExecutionTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
LoopInvariantNormalBehaviorTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
LoopInvariantNormalBehaviorTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
Modifier and Type | Method and Description |
---|---|
static MatchInstruction |
Instruction.matchAndBindVariables(ImmutableArray<QuantifiableVariable> boundVars) |
static MatchInstruction |
Instruction.matchTermLabelSV(ImmutableArray<TermLabel> labels) |
static MatchInstruction |
Instruction.unbindVariables(ImmutableArray<QuantifiableVariable> boundVars) |
Constructor and Description |
---|
BindVariablesInstruction(ImmutableArray<QuantifiableVariable> boundVars) |
MatchTermLabelInstruction(ImmutableArray<TermLabel> labels) |
Modifier and Type | Field and Description |
---|---|
protected ImmutableArray<Expression> |
MethodCall.arguments |
Modifier and Type | Method and Description |
---|---|
protected ImmutableArray<Expression> |
InitArray.extractInitializers(NewArray p_creationExpression)
Extract the variable initializers from the array initializer
|
Modifier and Type | Field and Description |
---|---|
ImmutableArray<TermLabel> |
PositionedLabeledString.labels |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<TermLabel> |
PositionedString.getLabels()
returns list of labels attached to this positioned string
|
ImmutableArray<TermLabel> |
PositionedLabeledString.getLabels()
returns the labels attached to this positioned string
|
Modifier and Type | Method and Description |
---|---|
PositionedLabeledString |
PositionedString.label(ImmutableArray<TermLabel> labels) |
Constructor and Description |
---|
PositionedLabeledString(java.lang.String text,
ImmutableArray<TermLabel> labels) |
PositionedLabeledString(java.lang.String text,
java.lang.String fileName,
ImmutableArray<TermLabel> labels) |
PositionedLabeledString(java.lang.String text,
java.lang.String fileName,
Position pos,
ImmutableArray<TermLabel> labels) |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<AbstractStrategyPropertyDefinition> |
StrategySettingsDefinition.getProperties()
Returns the definition of controls to edit
StrategyProperties . |
ImmutableArray<AbstractStrategyPropertyDefinition> |
AbstractStrategyPropertyDefinition.getSubProperties()
Returns children which edits related properties to this.
|
ImmutableArray<StrategyPropertyValueDefinition> |
OneOfStrategyPropertyDefinition.getValues()
Returns The possible
StrategyPropertyValueDefinition which the user can select. |
Modifier and Type | Method and Description |
---|---|
static boolean |
TruthValueTracingUtil.isIfThenElseFormula(Operator operator,
ImmutableArray<Term> subs)
|
static boolean |
TruthValueTracingUtil.isLogicOperator(Operator operator,
ImmutableArray<Term> subs)
|
Modifier and Type | Method and Description |
---|---|
protected abstract ImmutableArray<Node> |
AbstractSlicer.doSlicing(Node seedNode,
Location seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Performs the slicing.
|
ImmutableArray<Node> |
AbstractBackwardSlicer.doSlicing(Node seedNode,
Location seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Performs the slicing.
|
ImmutableArray<Term> |
Access.getDimensionExpressions()
Returns the accessed array index or
null if it is not an array access. |
ImmutableArray<Node> |
AbstractSlicer.slice(Node seedNode,
Location seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the slice.
|
ImmutableArray<Node> |
AbstractSlicer.slice(Node seedNode,
ReferencePrefix seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the slice.
|
ImmutableArray<Node> |
AbstractSlicer.slice(Node seedNode,
Term term,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the slice.
|
static ImmutableArray<Term> |
AbstractSlicer.toTerm(Services services,
ImmutableArray<Expression> expressions,
ExecutionContext ec)
Converts the given
Expression s into Term s. |
Modifier and Type | Method and Description |
---|---|
static ImmutableArray<Term> |
AbstractSlicer.toTerm(Services services,
ImmutableArray<Expression> expressions,
ExecutionContext ec)
Converts the given
Expression s into Term s. |
Constructor and Description |
---|
Access(ImmutableArray<Term> dimensionExpressions)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected static ImmutableArray<Term> |
SymbolicExecutionUtil.extractValueFromUpdate(Term term,
IProgramVariable variable)
Utility method to extract the value of the
IProgramVariable
from the given update term. |
Copyright © 2003-2019 The KeY-Project.