de.uka.ilkd.key.rule

Class AbstractLoopContractBuiltInRuleApp

java.lang.Object

de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

de.uka.ilkd.key.rule.AbstractAuxiliaryContractBuiltInRuleApp

de.uka.ilkd.key.rule.AbstractLoopContractBuiltInRuleApp

All Implemented Interfaces:

IBuiltInRuleApp, RuleApp

Direct Known Subclasses:

LoopContractExternalBuiltInRuleApp, LoopContractInternalBuiltInRuleApp

public abstract class AbstractLoopContractBuiltInRuleApp
extends AbstractAuxiliaryContractBuiltInRuleApp

Application of AbstractLoopContractRule.

Author:

lanzinger

Field Summary

Fields

Modifier and Type	Field and Description
protected LoopContract	contract

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

context, heaps, infFlowVars

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

builtInRule, ifInsts, pio

Constructor Summary

Constructors

Constructor and Description
AbstractLoopContractBuiltInRuleApp(BuiltInRule rule, PosInOccurrence occurrence, ImmutableList<PosInOccurrence> ifInstantiations)

Method Summary

Modifier and Type	Method and Description
LoopContract	getContract()
AbstractLoopContractBuiltInRuleApp	tryToInstantiate(Goal goal, AbstractLoopContractRule rule)
void	update(JavaStatement statement, LoopContract contract, java.util.List<LocationVariable> heaps)

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

cannotComplete, complete, getExecutionContext, getHeapContext, getInformationFlowProofObligationVars, getStatement, isSufficientlyComplete, setStatement, update

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

execute, forceInstantiate, ifInsts, posInOccurrence, replacePos, rule, setIfInsts, setMutable, toString, tryToInstantiate

Methods inherited from class java.lang.Object

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

Field Detail

contract

protected LoopContract contract

See Also:

getContract()

Constructor Detail

AbstractLoopContractBuiltInRuleApp

public AbstractLoopContractBuiltInRuleApp(BuiltInRule rule,
                                          PosInOccurrence occurrence,
                                          ImmutableList<PosInOccurrence> ifInstantiations)

Parameters:

rule - the rule being applied.

occurrence - the position at which the rule is applied.

ifInstantiations - if instantiations.

Method Detail

getContract

public LoopContract getContract()

Specified by:

getContract in class AbstractAuxiliaryContractBuiltInRuleApp

Returns:

the contract being applied.

tryToInstantiate

public AbstractLoopContractBuiltInRuleApp tryToInstantiate(Goal goal,
                                                           AbstractLoopContractRule rule)

Parameters:

goal - the current goal.

rule - the rule being applied.

Returns:

this.

update

public void update(JavaStatement statement,
                   LoopContract contract,
                   java.util.List<LocationVariable> heaps)

Parameters:

statement - the new statement.

contract - the new contract.

heaps - the new heap context.