public class LoopInvariantBuiltInRuleApp extends AbstractBuiltInRuleApp
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
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)
public 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()
Copyright © 2003-2019 The KeY-Project.