de.uka.ilkd.key.rule

Class AbstractBlockContractBuiltInRuleApp

java.lang.Object

de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

de.uka.ilkd.key.rule.AbstractAuxiliaryContractBuiltInRuleApp

de.uka.ilkd.key.rule.AbstractBlockContractBuiltInRuleApp

All Implemented Interfaces:

IBuiltInRuleApp, RuleApp

Direct Known Subclasses:

BlockContractExternalBuiltInRuleApp, BlockContractInternalBuiltInRuleApp

public abstract class AbstractBlockContractBuiltInRuleApp
extends AbstractAuxiliaryContractBuiltInRuleApp

Application of AbstractBlockContractRule.

Author:

wacker, lanzinger

Field Summary

Fields

Modifier and Type	Field and Description
protected BlockContract	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
AbstractBlockContractBuiltInRuleApp(BuiltInRule rule, PosInOccurrence occurrence, ImmutableList<PosInOccurrence> ifInstantiations)

Method Summary

Modifier and Type	Method and Description
BlockContract	getContract()
AbstractBlockContractBuiltInRuleApp	tryToInstantiate(Goal goal, AbstractBlockContractRule rule)
void	update(JavaStatement statement, BlockContract 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 BlockContract contract

See Also:

getContract()

Constructor Detail

AbstractBlockContractBuiltInRuleApp

public AbstractBlockContractBuiltInRuleApp(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 BlockContract getContract()

Specified by:

getContract in class AbstractAuxiliaryContractBuiltInRuleApp

Returns:

the contract being applied.

tryToInstantiate

public AbstractBlockContractBuiltInRuleApp tryToInstantiate(Goal goal,
                                                            AbstractBlockContractRule rule)

Parameters:

goal - the current goal.

rule - the rule being applied.

Returns:

this.

update

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

Parameters:

statement - the new statement.

contract - the new contract.

heaps - the new heap context.