Modifier and Type | Method and Description |
---|---|
void |
AbstractProofControl.applyInteractive(RuleApp app,
Goal goal) |
void |
ProofControl.applyInteractive(RuleApp app,
Goal goal)
Apply a RuleApp and continue with update simplification or strategy
application according to current settings.
|
protected void |
AbstractProofControl.emitInteractiveRuleApplication(Goal goal,
RuleApp app) |
void |
InteractionListener.runRule(Goal goal,
RuleApp app) |
Constructor and Description |
---|
GUIOneStepChildTreeNode(GUIProofTreeModel tree,
GUIAbstractTreeNode parent,
RuleApp app) |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
UseInformationFlowContractMacro.PropExpansionStrategy.computeCost(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal) |
void |
UseInformationFlowContractMacro.PropExpansionStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal,
RuleAppCostCollector collector) |
boolean |
UseInformationFlowContractMacro.PropExpansionStrategy.isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
protected boolean |
SelfcompositionStateExpansionMacro.ruleApplicationInContextAllowed(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal) |
protected boolean |
UseInformationFlowContractMacro.ruleApplicationInContextAllowed(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal)
Checks whether the application of the passed rule is ok in the given
context.
|
Modifier and Type | Method and Description |
---|---|
protected void |
InfFlowContractAppTacletExecutor.addToAntec(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services) |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
FilterStrategy.computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal) |
RuleAppCost |
PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy.computeCost(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal) |
protected RuleAppCost |
PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
void |
FilterStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal,
RuleAppCostCollector collector) |
boolean |
FilterStrategy.isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
boolean |
PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy.isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
protected boolean |
AbstractPropositionalExpansionMacro.ruleApplicationInContextAllowed(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal)
Checks whether the application of the passed rule is ok in the given
context.
|
Modifier and Type | Method and Description |
---|---|
RuleApp |
Node.getAppliedRuleApp() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<RuleApp> |
Goal.appliedRuleApps()
returns set of rules applied at this branch
|
java.util.List<RuleApp> |
Goal.getAllBuiltInRuleApps() |
Modifier and Type | Method and Description |
---|---|
void |
Goal.addAppliedRuleApp(RuleApp app)
puts a RuleApp to the list of the applied rule apps at this goal
and stores it in the node of the goal
|
ImmutableList<Goal> |
Goal.apply(RuleApp ruleApp) |
static SourceElement |
NodeInfo.computeActiveStatement(RuleApp ruleApp)
Computes the active statement in the given
RuleApp . |
static SourceElement |
NodeInfo.computeFirstStatement(RuleApp ruleApp)
Computes the first statement in the given
RuleApp . |
static boolean |
NodeInfo.isSymbolicExecutionRuleApplied(RuleApp app)
Checks if the given
RuleApp performs symbolic execution. |
void |
NewRuleListener.ruleAdded(RuleApp rule,
PosInOccurrence pos)
Called when a new RuleApp is added
|
void |
NullNewRuleListener.ruleAdded(RuleApp rule,
PosInOccurrence pos) |
void |
Node.setAppliedRuleApp(RuleApp ruleApp) |
Modifier and Type | Method and Description |
---|---|
void |
NewRuleListener.rulesAdded(ImmutableList<? extends RuleApp> rule,
PosInOccurrence pos)
Called when a collection of new RuleApps is added
|
void |
NullNewRuleListener.rulesAdded(ImmutableList<? extends RuleApp> rule,
PosInOccurrence pos) |
Modifier and Type | Method and Description |
---|---|
RuleApp |
DelayedCut.getFirstAppliedRuleApp() |
Constructor and Description |
---|
DelayedCut(Proof proof,
Node node,
Term formula,
ImmutableList<Node> subtrees,
int sideOfDecisionPredicate,
RuleApp firstAppliedRuleApp) |
Modifier and Type | Method and Description |
---|---|
boolean |
Profile.isSpecificationInvolvedInRuleApp(RuleApp app) |
boolean |
JavaProfile.isSpecificationInvolvedInRuleApp(RuleApp app) |
void |
InitConfig.registerRuleIntroducedAtNode(RuleApp r,
Node node,
boolean isAxiom) |
Modifier and Type | Method and Description |
---|---|
RuleApp |
RuleJustificationByAddRules.motherTaclet() |
Modifier and Type | Method and Description |
---|---|
void |
ComplexRuleJustificationBySpec.add(RuleApp ruleApp,
RuleJustificationBySpec just) |
RuleJustification |
ProofCorrectnessMgt.getJustification(RuleApp r) |
RuleJustification |
RuleJustificationInfo.getJustification(RuleApp r,
TermServices services) |
RuleJustification |
ComplexRuleJustification.getSpecificJustification(RuleApp app,
TermServices services) |
RuleJustification |
ComplexRuleJustificationBySpec.getSpecificJustification(RuleApp app,
TermServices services) |
void |
ProofCorrectnessMgt.ruleApplied(RuleApp r) |
void |
ProofCorrectnessMgt.ruleUnApplied(RuleApp r) |
Modifier and Type | Method and Description |
---|---|
RuleApp |
RuleAppInfo.getRuleApp() |
Modifier and Type | Method and Description |
---|---|
RuleAppInfo |
NodeChangeJournal.getRuleAppInfo(RuleApp p_ruleApp)
Create an RuleAppInfo object containing all changes stored
within this object; remove all listeners
|
Modifier and Type | Method and Description |
---|---|
RuleApp |
SingleRuleApplicationInfo.getAppliedRuleApp() |
Modifier and Type | Interface and Description |
---|---|
interface |
IBuiltInRuleApp |
Modifier and Type | Class and Description |
---|---|
class |
AbstractAuxiliaryContractBuiltInRuleApp
Application for
AbstractAuxiliaryContractRule . |
class |
AbstractBlockContractBuiltInRuleApp
Application of
AbstractBlockContractRule . |
class |
AbstractBuiltInRuleApp |
class |
AbstractContractRuleApp |
class |
AbstractLoopContractBuiltInRuleApp
Application of
AbstractLoopContractRule . |
class |
BlockContractExternalBuiltInRuleApp
Application of
BlockContractExternalRule . |
class |
BlockContractInternalBuiltInRuleApp
Application of
BlockContractInternalRule . |
class |
ContractRuleApp
Represents an application of a contract rule.
|
class |
DefaultBuiltInRuleApp
this class represents an application of a built in rule
application
|
class |
LoopApplyHeadBuiltInRuleApp
Rule application for
LoopApplyHeadRule . |
class |
LoopContractExternalBuiltInRuleApp
Application of
LoopContractExternalRule . |
class |
LoopContractInternalBuiltInRuleApp
Application of
LoopContractInternalRule . |
class |
LoopInvariantBuiltInRuleApp
The built in rule app for the loop invariant rule.
|
class |
NoPosTacletApp
A no position taclet application has no position information yet.
|
class |
OneStepSimplifierRuleApp |
class |
PosTacletApp
A position taclet application object, contains already the information to
which term/formula of the sequent the taclet is attached.
|
class |
TacletApp
A TacletApp object contains information required for a concrete application.
|
class |
UseDependencyContractApp |
Modifier and Type | Field and Description |
---|---|
protected RuleApp |
SyntacticalReplaceVisitor.ruleApp |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
BlockContractExternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
Taclet.apply(Goal goal,
Services services,
RuleApp tacletApp)
applies the given rule application to the specified goal
|
ImmutableList<Goal> |
QueryExpand.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
Rule.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
ImmutableList<Goal> |
OneStepSimplifier.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
WhileInvariantRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
BlockContractInternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopContractExternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopContractInternalRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
UseDependencyContractRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopApplyHeadRule.apply(Goal goal,
Services services,
RuleApp application) |
ImmutableList<Goal> |
UseOperationContractRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
LoopScopeInvariantRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
AbstractLoopInvariantRule.LoopInvariantInformation |
AbstractLoopInvariantRule.doPreparations(Goal goal,
Services services,
RuleApp ruleApp)
Constructs the data needed for the currently implemented loop invariants;
also prepares the new set of goals, that is splitting the current goal is
no longer required after calling this method.
|
Constructor and Description |
---|
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 |
---|---|
ImmutableList<Goal> |
RuleExecutor.apply(Goal goal,
Services services,
RuleApp ruleApp)
applies the given rule application to the specified goal
|
Modifier and Type | Method and Description |
---|---|
protected void |
TacletExecutor.addToAntec(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
adds SequentFormula to antecedent depending on
position information (if none is handed over it is added at the
head of the antecedent).
|
protected void |
TacletExecutor.addToSucc(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
adds SequentFormula to succedent depending on
position information (if none is handed over it is added at the
head of the succedent).
|
ImmutableList<Goal> |
NoFindTacletExecutor.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
abstract ImmutableList<Goal> |
TacletExecutor.apply(Goal goal,
Services services,
RuleApp tacletApp)
applies the given rule application to the specified goal
|
ImmutableList<Goal> |
FindTacletExecutor.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
protected void |
RewriteTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
adds the sequent of the add part of the Taclet to the goal sequent
|
protected void |
SuccTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected abstract void |
FindTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected void |
AntecTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected void |
NoFindTacletExecutor.applyAdd(TermLabelState termLabelState,
Sequent add,
SequentChangeInfo currentSequent,
Services services,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp)
adds the sequent of the add part of the Taclet to the goal sequent
|
protected void |
RewriteTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
SuccTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected abstract void |
FindTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
AntecTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected ImmutableList<SequentFormula> |
TacletExecutor.instantiateSemisequent(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
instantiates the given semisequent with the instantiations found in
Matchconditions
|
protected void |
TacletExecutor.replaceAtPos(Semisequent semi,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
MatchConditions matchCond,
Taclet.TacletLabelHint labelHint,
Goal goal,
RuleApp ruleApp,
Services services)
replaces the constrained formula at the given position with the first
formula in the given semisequent and adds possible other formulas of the
semisequent starting at the position
|
protected Term |
TacletExecutor.syntacticalReplace(Term term,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
MatchConditions mc,
Goal goal,
RuleApp ruleApp,
Services services)
a new term is created by replacing variables of term whose replacement is
found in the given SVInstantiations
|
Modifier and Type | Method and Description |
---|---|
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 |
CloseAfterMergeRuleBuiltInRuleApp
Rule application class for close-after-merge rule applications.
|
class |
MergeRuleBuiltInRuleApp
Rule application class for merge rule applications.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
MergeRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
ImmutableList<Goal> |
CloseAfterMerge.apply(Goal goal,
Services services,
RuleApp ruleApp) |
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 |
---|---|
class |
RuleAppSMT
The rule application that is used when a goal is closed by means of an external solver.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
RuleAppSMT.SMTRule.apply(Goal goal,
Services services,
RuleApp ruleApp) |
Modifier and Type | Method and Description |
---|---|
abstract RuleApp |
RuleAppContainer.completeRuleApp(Goal p_goal)
Create a
RuleApp that is suitable to be applied
or null . |
RuleApp |
BuiltInRuleAppContainer.completeRuleApp(Goal goal) |
protected RuleApp |
RuleAppContainer.getRuleApp() |
RuleApp |
FocussedBreakpointRuleApplicationManager.next() |
RuleApp |
FocussedRuleApplicationManager.next() |
RuleApp |
AutomatedRuleApplicationManager.next() |
RuleApp |
QueueRuleApplicationManager.next() |
RuleApp |
FocussedBreakpointRuleApplicationManager.peekNext() |
RuleApp |
FocussedRuleApplicationManager.peekNext() |
RuleApp |
AutomatedRuleApplicationManager.peekNext() |
RuleApp |
QueueRuleApplicationManager.peekNext() |
Modifier and Type | Method and Description |
---|---|
void |
RuleAppCostCollector.collect(RuleApp app,
RuleAppCost cost) |
RuleAppCost |
SimpleFilteredStrategy.computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal)
Evaluate the cost of a
RuleApp . |
RuleAppCost |
FIFOStrategy.computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal)
Evaluate the cost of a
RuleApp . |
RuleAppCost |
IsInRangeProvable.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
JavaCardDLStrategy.computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal)
Evaluate the cost of a
RuleApp . |
long |
RuleAppFeature.cost(RuleApp app,
Goal goal)
Evaluate the cost of a RuleApp.
|
static RuleAppContainer |
RuleAppContainer.createAppContainer(RuleApp p_app,
PosInOccurrence p_pio,
Goal p_goal)
Create container for a RuleApp.
|
protected abstract RuleAppCost |
AbstractFeatureStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
protected RuleAppCost |
JavaCardDLStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
void |
SimpleFilteredStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal,
RuleAppCostCollector collector) |
void |
Strategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal,
RuleAppCostCollector collector)
Instantiate an incomplete
RuleApp . |
void |
FIFOStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal,
RuleAppCostCollector collector) |
void |
AbstractFeatureStrategy.instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal,
RuleAppCostCollector collector) |
boolean |
SimpleFilteredStrategy.isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal)
Re-Evaluate a
RuleApp . |
boolean |
Strategy.isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal)
Re-Evaluate a
RuleApp . |
boolean |
FIFOStrategy.isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal)
Re-Evaluate a
RuleApp . |
boolean |
JavaCardDLStrategy.isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal)
Re-Evaluate a
RuleApp . |
protected boolean |
FocussedRuleApplicationManager.isRuleApplicationForFocussedFormula(RuleApp rule,
PosInOccurrence pos) |
void |
FocussedBreakpointRuleApplicationManager.ruleAdded(RuleApp rule,
PosInOccurrence pos) |
void |
FocussedRuleApplicationManager.ruleAdded(RuleApp rule,
PosInOccurrence pos) |
void |
QueueRuleApplicationManager.ruleAdded(RuleApp rule,
PosInOccurrence pos)
Implementation of the method from
NewRuleListener . |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<RuleAppContainer> |
RuleAppContainer.createAppContainers(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos,
Goal goal)
Create containers for RuleApps.
|
void |
FocussedBreakpointRuleApplicationManager.rulesAdded(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos) |
void |
FocussedRuleApplicationManager.rulesAdded(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos) |
void |
QueueRuleApplicationManager.rulesAdded(ImmutableList<? extends RuleApp> rules,
PosInOccurrence pos)
Implementation of the method from
NewRuleListener . |
Constructor and Description |
---|
RuleAppContainer(RuleApp p_app,
RuleAppCost p_cost) |
TacletAppContainer(RuleApp p_app,
RuleAppCost p_cost,
long p_age) |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
CountBranchFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Compute the cost of a RuleApp.
|
RuleAppCost |
AgeFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
BinaryFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ConstFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
FocusIsSubFormulaOfInfFlowContractAppFeature.computeCost(RuleApp ruleApp,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
LetFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
IfThenElseMalusFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
FindDepthFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ComprehendedSumFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
PrintFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
SimplifyReplaceKnownCandidateFeature.computeCost(RuleApp ruleApp,
PosInOccurrence pos,
Goal goal)
Compute the cost of a RuleApp.
|
RuleAppCost |
Feature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Evaluate the cost of a
RuleApp . |
RuleAppCost |
ShannonFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
RuleSetDispatchFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ContainsTermFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
SumFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
FindRightishFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
DeleteMergePointRuleFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ConditionalFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
MergeRuleFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
AbstractBetaFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Compute the cost of a RuleApp.
|
RuleAppCost |
InfFlowContractAppFeature.computeCost(RuleApp ruleApp,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
QueryExpandCost.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
ApplyTFFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
SortComparisonFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
FocusInAntecFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
DependencyContractFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected abstract boolean |
BinaryFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal)
Compute whether the result of the feature is zero (
true )
or infinity (false ) |
protected boolean |
ThrownExceptionFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
ImplicitCastNecessary.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
DirectlyBelowFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
SeqContainsExecutableCodeFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
boolean |
FormulaAddedByRuleFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
BinaryTacletAppFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
NotInScopeOfModalityFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
boolean |
AllowedCutPositionFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
boolean |
NotBelowBinderFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
boolean |
NotBelowQuantifierFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected int |
QueryExpandCost.queryExpandAlreadyAppliedAtPos(RuleApp app,
PosInOccurrence pos,
Goal goal)
The method checks if the same rule has been applied earlier on this branch
at the same position in the sequent.
|
protected boolean |
InfFlowContractAppFeature.sameApplication(RuleApp ruleCmp,
TacletApp newApp,
PosInOccurrence newPio)
Check whether the old rule application
ruleCmp is a duplicate of the new application
newApp at position
newPio .newPio can be
null |
protected boolean |
AbstractNonDuplicateAppFeature.sameApplication(RuleApp ruleCmp,
TacletApp newApp,
PosInOccurrence newPio)
Check whether the old rule application
ruleCmp is a
duplicate of the new application newApp at position
newPio .newPio can be null |
Modifier and Type | Method and Description |
---|---|
protected boolean |
NonDuplicateAppFeature.containsRuleApp(ImmutableList<RuleApp> list,
TacletApp rapp,
PosInOccurrence pio) |
Modifier and Type | Method and Description |
---|---|
RuleApp |
BackTrackingManager.getResultingapp() |
RuleApp |
CPBranch.getRuleAppForBranch() |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
ForEachCP.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
OneOfCP.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
SVInstantiationCP.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<CPBranch> |
ChoicePoint.getBranches(RuleApp oldApp)
Obtain the branches that can be taken at this point.
|
void |
BackTrackingManager.setup(RuleApp initialApp)
Method that has to be called before a sequence of evaluation runs of a
feature term.
|
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
InstantiationCostScalerFeature.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal) |
RuleAppCost |
InstantiationCost.computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Compute the cost of a RuleApp.
|
protected boolean |
SplittableQuantifiedFormulaFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
HeuristicInstantiation.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Constructor and Description |
---|
ConstraintAwareSyntacticalReplaceVisitor(TermLabelState termLabelState,
Services services,
Constraint metavariableInst,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Taclet.TacletLabelHint labelHint,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
protected boolean |
ContainsLabelNameFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected boolean |
ContainsLabelFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
java.util.Iterator<Term> |
HeapGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
TriggeredInstantiations.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
MultiplesModEquationsGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
TermGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
AllowedCutPositionsGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
SequentFormulasGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
RootsGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
java.util.Iterator<Term> |
SuperTermGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected Term |
SubtermGenerator.getTermInst(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
Term |
TermBuffer.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
AssumptionProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
ProjectionToTerm.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
TermConstructionProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
SVInstantiationProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
CoeffGcdProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
SubtermProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
TriggerVariableInstantiationProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
AbstractDividePolynomialsProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
ReduceMonomialsProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
FocusProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Term |
FocusFormulaProjection.toTerm(RuleApp app,
PosInOccurrence pos,
Goal goal) |
Modifier and Type | Method and Description |
---|---|
RuleApp |
ExecutionNodeReader.AbstractKeYlessExecutionElement.getAppliedRuleApp()
Returns the applied
RuleApp . |
Modifier and Type | Method and Description |
---|---|
protected Node |
SymbolicExecutionTreeBuilder.findMethodCallNode(Node currentNode,
RuleApp ruleApp)
|
protected java.util.Map<Node,ImmutableList<Node>> |
SymbolicExecutionTreeBuilder.getMethodCallStack(RuleApp ruleApp)
Returns the method call stack.
|
protected java.util.Set<Node> |
SymbolicExecutionTreeBuilder.getMethodReturnsToIgnore(RuleApp ruleApp)
Returns the method
Node s of method calls for
which its return should be ignored. |
protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> |
SymbolicExecutionTreeBuilder.updateAfterBlockMap(Node node,
RuleApp ruleApp)
Updates the after block maps when a symbolic execution tree node is detected.
|
Modifier and Type | Method and Description |
---|---|
RuleApp |
IExecutionElement.getAppliedRuleApp()
Returns the applied
RuleApp . |
Modifier and Type | Method and Description |
---|---|
RuleApp |
AbstractExecutionElement.getAppliedRuleApp()
Returns the applied
RuleApp . |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
ModalitySideProofRule.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
ImmutableList<Goal> |
QuerySideProofRule.apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
CutHeapObjectsFeature.filter(RuleApp app,
PosInOccurrence pos,
Goal goal)
Compute whether the result of the feature is zero (
true )
or infinity (false ) |
java.util.Iterator<Term> |
CutHeapObjectsTermGenerator.generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
protected void |
ExecutedSymbolicExecutionTreeNodesStopCondition.handleNodeLimitExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is exceeded.
|
protected void |
ExecutedSymbolicExecutionTreeNodesStopCondition.handleNodeLimitNotExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is not exceeded.
|
protected void |
SymbolicExecutionBreakpointStopCondition.handleNodeLimitNotExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is not exceeded.
|
protected boolean |
SymbolicExecutionBreakpointStopCondition.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Checks if a breakpoint is hit.
|
protected boolean |
BreakpointStopCondition.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Checks if a breakpoint is hit.
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
AbstractConditionalBreakpoint.conditionMet(RuleApp ruleApp,
Proof proof,
Node node)
Checks if the condition, that was given by the user, evaluates to true with the current of the proof
|
protected boolean |
KeYWatchpoint.conditionMet(RuleApp ruleApp,
Proof proof,
Node node) |
boolean |
AbstractHitCountBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
AbstractConditionalBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
SymbolicExecutionExceptionBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
ExceptionBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
FieldWatchpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
IBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
KeYWatchpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node) |
boolean |
MethodBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node) |
boolean |
LineBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node) |
protected void |
AbstractConditionalBreakpoint.refreshVarMaps(RuleApp ruleApp,
Node node)
Modifies toKeep and variableNamingMap to hold the correct parameters after execution of the given ruleApp on the given node
|
Modifier and Type | Method and Description |
---|---|
static Pair<java.lang.Integer,SourceElement> |
SymbolicExecutionUtil.computeSecondStatement(RuleApp ruleApp)
Computes the call stack size and the second statement
similar to
NodeInfo.computeActiveStatement(SourceElement) . |
static int |
SymbolicExecutionUtil.computeStackSize(RuleApp ruleApp)
|
static SymbolicExecutionTermLabel |
SymbolicExecutionUtil.getSymbolicExecutionLabel(RuleApp ruleApp)
Returns the contained
SymbolicExecutionTermLabel if available. |
static boolean |
SymbolicExecutionUtil.hasLoopBodyLabel(RuleApp ruleApp)
|
static boolean |
SymbolicExecutionUtil.hasLoopBodyTerminationLabel(RuleApp ruleApp)
|
static boolean |
SymbolicExecutionUtil.hasLoopCondition(Node node,
RuleApp ruleApp,
SourceElement statement)
Checks if the given
Node has a loop condition. |
static boolean |
SymbolicExecutionUtil.hasSymbolicExecutionLabel(RuleApp ruleApp)
|
static boolean |
SymbolicExecutionUtil.isBlockContractValidityBranch(RuleApp appliedRuleApp)
Checks if the modality at the applied rule represents the validity branch of an applied block contract.
|
static boolean |
SymbolicExecutionUtil.isBlockSpecificationElement(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as block/loop contract.
|
static boolean |
SymbolicExecutionUtil.isBranchStatement(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as branch statement.
|
static boolean |
SymbolicExecutionUtil.isCloseAfterJoin(RuleApp ruleApp)
Checks if the
CloseAfterMergeRuleBuiltInRuleApp is applied. |
static boolean |
SymbolicExecutionUtil.isExceptionalMethodReturnNode(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as exceptional method return.
|
static boolean |
SymbolicExecutionUtil.isInImplicitMethod(Node node,
RuleApp ruleApp)
Checks if the currently executed code is in an implicit method
(
IProgramMethod.isImplicit() is true ). |
static boolean |
SymbolicExecutionUtil.isJoin(RuleApp ruleApp)
Checks if the
MergeRuleBuiltInRuleApp is applied. |
static boolean |
SymbolicExecutionUtil.isLoopBodyTermination(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as loop body termination.
|
static boolean |
SymbolicExecutionUtil.isLoopInvariant(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as loop invariant.
|
static boolean |
SymbolicExecutionUtil.isLoopStatement(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as loop statement.
|
static boolean |
SymbolicExecutionUtil.isMethodCallNode(Node node,
RuleApp ruleApp,
SourceElement statement)
Checks if the given node should be represented as method call.
|
static boolean |
SymbolicExecutionUtil.isMethodCallNode(Node node,
RuleApp ruleApp,
SourceElement statement,
boolean allowImpliciteMethods)
Checks if the given node should be represented as method call.
|
static boolean |
SymbolicExecutionUtil.isMethodReturnNode(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as method return.
|
static boolean |
SymbolicExecutionUtil.isOperationContract(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as operation contract.
|
static boolean |
SymbolicExecutionUtil.isRuleAppToIgnore(RuleApp ruleApp)
Checks if the given
RuleApp should be ignored or
checked for possible symbolic execution tree node representation. |
static boolean |
SymbolicExecutionUtil.isStatementNode(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as statement.
|
static boolean |
SymbolicExecutionUtil.isSymbolicExecutionTreeNode(Node node,
RuleApp ruleApp)
|
static boolean |
SymbolicExecutionUtil.isTerminationNode(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as termination.
|
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
MiscTools.getRuleDisplayName(RuleApp ruleApp)
Returns the display name of the
RuleApp . |
static java.lang.String |
MiscTools.getRuleName(RuleApp ruleApp)
Returns the name of the
RuleApp . |
Modifier and Type | Method and Description |
---|---|
void |
InteractionRecorder.runRule(Goal goal,
RuleApp app) |
Constructor and Description |
---|
RuleInteraction(Node node,
RuleApp app) |
Copyright © 2003-2019 The KeY-Project.