public class UseDependencyContractApp extends AbstractContractRuleApp
Modifier and Type | Field and Description |
---|---|
private java.util.List<LocationVariable> |
heapContext |
private PosInOccurrence |
step |
instantiation
builtInRule, ifInsts, pio
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) |
check, getInstantiation
execute, forceInstantiate, ifInsts, posInOccurrence, setMutable, toString
private final PosInOccurrence step
private java.util.List<LocationVariable> heapContext
public UseDependencyContractApp(BuiltInRule builtInRule, PosInOccurrence pio)
public UseDependencyContractApp(BuiltInRule builtInRule, PosInOccurrence pio, Contract instantiation, PosInOccurrence step)
public UseDependencyContractApp(BuiltInRule rule, PosInOccurrence pio, ImmutableList<PosInOccurrence> ifInsts, Contract contract, PosInOccurrence step)
public UseDependencyContractApp replacePos(PosInOccurrence newPos)
replacePos
in interface IBuiltInRuleApp
replacePos
in class AbstractBuiltInRuleApp
public boolean isSufficientlyComplete()
IBuiltInRuleApp
isSufficientlyComplete
in interface IBuiltInRuleApp
isSufficientlyComplete
in class AbstractBuiltInRuleApp
public boolean complete()
AbstractBuiltInRuleApp
complete
in interface RuleApp
complete
in class AbstractContractRuleApp
private UseDependencyContractApp computeStep(Sequent seq, Services services)
public PosInOccurrence step(Sequent seq, TermServices services)
public UseDependencyContractApp setStep(PosInOccurrence p_step)
public UseDependencyContractApp setContract(Contract contract)
setContract
in class AbstractContractRuleApp
public UseDependencyContractRule rule()
AbstractBuiltInRuleApp
rule
in interface IBuiltInRuleApp
rule
in interface RuleApp
rule
in class AbstractBuiltInRuleApp
public UseDependencyContractApp tryToInstantiate(Goal goal)
IBuiltInRuleApp
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
.tryToInstantiate
in interface IBuiltInRuleApp
tryToInstantiate
in class AbstractContractRuleApp
public UseDependencyContractApp tryToInstantiateContract(Services services)
public java.util.List<LocationVariable> getHeapContext()
getHeapContext
in interface IBuiltInRuleApp
getHeapContext
in class AbstractBuiltInRuleApp
public IObserverFunction getObserverFunction(Services services)
getObserverFunction
in class AbstractContractRuleApp
public UseDependencyContractApp setIfInsts(ImmutableList<PosInOccurrence> ifInsts)
setIfInsts
in interface IBuiltInRuleApp
setIfInsts
in class AbstractBuiltInRuleApp