de.uka.ilkd.key.strategy.feature

Class InfFlowContractAppFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.InfFlowContractAppFeature

All Implemented Interfaces:

Feature

public class InfFlowContractAppFeature
extends java.lang.Object
implements Feature

Field Summary

Fields

Modifier and Type	Field and Description
static Feature	INSTANCE

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	InfFlowContractAppFeature()

Method Summary

Modifier and Type	Method and Description
protected boolean	comparePio(TacletApp newApp, TacletApp oldApp, PosInOccurrence newPio, PosInOccurrence oldPio) Compare whether two PosInOccurrences are equal.
RuleAppCost	computeCost(RuleApp ruleApp, PosInOccurrence pos, Goal goal) Evaluate the cost of a RuleApp.
protected boolean	duplicateFindTaclet(TacletApp app, PosInOccurrence pos, Goal goal) Search for a duplicate of the application app by walking upwards in the proof tree.
private boolean	equalInterestingInsts(SVInstantiations inst0, SVInstantiations inst1)
private java.util.ArrayList<SequentFormula>	getRelatesTerms(Goal goal)
private boolean	isInfFlowProof(Proof proof)
protected boolean	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.
protected boolean	semiSequentContains(Semisequent semisequent, SequentFormula cfma) Check whether a semisequent contains a formula.
private boolean	subset(ImmutableMap<SchemaVariable,InstantiationEntry<?>> insts0, ImmutableMap<SchemaVariable,InstantiationEntry<?>> insts1)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

INSTANCE

public static final Feature INSTANCE

Constructor Detail

InfFlowContractAppFeature

protected InfFlowContractAppFeature()

Method Detail

comparePio

protected boolean comparePio(TacletApp newApp,
                             TacletApp oldApp,
                             PosInOccurrence newPio,
                             PosInOccurrence oldPio)

Compare whether two PosInOccurrences are equal. This can be done using equals or eqEquals (checking for same or equal formulas), which has to be decided by the subclasses

semiSequentContains

protected boolean semiSequentContains(Semisequent semisequent,
                                      SequentFormula cfma)

Check whether a semisequent contains a formula. Again, one can either search for the same or an equal formula

sameApplication

protected boolean 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

equalInterestingInsts

private boolean equalInterestingInsts(SVInstantiations inst0,
                                      SVInstantiations inst1)

subset

private boolean subset(ImmutableMap<SchemaVariable,InstantiationEntry<?>> insts0,
                       ImmutableMap<SchemaVariable,InstantiationEntry<?>> insts1)

duplicateFindTaclet

protected boolean duplicateFindTaclet(TacletApp app,
                                      PosInOccurrence pos,
                                      Goal goal)

Search for a duplicate of the application app by walking upwards in the proof tree. Here, we assume that pos is non-null, and as an optimisation we stop as soon as we have reached a point where the formula containing the focus no longer occurs in the sequent

computeCost

public RuleAppCost computeCost(RuleApp ruleApp,
                               PosInOccurrence pos,
                               Goal goal)

Description copied from interface: Feature

Evaluate the cost of a RuleApp.

Specified by:

computeCost in interface Feature

Parameters:

ruleApp - the RuleApp

pos - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

the cost of the rule application expressed as a RuleAppCost object. TopRuleAppCost.INSTANCE indicates that the rule shall not be applied at all (it is discarded by the strategy).

isInfFlowProof

private boolean isInfFlowProof(Proof proof)

getRelatesTerms

private java.util.ArrayList<SequentFormula> getRelatesTerms(Goal goal)