public class BlockContractBuiltInRuleApp extends AbstractBuiltInRuleApp
Modifier and Type | Field and Description |
---|---|
private StatementBlock |
block |
private ExecutionContext |
context |
private BlockContract |
contract |
private List<LocationVariable> |
heaps |
private IFProofObligationVars |
infFlowVars |
builtInRule, ifInsts, pio
Constructor and Description |
---|
BlockContractBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence) |
BlockContractBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations,
StatementBlock block,
BlockContract contract,
List<LocationVariable> heaps) |
Modifier and Type | Method and Description |
---|---|
boolean |
cannotComplete(Goal goal) |
boolean |
complete()
returns true if all variables are instantiated
|
StatementBlock |
getBlock() |
BlockContract |
getContract() |
ExecutionContext |
getExecutionContext() |
List<LocationVariable> |
getHeapContext() |
IFProofObligationVars |
getInformationFlowProofObligationVars() |
boolean |
isSufficientlyComplete()
returns true if tryToInstantiate may be able to complete the app
|
BlockContractBuiltInRuleApp |
replacePos(PosInOccurrence newOccurrence) |
BlockContractBuiltInRuleApp |
setIfInsts(ImmutableList<PosInOccurrence> ifInstantiations) |
BlockContractBuiltInRuleApp |
tryToInstantiate(Goal goal)
Tries to complete the rule application from the available information.
|
void |
update(IFProofObligationVars vars,
ExecutionContext context) |
void |
update(StatementBlock block,
BlockContract contract,
List<LocationVariable> heaps) |
execute, forceInstantiate, ifInsts, posInOccurrence, rule, setMutable, toString
private StatementBlock block
private BlockContract contract
private List<LocationVariable> heaps
private IFProofObligationVars infFlowVars
private ExecutionContext context
public BlockContractBuiltInRuleApp(BuiltInRule rule, PosInOccurrence occurrence)
public BlockContractBuiltInRuleApp(BuiltInRule rule, PosInOccurrence occurrence, ImmutableList<PosInOccurrence> ifInstantiations, StatementBlock block, BlockContract contract, List<LocationVariable> heaps)
public StatementBlock getBlock()
public BlockContract getContract()
public List<LocationVariable> getHeapContext()
getHeapContext
in interface IBuiltInRuleApp
getHeapContext
in class AbstractBuiltInRuleApp
public BlockContractBuiltInRuleApp replacePos(PosInOccurrence newOccurrence)
replacePos
in interface IBuiltInRuleApp
replacePos
in class AbstractBuiltInRuleApp
public BlockContractBuiltInRuleApp setIfInsts(ImmutableList<PosInOccurrence> ifInstantiations)
setIfInsts
in interface IBuiltInRuleApp
setIfInsts
in class AbstractBuiltInRuleApp
public boolean complete()
AbstractBuiltInRuleApp
complete
in interface RuleApp
complete
in class AbstractBuiltInRuleApp
public boolean isSufficientlyComplete()
IBuiltInRuleApp
isSufficientlyComplete
in interface IBuiltInRuleApp
isSufficientlyComplete
in class AbstractBuiltInRuleApp
public BlockContractBuiltInRuleApp 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 AbstractBuiltInRuleApp
public boolean cannotComplete(Goal goal)
public void update(StatementBlock block, BlockContract contract, List<LocationVariable> heaps)
public void update(IFProofObligationVars vars, ExecutionContext context)
public IFProofObligationVars getInformationFlowProofObligationVars()
public ExecutionContext getExecutionContext()