public class LoopInvariantBuiltInRuleApp extends AbstractBuiltInRuleApp
Modifier and Type | Field and Description |
---|---|
private ExecutionContext |
executionContext |
private Term |
guard |
private java.util.List<LocationVariable> |
heapContext |
private IFProofObligationVars |
infFlowVars |
private While |
loop |
private TermServices |
services |
private LoopSpecification |
spec |
builtInRule, ifInsts, pio
Modifier | Constructor and Description |
---|---|
protected |
LoopInvariantBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
LoopSpecification inv,
java.util.List<LocationVariable> heapContext,
TermServices services) |
protected |
LoopInvariantBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
LoopSpecification inv,
TermServices services) |
|
LoopInvariantBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pos,
TermServices services) |
execute, forceInstantiate, ifInsts, posInOccurrence, rule, setMutable, toString
private final While loop
private LoopSpecification spec
private final java.util.List<LocationVariable> heapContext
private IFProofObligationVars infFlowVars
private ExecutionContext executionContext
private Term guard
private final TermServices services
public LoopInvariantBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pos, TermServices services)
protected LoopInvariantBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pio, ImmutableList<PosInOccurrence> ifInsts, LoopSpecification inv, java.util.List<LocationVariable> heapContext, TermServices services)
protected LoopInvariantBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pio, LoopSpecification inv, TermServices services)
private LoopSpecification instantiateIndexValues(LoopSpecification rawInv, TermServices services)
\index
keyword from JML.
The values function symbol is a placeholder which stems from translating the \values
keyword from JML.
Both are used to refer to a runtime-generated variable.
If the loop guard has the form i < x
, index is instantiated with i
,
if the second statement in the loop body has the form v = xxx
,
where v
is a ghost variable of type sequence, values is instantiated with v
,
otherwise rawInv
is returned.services
- TODOpublic boolean complete()
AbstractBuiltInRuleApp
complete
in interface RuleApp
complete
in class AbstractBuiltInRuleApp
public LoopSpecification getSpec()
public While getLoopStatement()
public boolean invariantAvailable()
public boolean isSufficientlyComplete()
IBuiltInRuleApp
isSufficientlyComplete
in interface IBuiltInRuleApp
isSufficientlyComplete
in class AbstractBuiltInRuleApp
public Term programTerm()
public LoopInvariantBuiltInRuleApp replacePos(PosInOccurrence newPos)
replacePos
in interface IBuiltInRuleApp
replacePos
in class AbstractBuiltInRuleApp
public LoopSpecification retrieveLoopInvariantFromSpecification(Services services)
public LoopInvariantBuiltInRuleApp setIfInsts(ImmutableList<PosInOccurrence> ifInsts)
setIfInsts
in interface IBuiltInRuleApp
setIfInsts
in class AbstractBuiltInRuleApp
public LoopInvariantBuiltInRuleApp setLoopInvariant(LoopSpecification inv)
public void setInformationFlowProofObligationVars(IFProofObligationVars vars)
public void setGuard(Term guard)
public void setExecutionContext(ExecutionContext context)
public LoopInvariantBuiltInRuleApp 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 variantAvailable()
public boolean variantRequired()
public java.util.List<LocationVariable> getHeapContext()
getHeapContext
in interface IBuiltInRuleApp
getHeapContext
in class AbstractBuiltInRuleApp
public IFProofObligationVars getInformationFlowProofObligationVars()
public Term getGuard()
public ExecutionContext getExecutionContext()