de.uka.ilkd.key.rule

Class AbstractLoopContractRule

java.lang.Object

de.uka.ilkd.key.rule.AbstractAuxiliaryContractRule

de.uka.ilkd.key.rule.AbstractLoopContractRule

All Implemented Interfaces:

BuiltInRule, Rule

Direct Known Subclasses:

LoopContractExternalRule, LoopContractInternalRule

public abstract class AbstractLoopContractRule
extends AbstractAuxiliaryContractRule

Rule for the application of LoopContracts.

Author:

lanzinger

See Also:

AbstractLoopContractBuiltInRuleApp

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected static class	AbstractLoopContractRule.Instantiator A builder for Instantiations.

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

AbstractAuxiliaryContractRule.Instantiation

Field Summary

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

FULL_PRECONDITION_TERM_HINT, NEW_POSTCONDITION_TERM_HINT

Constructor Summary

Constructors

Constructor and Description
AbstractLoopContractRule()

Method Summary

Modifier and Type	Method and Description
protected static boolean	contractApplied(LoopContract contract, Goal goal)
protected java.util.Map<LocationVariable,Function>	createAndRegisterAnonymisationVariables(java.lang.Iterable<LocationVariable> variables, LoopContract contract, TermServices services)
protected static ImmutableSet<LoopContract>	filterAppliedContracts(ImmutableSet<LoopContract> collectedContracts, Goal goal)
static ImmutableSet<LoopContract>	getApplicableContracts(AbstractAuxiliaryContractRule.Instantiation instantiation, Goal goal, Services services)
static ImmutableSet<LoopContract>	getApplicableContracts(SpecificationRepository specifications, JavaStatement statement, Modality modality, Goal goal)
AbstractAuxiliaryContractRule.Instantiation	instantiate(Term formula, Goal goal, Services services)
boolean	isApplicable(Goal goal, PosInOccurrence occurrence) returns true iff a rule is applicable at the given position.

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

createLocalAnonUpdate, createLocalVariable, displayName, getLastFocusTerm, getLastInstantiation, isApplicableOnSubTerms, occursNotAtTopLevelInSuccedent, register, setLastFocusTerm, setLastInstantiation, toString

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.rule.BuiltInRule

createApp

Methods inherited from interface de.uka.ilkd.key.rule.Rule

apply, name

Constructor Detail

AbstractLoopContractRule

public AbstractLoopContractRule()

Method Detail

getApplicableContracts

public static ImmutableSet<LoopContract> getApplicableContracts(AbstractAuxiliaryContractRule.Instantiation instantiation,
                                                                Goal goal,
                                                                Services services)

Parameters:

instantiation - an instantiation.

goal - the current goal.

services - services.

Returns:

all applicable loop contracts for the instantiation.

getApplicableContracts

public static ImmutableSet<LoopContract> getApplicableContracts(SpecificationRepository specifications,
                                                                JavaStatement statement,
                                                                Modality modality,
                                                                Goal goal)

Parameters:

specifications - a specification repository.

statement - a statement.

modality - the current goal's modality.

goal - the current goal.

Returns:

all applicable loop contracts for the block from the repository.

filterAppliedContracts

protected static ImmutableSet<LoopContract> filterAppliedContracts(ImmutableSet<LoopContract> collectedContracts,
                                                                   Goal goal)

Parameters:

collectedContracts - a set of loop contracts.

goal - the current goal.

Returns:

the set with all non-applicable contracts filtered out.

contractApplied

protected static boolean contractApplied(LoopContract contract,
                                         Goal goal)

Parameters:

contract - a loop contract.

goal - the current goal.

Returns:

true if the contract has already been applied.

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)

instantiate

public AbstractAuxiliaryContractRule.Instantiation instantiate(Term formula,
                                                               Goal goal,
                                                               Services services)

Parameters:

formula - the formula on which the rule is to be applied.

goal - the current goal.

services - services.

Returns:

a new instantiation.

createAndRegisterAnonymisationVariables

protected java.util.Map<LocationVariable,Function> createAndRegisterAnonymisationVariables(java.lang.Iterable<LocationVariable> variables,
                                                                                           LoopContract contract,
                                                                                           TermServices services)

Parameters:

variables - variables.

contract - a loop contract.

services - services.

Returns:

a map from every variable that is changed in the block to its anonymization constant.