public class UseDependencyContractApp extends AbstractContractRuleApp
Modifier and Type | Field and Description |
---|---|
private 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) |
Modifier and Type | Method and Description |
---|---|
boolean |
complete()
returns true if all variables are instantiated
|
private UseDependencyContractApp |
computeStep(Sequent seq,
Services services) |
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) |
check, getInstantiation
execute, forceInstantiate, ifInsts, posInOccurrence, setMutable, toString
private final PosInOccurrence step
private 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 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