de.uka.ilkd.key.rule

Class LoopInvariantBuiltInRuleApp

java.lang.Object

de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

de.uka.ilkd.key.rule.LoopInvariantBuiltInRuleApp

All Implemented Interfaces:

IBuiltInRuleApp, RuleApp

public class LoopInvariantBuiltInRuleApp
extends AbstractBuiltInRuleApp

The built in rule app for the loop invariant rule.

Field Summary

Fields

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

Fields inherited from class de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

builtInRule, ifInsts, pio

Constructor Summary

Constructors

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)

Method Summary

Modifier and Type	Method and Description
boolean	complete() returns true if all variables are instantiated
ExecutionContext	getExecutionContext()
Term	getGuard()
java.util.List<LocationVariable>	getHeapContext()
IFProofObligationVars	getInformationFlowProofObligationVars()
While	getLoopStatement()
LoopSpecification	getSpec()
private LoopSpecification	instantiateIndexValues(LoopSpecification rawInv, TermServices services) Replaces the function symbols "index" and "values" by actual program entities.
boolean	invariantAvailable()
boolean	isSufficientlyComplete() returns true if tryToInstantiate may be able to complete the app
Term	programTerm()
LoopInvariantBuiltInRuleApp	replacePos(PosInOccurrence newPos)
LoopSpecification	retrieveLoopInvariantFromSpecification(Services services)
void	setExecutionContext(ExecutionContext context)
void	setGuard(Term guard)
LoopInvariantBuiltInRuleApp	setIfInsts(ImmutableList<PosInOccurrence> ifInsts)
void	setInformationFlowProofObligationVars(IFProofObligationVars vars)
LoopInvariantBuiltInRuleApp	setLoopInvariant(LoopSpecification inv)
LoopInvariantBuiltInRuleApp	tryToInstantiate(Goal goal) Tries to complete the rule application from the available information.
boolean	variantAvailable()
boolean	variantRequired()

Methods inherited from class de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

execute, forceInstantiate, ifInsts, posInOccurrence, rule, setMutable, toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

loop

private final While loop

spec

private LoopSpecification spec

heapContext

private final java.util.List<LocationVariable> heapContext

infFlowVars

private IFProofObligationVars infFlowVars

executionContext

private ExecutionContext executionContext

guard

private Term guard

services

private final TermServices services

Constructor Detail

LoopInvariantBuiltInRuleApp

public LoopInvariantBuiltInRuleApp(BuiltInRule rule,
                                   PosInOccurrence pos,
                                   TermServices services)

LoopInvariantBuiltInRuleApp

protected LoopInvariantBuiltInRuleApp(BuiltInRule rule,
                                      PosInOccurrence pio,
                                      ImmutableList<PosInOccurrence> ifInsts,
                                      LoopSpecification inv,
                                      java.util.List<LocationVariable> heapContext,
                                      TermServices services)

LoopInvariantBuiltInRuleApp

protected LoopInvariantBuiltInRuleApp(BuiltInRule rule,
                                      PosInOccurrence pio,
                                      LoopSpecification inv,
                                      TermServices services)

Method Detail

instantiateIndexValues

private LoopSpecification instantiateIndexValues(LoopSpecification rawInv,
                                                 TermServices services)

Replaces the function symbols "index" and "values" by actual program entities. The index function symbol is a placeholder which stems from translating the \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.

Parameters:

services - TODO

complete

public boolean complete()

Description copied from class: AbstractBuiltInRuleApp

returns true if all variables are instantiated

Specified by:

complete in interface RuleApp

Overrides:

complete in class AbstractBuiltInRuleApp

Returns:

true if all variables are instantiated

getSpec

public LoopSpecification getSpec()

getLoopStatement

public While getLoopStatement()

invariantAvailable

public boolean invariantAvailable()

isSufficientlyComplete

public boolean isSufficientlyComplete()

Description copied from interface: IBuiltInRuleApp

returns true if tryToInstantiate may be able to complete the app

Specified by:

isSufficientlyComplete in interface IBuiltInRuleApp

Overrides:

isSufficientlyComplete in class AbstractBuiltInRuleApp

Returns:

programTerm

public Term programTerm()

replacePos

public LoopInvariantBuiltInRuleApp replacePos(PosInOccurrence newPos)

Specified by:

replacePos in interface IBuiltInRuleApp

Specified by:

replacePos in class AbstractBuiltInRuleApp

retrieveLoopInvariantFromSpecification

public LoopSpecification retrieveLoopInvariantFromSpecification(Services services)

setIfInsts

public LoopInvariantBuiltInRuleApp setIfInsts(ImmutableList<PosInOccurrence> ifInsts)

Specified by:

setIfInsts in interface IBuiltInRuleApp

Specified by:

setIfInsts in class AbstractBuiltInRuleApp

setLoopInvariant

public LoopInvariantBuiltInRuleApp setLoopInvariant(LoopSpecification inv)

setInformationFlowProofObligationVars

public void setInformationFlowProofObligationVars(IFProofObligationVars vars)

setGuard

public void setGuard(Term guard)

setExecutionContext

public void setExecutionContext(ExecutionContext context)

tryToInstantiate

public LoopInvariantBuiltInRuleApp tryToInstantiate(Goal goal)

Description copied from interface: IBuiltInRuleApp

Tries to complete the rule application from the available information. Attention: Do neither add GUI code to the rules nor use this method directly Instead ask the implementation of the 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.

Specified by:

tryToInstantiate in interface IBuiltInRuleApp

Specified by:

tryToInstantiate in class AbstractBuiltInRuleApp

variantAvailable

public boolean variantAvailable()

variantRequired

public boolean variantRequired()

getHeapContext

public java.util.List<LocationVariable> getHeapContext()

Specified by:

getHeapContext in interface IBuiltInRuleApp

Overrides:

getHeapContext in class AbstractBuiltInRuleApp

getInformationFlowProofObligationVars

public IFProofObligationVars getInformationFlowProofObligationVars()

getGuard

public Term getGuard()

getExecutionContext

public ExecutionContext getExecutionContext()