de.uka.ilkd.key.rule

Class DefaultBuiltInRuleApp

java.lang.Object

de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

de.uka.ilkd.key.rule.DefaultBuiltInRuleApp

All Implemented Interfaces:

IBuiltInRuleApp, RuleApp

Direct Known Subclasses:

OneStepSimplifierRuleApp

public class DefaultBuiltInRuleApp
extends AbstractBuiltInRuleApp

this class represents an application of a built in rule application

Field Summary

Fields inherited from class de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

builtInRule, ifInsts, pio

Constructor Summary

Constructors

Constructor and Description
DefaultBuiltInRuleApp(BuiltInRule builtInRule, PosInOccurrence pio)
DefaultBuiltInRuleApp(BuiltInRule builtInRule, PosInOccurrence pio, ImmutableList<PosInOccurrence> ifInsts)

Method Summary

Modifier and Type	Method and Description
DefaultBuiltInRuleApp	replacePos(PosInOccurrence newPos)
DefaultBuiltInRuleApp	setIfInsts(ImmutableList<PosInOccurrence> ifInsts)
DefaultBuiltInRuleApp	tryToInstantiate(Goal goal) Tries to complete the rule application from the available information.

Methods inherited from class de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

complete, execute, forceInstantiate, getHeapContext, ifInsts, isSufficientlyComplete, posInOccurrence, rule, setMutable, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

DefaultBuiltInRuleApp

public DefaultBuiltInRuleApp(BuiltInRule builtInRule,
                             PosInOccurrence pio)

DefaultBuiltInRuleApp

public DefaultBuiltInRuleApp(BuiltInRule builtInRule,
                             PosInOccurrence pio,
                             ImmutableList<PosInOccurrence> ifInsts)

Method Detail

replacePos

public DefaultBuiltInRuleApp replacePos(PosInOccurrence newPos)

Specified by:

replacePos in interface IBuiltInRuleApp

Specified by:

replacePos in class AbstractBuiltInRuleApp

tryToInstantiate

public DefaultBuiltInRuleApp tryToInstantiate(Goal goal)

Description copied from interface: IBuiltInRuleApp

Tries to complete the rule application from the available information. Attention: Do neither add GUI code to the rules nor use this method directly Instead ask the implementation of the UserInterfaceControl to complete a built-in rule. Returns a complete app only if there is exactly one contract. If you want a complete app for combined contracts, use forceInstantiate instead. For an example implementation see e.g. UseOperationContractRule or UseDependencyContractRule.

Specified by:

tryToInstantiate in interface IBuiltInRuleApp

Specified by:

tryToInstantiate in class AbstractBuiltInRuleApp

setIfInsts

public DefaultBuiltInRuleApp setIfInsts(ImmutableList<PosInOccurrence> ifInsts)

Specified by:

setIfInsts in interface IBuiltInRuleApp

Specified by:

setIfInsts in class AbstractBuiltInRuleApp