de.uka.ilkd.key.rule

Class AbstractAuxiliaryContractBuiltInRuleApp

java.lang.Object

de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

de.uka.ilkd.key.rule.AbstractAuxiliaryContractBuiltInRuleApp

All Implemented Interfaces:

IBuiltInRuleApp, RuleApp

Direct Known Subclasses:

AbstractBlockContractBuiltInRuleApp, AbstractLoopContractBuiltInRuleApp

public abstract class AbstractAuxiliaryContractBuiltInRuleApp
extends AbstractBuiltInRuleApp

Application for AbstractAuxiliaryContractRule.

Author:

wacker, lanzinger

Field Summary

Fields

Modifier and Type	Field and Description
protected ExecutionContext	context
protected java.util.List<LocationVariable>	heaps
protected IFProofObligationVars	infFlowVars
private JavaStatement	statement

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

builtInRule, ifInsts, pio

Constructor Summary

Constructors

Constructor and Description
AbstractAuxiliaryContractBuiltInRuleApp(BuiltInRule rule, PosInOccurrence occurrence, ImmutableList<PosInOccurrence> ifInstantiations)

Method Summary

Modifier and Type	Method and Description
boolean	cannotComplete(Goal goal)
boolean	complete() returns true if all variables are instantiated
abstract AuxiliaryContract	getContract()
ExecutionContext	getExecutionContext()
java.util.List<LocationVariable>	getHeapContext()
IFProofObligationVars	getInformationFlowProofObligationVars()
JavaStatement	getStatement()
boolean	isSufficientlyComplete() returns true if tryToInstantiate may be able to complete the app
void	setStatement(JavaStatement s)
void	update(IFProofObligationVars vars, ExecutionContext context) Sets the proof obligation variables and execution context to new values.

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

execute, forceInstantiate, ifInsts, posInOccurrence, replacePos, rule, setIfInsts, setMutable, toString, tryToInstantiate

Methods inherited from class java.lang.Object

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

Field Detail

statement

private JavaStatement statement

See Also:

getStatement()

heaps

protected java.util.List<LocationVariable> heaps

See Also:

getHeapContext()

infFlowVars

protected IFProofObligationVars infFlowVars

See Also:

getInformationFlowProofObligationVars()

context

protected ExecutionContext context

See Also:

getExecutionContext()

Constructor Detail

AbstractAuxiliaryContractBuiltInRuleApp

public AbstractAuxiliaryContractBuiltInRuleApp(BuiltInRule rule,
                                               PosInOccurrence occurrence,
                                               ImmutableList<PosInOccurrence> ifInstantiations)

Parameters:

rule - the rule being applied.

occurrence - the position at which the rule is applied.

ifInstantiations - if instantiations.

Method Detail

setStatement

public void setStatement(JavaStatement s)

Parameters:

s - the statement (block or loop) which the applied contract belongs to.

getStatement

public JavaStatement getStatement()

Returns:

the statement (block or loop) which the applied contract belongs to.

getContract

public abstract AuxiliaryContract getContract()

Returns:

the contract being applied.

getInformationFlowProofObligationVars

public IFProofObligationVars getInformationFlowProofObligationVars()

Returns:

set of four sets of ProofObligationVars necessary for information flow proofs.

getExecutionContext

public ExecutionContext getExecutionContext()

Returns:

the execution context in which the block occurrs.

getHeapContext

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

Specified by:

getHeapContext in interface IBuiltInRuleApp

Overrides:

getHeapContext in class AbstractBuiltInRuleApp

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

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:

cannotComplete

public boolean cannotComplete(Goal goal)

Parameters:

goal - the current goal.

Returns:

true iff the rule application cannot be completed for the current goal.

update

public void update(IFProofObligationVars vars,
                   ExecutionContext context)

Sets the proof obligation variables and execution context to new values.

Parameters:

vars - new proof obligation variables.

context - new execution context.