Package | Description |
---|---|
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.gui.extension.api | |
de.uka.ilkd.key.informationflow.rule | |
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.mgt |
This package contains classes for proof environments and proof management.
|
de.uka.ilkd.key.proof.rulefilter | |
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.label | |
de.uka.ilkd.key.rule.merge | |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.smt |
This package contains the SMT backend of KeY, allowing to translate KeY formulas
to formulas in formats such as SMT-LIB, and allowing to send such formulas to
SMT solvers such as Simplify or Z3.
|
de.uka.ilkd.key.strategy.quantifierHeuristics | |
de.uka.ilkd.key.symbolic_execution.rule |
Modifier and Type | Method and Description |
---|---|
Rule |
InfoTreeNode.getRule() |
Modifier and Type | Method and Description |
---|---|
java.util.List<javax.swing.Action> |
ContextMenuAdapter.getContextActions(KeYMediator mediator,
ContextMenuKind kind,
Rule underlyingObject) |
Modifier and Type | Class and Description |
---|---|
class |
InfFlowContractAppTaclet
A normal RewriteTaclet except that the formula which is added by this taclet
is also added to the list of formulas contained in the
INF_FLOW_CONTRACT_APPL_PROPERTY.
|
Modifier and Type | Method and Description |
---|---|
static boolean |
InfFlowContractAppTaclet.hasType(Rule rule) |
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 TermLabelManager.RefactoringsContainer |
TermLabelManager.computeRefactorings(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Computes the
TermLabelRefactoring to consider. |
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)
|
static Term |
TermLabelManager.label(Services services,
TermLabelState state,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
TermLabelManager.instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp,
Goal, Object, Term, Operator, ImmutableArray, ImmutableArray,
JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
TermLabelManager.refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object,
Rule, Term) . |
static Term |
TermLabelManager.label(Services services,
TermLabelState state,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
TermLabelManager.instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp,
Goal, Object, Term, Operator, ImmutableArray, ImmutableArray,
JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
TermLabelManager.refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object,
Rule, Term) . |
Term |
TermLabelManager.label(TermLabelState state,
Services services,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
TermLabelManager.instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp,
Goal, Object, Term, Operator, ImmutableArray, ImmutableArray,
JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
TermLabelManager.refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object,
Rule, Term) . |
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 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 . |
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.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 Term |
TermLabelManager.refactorApplicationTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
TermLabelManager.RefactoringsContainer refactorings,
TermFactory tf)
Refactors the labels of the application term.
|
static void |
TermLabelManager.refactorGoal(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
void |
TermLabelManager.refactorGoal(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
protected Term |
TermLabelManager.refactorLabelsRecursive(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
ImmutableList<TermLabelRefactoring> activeRefactorings)
|
protected void |
TermLabelManager.refactorSemisequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Semisequent semisequent,
boolean inAntec,
ImmutableList<TermLabelRefactoring> activeRefactorings)
Performs a
TermLabel refactoring on the given Semisequent . |
static void |
TermLabelManager.refactorSequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
void |
TermLabelManager.refactorSequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
Term |
TermLabelManager.refactorSequentFormula(TermLabelState state,
Services services,
Term sequentFormula,
PosInOccurrence applicationPosInOccurrence,
Goal goal,
java.lang.Object hint,
Rule rule,
Term tacletTerm)
|
static Term |
TermLabelManager.refactorSequentFormula(TermLabelState state,
Services services,
Term sequentFormula,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
|
Term |
TermLabelManager.refactorTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Goal goal,
java.lang.Object hint,
Rule rule,
Term tacletTerm)
Refactors all labels in the given application
Term . |
static Term |
TermLabelManager.refactorTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
protected Term |
TermLabelManager.replaceTerm(TermLabelState state,
PosInOccurrence pio,
Term newTerm,
TermFactory tf,
ImmutableList<TermLabelRefactoring> parentRefactorings,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Replaces the
Term at the specified PosInOccurrence . |
Modifier and Type | Method and Description |
---|---|
RuleJustification |
Profile.getJustification(Rule r)
returns the (default) justification for the given rule
|
RuleJustification |
JavaProfile.getJustification(Rule r)
determines the justification of rule
r . |
RuleJustification |
AbstractProfile.getJustification(Rule r)
any standard rule has is by default justified by an axiom rule
justification
|
void |
InitConfig.registerRule(Rule r,
RuleJustification j)
registers a rule with the given justification at the
justification managing
RuleJustification object of this
environment. |
Modifier and Type | Method and Description |
---|---|
void |
InitConfig.registerRules(java.lang.Iterable<? extends Rule> s,
RuleJustification j)
registers a list of rules with the given justification at the
justification managing
RuleJustification object of this
environment. |
Modifier and Type | Method and Description |
---|---|
void |
RuleJustificationInfo.addJustification(Rule r,
RuleJustification j) |
RuleJustification |
RuleJustificationInfo.getJustification(Rule r) |
void |
RuleJustificationInfo.removeJustificationFor(Rule rule) |
Modifier and Type | Method and Description |
---|---|
void |
SetRuleFilter.addRuleToSet(Rule rule) |
boolean |
SetRuleFilter.filter(Rule rule) |
boolean |
TacletFilter.filter(Rule rule) |
boolean |
NotRuleFilter.filter(Rule rule) |
boolean |
AndRuleFilter.filter(Rule rule) |
boolean |
ClassRuleFilter.filter(Rule rule) |
boolean |
RuleFilter.filter(Rule rule) |
Modifier and Type | Interface and Description |
---|---|
interface |
BuiltInRule
Buit-in rule interface.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractAuxiliaryContractRule
Rule for the application of
AuxiliaryContract s. |
class |
AbstractBlockContractRule
Rule for the application of
BlockContract s. |
class |
AbstractLoopContractRule
Rule for the application of
LoopContract s. |
class |
AbstractLoopInvariantRule
An abstract super class for loop invariant rules.
|
class |
AntecTaclet
An AntecTaclet represents a taclet whose find part has to match a top level
formula in the antecedent of the sequent.
|
class |
BlockContractExternalRule
Rule for the application of
BlockContract s. |
class |
BlockContractInternalRule
Rule for the application of
BlockContract s. |
class |
FindTaclet
An abstract class to represent Taclets with a find part.
|
class |
LoopApplyHeadRule
This rule transforms a block that starts with a for loop into one that starts with a while loop.
|
class |
LoopContractExternalRule
Rule for the application of
LoopContract s. |
class |
LoopContractInternalRule
Rule for the application of
LoopContract s. |
class |
LoopScopeInvariantRule
Implementation of the "loop scope invariant" rule as
proposed in the PhD thesis by Nathan Wasser.
|
class |
NoFindTaclet
Used to implement a Taclet that has no find part.
|
class |
OneStepSimplifier |
class |
QueryExpand
The QueryExpand rule allows to apply contracts or to symbolically execute a query
expression in the logic.
|
class |
RewriteTaclet
A RewriteTaclet represents a taclet, whose find can be matched against any
term in the sequent no matter where it occurs.
|
class |
SuccTaclet
A SuccTaclet represents a taclet whose find part has to match a top level
formula in the succedent of the sequent.
|
class |
Taclet
Taclets are the DL-extension of schematic theory specific rules.
|
class |
UseDependencyContractRule |
class |
UseOperationContractRule
Implements the rule which inserts operation contracts for a method call.
|
class |
WhileInvariantRule |
Modifier and Type | Field and Description |
---|---|
Rule |
RuleKey.r |
protected Rule |
SyntacticalReplaceVisitor.rule |
Modifier and Type | Method and Description |
---|---|
Rule |
TacletApp.rule()
returns the rule the application information is collected for
|
Rule |
RuleApp.rule()
returns the rule of this rule application
|
Constructor and Description |
---|
RuleKey(Rule r) |
SyntacticalReplaceVisitor(TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
Goal goal,
Rule rule,
RuleApp ruleApp,
Services services,
TermBuilder termBuilder) |
SyntacticalReplaceVisitor(TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
SVInstantiations svInst,
Goal goal,
Rule rule,
RuleApp ruleApp,
Services services)
constructs a term visitor replacing any occurrence of a schemavariable found
in
svInst by its instantiation |
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)
|
TermLabelRefactoring.RefactoringScope |
TermLabelRefactoring.defineRefactoringScope(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Defines if a refactoring is required and if so in which
TermLabelRefactoring.RefactoringScope . |
TermLabelRefactoring.RefactoringScope |
OriginTermLabelRefactoring.defineRefactoringScope(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm) |
TermLabelRefactoring.RefactoringScope |
FormulaTermLabelRefactoring.defineRefactoringScope(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Defines if a refactoring is required and if so in which
TermLabelRefactoring.RefactoringScope . |
TermLabelRefactoring.RefactoringScope |
RemoveInCheckBranchesTermLabelRefactoring.defineRefactoringScope(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Defines if a refactoring is required and if so in which
TermLabelRefactoring.RefactoringScope . |
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 |
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 |
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)
|
void |
TermLabelRefactoring.refactorLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
java.util.List<TermLabel> labels)
This method is used to refactor the labels of the given
Term . |
void |
OriginTermLabelRefactoring.refactorLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
java.util.List<TermLabel> labels) |
void |
FormulaTermLabelRefactoring.refactorLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
java.util.List<TermLabel> labels)
This method is used to refactor the labels of the given
Term . |
void |
RemoveInCheckBranchesTermLabelRefactoring.refactorLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
java.util.List<TermLabel> labels)
This method is used to refactor the labels of the given
Term . |
static boolean |
TermLabelRefactoring.shouldRefactorOnBuiltInRule(Rule rule,
Goal goal,
java.lang.Object hint)
Determines whether any refatorings should be applied on an application of the given
BuiltInRule . |
protected boolean |
FormulaTermLabelRefactoring.shouldRefactorSpecificationApplication(Rule rule,
Goal goal,
java.lang.Object hint)
Checks if the given hint requires a refactoring.
|
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 |
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 |
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)
|
Modifier and Type | Class and Description |
---|---|
class |
CloseAfterMerge
Rule for closing a partner goal after a merge operation.
|
class |
MergeRule
Base for implementing merge rules.
|
Modifier and Type | Method and Description |
---|---|
Term |
WhileInvariantTransformer.transform(TermLabelState termLabelState,
Rule rule,
RuleApp ruleApp,
Goal goal,
Sequent applicationSequent,
PosInOccurrence applicationPos,
Term initialPost,
Term invariantFramingTermination,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Modifier and Type | Class and Description |
---|---|
static class |
RuleAppSMT.SMTRule |
Constructor and Description |
---|
ConstraintAwareSyntacticalReplaceVisitor(TermLabelState termLabelState,
Services services,
Constraint metavariableInst,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Taclet.TacletLabelHint labelHint,
Goal goal) |
Modifier and Type | Class and Description |
---|---|
class |
AbstractSideProofRule
Provides the basic functionality of
BuiltInRule which
computes something in a side proof. |
class |
ModalitySideProofRule
A
BuiltInRule which evaluates a modality in a side proof. |
class |
QuerySideProofRule
A
BuiltInRule which evaluates a query in a side proof. |
Copyright © 2003-2019 The KeY-Project.