de.uka.ilkd.key.rule

Class LoopContractInternalBuiltInRuleApp

java.lang.Object

de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

de.uka.ilkd.key.rule.AbstractAuxiliaryContractBuiltInRuleApp

de.uka.ilkd.key.rule.AbstractLoopContractBuiltInRuleApp

de.uka.ilkd.key.rule.LoopContractInternalBuiltInRuleApp

All Implemented Interfaces:

IBuiltInRuleApp, RuleApp

public class LoopContractInternalBuiltInRuleApp
extends AbstractLoopContractBuiltInRuleApp

Application of LoopContractInternalRule.

Author:

lanzinger

Field Summary

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

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
LoopContractInternalBuiltInRuleApp(BuiltInRule rule, PosInOccurrence occurrence)
LoopContractInternalBuiltInRuleApp(BuiltInRule rule, PosInOccurrence occurrence, ImmutableList<PosInOccurrence> ifInstantiations, JavaStatement statement, LoopContract contract, java.util.List<LocationVariable> heaps)

Method Summary

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

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

getContract, tryToInstantiate, update

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, rule, setMutable, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

LoopContractInternalBuiltInRuleApp

public LoopContractInternalBuiltInRuleApp(BuiltInRule rule,
                                          PosInOccurrence occurrence)

Parameters:

rule - the rule being applied.

occurrence - the position at which the rule is applied.

LoopContractInternalBuiltInRuleApp

public LoopContractInternalBuiltInRuleApp(BuiltInRule rule,
                                          PosInOccurrence occurrence,
                                          ImmutableList<PosInOccurrence> ifInstantiations,
                                          JavaStatement statement,
                                          LoopContract contract,
                                          java.util.List<LocationVariable> heaps)

Parameters:

rule - the rule being applied.

occurrence - the position at which the rule is applied.

ifInstantiations - if instantiations.

statement - the statement which the applied contract belongs to.

contract - the contract being applied.

heaps - the heap context.

Method Detail

replacePos

public LoopContractInternalBuiltInRuleApp replacePos(PosInOccurrence newOccurrence)

Specified by:

replacePos in interface IBuiltInRuleApp

Specified by:

replacePos in class AbstractBuiltInRuleApp

setIfInsts

public LoopContractInternalBuiltInRuleApp setIfInsts(ImmutableList<PosInOccurrence> ifInstantiations)

Specified by:

setIfInsts in interface IBuiltInRuleApp

Specified by:

setIfInsts in class AbstractBuiltInRuleApp

tryToInstantiate

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