de.uka.ilkd.key.rule

Class UseDependencyContractApp

java.lang.Object

de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

de.uka.ilkd.key.rule.AbstractContractRuleApp

de.uka.ilkd.key.rule.UseDependencyContractApp

All Implemented Interfaces:

IBuiltInRuleApp, RuleApp

public class UseDependencyContractApp
extends AbstractContractRuleApp

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.List<LocationVariable>	heapContext
private PosInOccurrence	step

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

instantiation

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

builtInRule, ifInsts, pio

Constructor Summary

Constructors

Constructor and Description
UseDependencyContractApp(BuiltInRule builtInRule, PosInOccurrence pio)
UseDependencyContractApp(BuiltInRule builtInRule, PosInOccurrence pio, Contract instantiation, PosInOccurrence step)
UseDependencyContractApp(BuiltInRule rule, PosInOccurrence pio, ImmutableList<PosInOccurrence> ifInsts, Contract contract, PosInOccurrence step)

Method Summary

Modifier and Type	Method and Description
boolean	complete() returns true if all variables are instantiated
private UseDependencyContractApp	computeStep(Sequent seq, Services services)
java.util.List<LocationVariable>	getHeapContext()
IObserverFunction	getObserverFunction(Services services)
boolean	isSufficientlyComplete() returns true if tryToInstantiate may be able to complete the app
UseDependencyContractApp	replacePos(PosInOccurrence newPos)
UseDependencyContractRule	rule() returns the rule of this rule application
UseDependencyContractApp	setContract(Contract contract)
UseDependencyContractApp	setIfInsts(ImmutableList<PosInOccurrence> ifInsts)
UseDependencyContractApp	setStep(PosInOccurrence p_step)
PosInOccurrence	step(Sequent seq, TermServices services)
UseDependencyContractApp	tryToInstantiate(Goal goal) Tries to complete the rule application from the available information.
UseDependencyContractApp	tryToInstantiateContract(Services services)

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

check, getInstantiation

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

execute, forceInstantiate, ifInsts, posInOccurrence, setMutable, toString

Methods inherited from class java.lang.Object

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

Field Detail

step

private final PosInOccurrence step

heapContext

private java.util.List<LocationVariable> heapContext

Constructor Detail

UseDependencyContractApp

public UseDependencyContractApp(BuiltInRule builtInRule,
                                PosInOccurrence pio)

UseDependencyContractApp

public UseDependencyContractApp(BuiltInRule builtInRule,
                                PosInOccurrence pio,
                                Contract instantiation,
                                PosInOccurrence step)

UseDependencyContractApp

public UseDependencyContractApp(BuiltInRule rule,
                                PosInOccurrence pio,
                                ImmutableList<PosInOccurrence> ifInsts,
                                Contract contract,
                                PosInOccurrence step)

Method Detail

replacePos

public UseDependencyContractApp replacePos(PosInOccurrence newPos)

Specified by:

replacePos in interface IBuiltInRuleApp

Specified by:

replacePos in class AbstractBuiltInRuleApp

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:

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 AbstractContractRuleApp

Returns:

true if all variables are instantiated

computeStep

private UseDependencyContractApp computeStep(Sequent seq,
                                             Services services)

step

public PosInOccurrence step(Sequent seq,
                            TermServices services)

setStep

public UseDependencyContractApp setStep(PosInOccurrence p_step)

setContract

public UseDependencyContractApp setContract(Contract contract)

Specified by:

setContract in class AbstractContractRuleApp

rule

public UseDependencyContractRule rule()

Description copied from class: AbstractBuiltInRuleApp

returns the rule of this rule application

Specified by:

rule in interface IBuiltInRuleApp

Specified by:

rule in interface RuleApp

Overrides:

rule in class AbstractBuiltInRuleApp

tryToInstantiate

public UseDependencyContractApp 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 AbstractContractRuleApp

tryToInstantiateContract

public UseDependencyContractApp tryToInstantiateContract(Services services)

getHeapContext

public java.util.List<LocationVariable> getHeapContext()

Specified by:

getHeapContext in interface IBuiltInRuleApp

Overrides:

getHeapContext in class AbstractBuiltInRuleApp

getObserverFunction

public IObserverFunction getObserverFunction(Services services)

Specified by:

getObserverFunction in class AbstractContractRuleApp

setIfInsts

public UseDependencyContractApp setIfInsts(ImmutableList<PosInOccurrence> ifInsts)

Specified by:

setIfInsts in interface IBuiltInRuleApp

Specified by:

setIfInsts in class AbstractBuiltInRuleApp