de.uka.ilkd.key.rule

Class LoopApplyHeadBuiltInRuleApp

java.lang.Object

de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

de.uka.ilkd.key.rule.LoopApplyHeadBuiltInRuleApp

All Implemented Interfaces:

IBuiltInRuleApp, RuleApp

public class LoopApplyHeadBuiltInRuleApp
extends AbstractBuiltInRuleApp

Rule application for LoopApplyHeadRule.

Author:

lanzinger

Field Summary

Fields

Modifier and Type	Field and Description
protected ImmutableSet<LoopContract>	contracts The loop contracts on which the rule is applied.
protected AbstractAuxiliaryContractRule.Instantiation	instantiation The instantiation.
private LoopApplyHeadRule	rule The rule being applied.

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

builtInRule, ifInsts, pio

Constructor Summary

Constructors

Constructor and Description
LoopApplyHeadBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pio)
LoopApplyHeadBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pio, ImmutableSet<LoopContract> contracts)

Method Summary

Modifier and Type	Method and Description
boolean	cannotComplete(Goal goal)
boolean	complete() returns true if all variables are instantiated
boolean	isSufficientlyComplete() returns true if tryToInstantiate may be able to complete the app
AbstractBuiltInRuleApp	replacePos(PosInOccurrence newPos)
IBuiltInRuleApp	setIfInsts(ImmutableList<PosInOccurrence> ifInsts)
AbstractBuiltInRuleApp	tryToInstantiate(Goal goal) Tries to complete the rule application from the available information.

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

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

Methods inherited from class java.lang.Object

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

Field Detail

rule

private LoopApplyHeadRule rule

The rule being applied.

contracts

protected ImmutableSet<LoopContract> contracts

The loop contracts on which the rule is applied.

instantiation

protected AbstractAuxiliaryContractRule.Instantiation instantiation

The instantiation.

Constructor Detail

LoopApplyHeadBuiltInRuleApp

public LoopApplyHeadBuiltInRuleApp(BuiltInRule rule,
                                   PosInOccurrence pio)

Parameters:

rule - the rule being applied.

pio - the position at which the rule is applied.

LoopApplyHeadBuiltInRuleApp

public LoopApplyHeadBuiltInRuleApp(BuiltInRule rule,
                                   PosInOccurrence pio,
                                   ImmutableSet<LoopContract> contracts)

Parameters:

rule - the rule being applied.

pio - the position at which the rule is applied.

contracts - the contracts on which the rule is applied.

Method Detail

complete

public boolean complete()

Description copied from class: AbstractBuiltInRuleApp

returns true if all variables are instantiated

Specified by:

complete in interface RuleApp

Overrides:

complete in class AbstractBuiltInRuleApp

Returns:

true if all variables are instantiated

cannotComplete

public boolean cannotComplete(Goal goal)

Parameters:

goal - the current goal.

Returns:

true iff the rule application cannot be completed for the current goal.

isSufficientlyComplete

public boolean isSufficientlyComplete()

Description copied from interface: IBuiltInRuleApp

returns true if tryToInstantiate may be able to complete the app

Specified by:

isSufficientlyComplete in interface IBuiltInRuleApp

Overrides:

isSufficientlyComplete in class AbstractBuiltInRuleApp

Returns:

replacePos

public AbstractBuiltInRuleApp replacePos(PosInOccurrence newPos)

Specified by:

replacePos in interface IBuiltInRuleApp

Specified by:

replacePos in class AbstractBuiltInRuleApp

setIfInsts

public IBuiltInRuleApp setIfInsts(ImmutableList<PosInOccurrence> ifInsts)

Specified by:

setIfInsts in interface IBuiltInRuleApp

Specified by:

setIfInsts in class AbstractBuiltInRuleApp

tryToInstantiate

public AbstractBuiltInRuleApp 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