de.uka.ilkd.key.rule

Class LoopContractExternalRule

java.lang.Object

de.uka.ilkd.key.rule.AbstractAuxiliaryContractRule

de.uka.ilkd.key.rule.AbstractLoopContractRule

de.uka.ilkd.key.rule.LoopContractExternalRule

All Implemented Interfaces:

BuiltInRule, Rule

public final class LoopContractExternalRule
extends AbstractLoopContractRule

Rule for the application of LoopContracts.

This splits the goal into two branches:

1. Precondition
2. Usage

The validity of all LoopContracts that were used in the application of this rule must be proven in a FunctionalLoopContractPO before the current proof is considered closed.

Author:

lanzinger

See Also:

LoopContractExternalBuiltInRuleApp

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.rule.AbstractLoopContractRule

AbstractLoopContractRule.Instantiator

Nested classes/interfaces inherited from class de.uka.ilkd.key.rule.AbstractAuxiliaryContractRule

AbstractAuxiliaryContractRule.Instantiation

Field Summary

Fields

Modifier and Type	Field and Description
static LoopContractExternalRule	INSTANCE The only instance of this class.
private Term	lastFocusTerm
private AbstractAuxiliaryContractRule.Instantiation	lastInstantiation
private static Name	NAME This rule's name.

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

FULL_PRECONDITION_TERM_HINT, NEW_POSTCONDITION_TERM_HINT

Constructor Summary

Constructors

Modifier	Constructor and Description
private	LoopContractExternalRule()

Method Summary

Modifier and Type	Method and Description
ImmutableList<Goal>	apply(Goal goal, Services services, RuleApp ruleApp) the rule is applied on the given goal using the information of rule application.
IBuiltInRuleApp	createApp(PosInOccurrence pos, TermServices services)
private static Term[]	createPreconditions(Term selfTerm, LoopContract contract, java.util.List<LocationVariable> heaps, ImmutableSet<ProgramVariable> localInVariables, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder, Services services)
private static Term[]	createUpdates(Term contextUpdate, java.util.List<LocationVariable> heaps, java.util.Map<LocationVariable,Function> anonymisationHeaps, AuxiliaryContract.Variables variables, java.util.Map<LocationVariable,Term> modifiesClauses, Services services)
private static Term[]	createUsageAssumptions(ImmutableSet<ProgramVariable> localOutVariables, java.util.Map<LocationVariable,Function> anonymisationHeaps, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)
Term	getLastFocusTerm()
AbstractAuxiliaryContractRule.Instantiation	getLastInstantiation()
boolean	isApplicable(Goal goal, PosInOccurrence occurrence) returns true iff a rule is applicable at the given position.
Name	name() the name of the rule
protected void	setLastFocusTerm(Term lastFocusTerm)
protected void	setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation lastInstantiation)

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

contractApplied, createAndRegisterAnonymisationVariables, filterAppliedContracts, getApplicableContracts, getApplicableContracts, instantiate

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

createLocalAnonUpdate, createLocalVariable, displayName, isApplicableOnSubTerms, occursNotAtTopLevelInSuccedent, register, toString

Methods inherited from class java.lang.Object

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

Field Detail

INSTANCE

public static final LoopContractExternalRule INSTANCE

The only instance of this class.

NAME

private static final Name NAME

This rule's name.

lastFocusTerm

private Term lastFocusTerm

See Also:

getLastFocusTerm()

lastInstantiation

private AbstractAuxiliaryContractRule.Instantiation lastInstantiation

See Also:

getLastInstantiation()

Constructor Detail

LoopContractExternalRule

private LoopContractExternalRule()

Method Detail

createUpdates

private static Term[] createUpdates(Term contextUpdate,
                                    java.util.List<LocationVariable> heaps,
                                    java.util.Map<LocationVariable,Function> anonymisationHeaps,
                                    AuxiliaryContract.Variables variables,
                                    java.util.Map<LocationVariable,Term> modifiesClauses,
                                    Services services)

Parameters:

contextUpdate - the context update.

heaps - the heaps.

anonymisationHeaps - the anonymization heaps.

variables - the variables.

modifiesClauses - the modifies clauses.

services - services.

Returns:

the updates for the usage branch.

createPreconditions

private static Term[] createPreconditions(Term selfTerm,
                                          LoopContract contract,
                                          java.util.List<LocationVariable> heaps,
                                          ImmutableSet<ProgramVariable> localInVariables,
                                          AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder,
                                          Services services)

Parameters:

selfTerm - the self term.

contract - the loop contract being applied.

heaps - the heaps.

localInVariables - all free program variables in the block.

conditionsAndClausesBuilder - a ConditionsAndClausesBuilder.

services - services.

Returns:

the preconditions.

createUsageAssumptions

private static Term[] createUsageAssumptions(ImmutableSet<ProgramVariable> localOutVariables,
                                             java.util.Map<LocationVariable,Function> anonymisationHeaps,
                                             AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)

Parameters:

localOutVariables - all free program variables modified by the block.

anonymisationHeaps - the anonymization heaps.

conditionsAndClausesBuilder - a ConditionsAndClausesBuilder.

Returns:

preconditions for the usage branch.

getLastFocusTerm

public Term getLastFocusTerm()

Specified by:

getLastFocusTerm in class AbstractAuxiliaryContractRule

Returns:

the term on which the rule was last applied.

setLastFocusTerm

protected void setLastFocusTerm(Term lastFocusTerm)

Specified by:

setLastFocusTerm in class AbstractAuxiliaryContractRule

Parameters:

lastFocusTerm - the last focus term.

See Also:

AbstractAuxiliaryContractRule.getLastFocusTerm()

getLastInstantiation

public AbstractAuxiliaryContractRule.Instantiation getLastInstantiation()

Specified by:

getLastInstantiation in class AbstractAuxiliaryContractRule

Returns:

the instantiation from the last time this rule was applied.

name

public Name name()

Description copied from interface: Rule

the name of the rule

setLastInstantiation

protected void setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation lastInstantiation)

Specified by:

setLastInstantiation in class AbstractAuxiliaryContractRule

Parameters:

lastInstantiation - the last instantiation.

See Also:

AbstractAuxiliaryContractRule.getLastInstantiation()

createApp

public IBuiltInRuleApp createApp(PosInOccurrence pos,
                                 TermServices services)

isApplicable

public boolean isApplicable(Goal goal,
                            PosInOccurrence occurrence)

Description copied from interface: BuiltInRule

returns true iff a rule is applicable at the given position. This does not necessarily mean that a rule application will change the goal (this decision is made due to performance reasons)

Specified by:

isApplicable in interface BuiltInRule

Overrides:

isApplicable in class AbstractLoopContractRule

apply

public ImmutableList<Goal> apply(Goal goal,
                                 Services services,
                                 RuleApp ruleApp)
                          throws RuleAbortException

Description copied from interface: Rule

the rule is applied on the given goal using the information of rule application.

Parameters:

goal - the Goal on which to apply ruleApp

services - the Services with the necessary information about the java programs

ruleApp - the rule application to be executed

Returns:

all open goals below \old(goal.node()), i.e. the goals resulting from the rule application

Throws:

RuleAbortException