de.uka.ilkd.key.rule

Class LoopContractInternalRule

java.lang.Object

de.uka.ilkd.key.rule.AbstractAuxiliaryContractRule

de.uka.ilkd.key.rule.AbstractLoopContractRule

de.uka.ilkd.key.rule.LoopContractInternalRule

All Implemented Interfaces:

BuiltInRule, Rule

public final class LoopContractInternalRule
extends AbstractLoopContractRule

Rule for the application of LoopContracts.

This splits the goal into two branches:

1. Validity
2. Precondition
3. Usage

Author:

lanzinger

See Also:

LoopContractInternalBuiltInRuleApp

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 LoopContractInternalRule	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	LoopContractInternalRule()

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.
LoopContractInternalBuiltInRuleApp	createApp(PosInOccurrence occurrence, TermServices services)
private static Term	createContext(java.util.List<LocationVariable> heaps, AuxiliaryContractBuilders.UpdatesBuilder updatesBuilder, AbstractAuxiliaryContractRule.Instantiation instantiation, Services services)
private static Term[]	createPostconditions(java.util.Map<LocationVariable,Term> modifiesClauses, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)
private static Term[]	createPostconditionsNext(Term selfTerm, LoopContract contract, java.util.List<LocationVariable> heaps, AuxiliaryContract.Variables nextVariables, java.util.Map<LocationVariable,Term> modifiesClauses, Services 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(AbstractAuxiliaryContractRule.Instantiation instantiation, java.util.List<LocationVariable> heaps, java.util.Map<LocationVariable,Function> anonOutHeaps, java.util.Map<LocationVariable,Term> modifiesClauses, AuxiliaryContractBuilders.UpdatesBuilder updatesBuilder)
private static Term[]	createUsageAssumptions(Term[] postconditions, java.util.Map<LocationVariable,Function> anonOutHeaps, ImmutableSet<ProgramVariable> localOutVariables, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)
private static AuxiliaryContract.Variables[]	createVars(Goal goal, Term selfTerm, LoopContract contract, Services services)
Term	getLastFocusTerm()
AbstractAuxiliaryContractRule.Instantiation	getLastInstantiation()
Name	name() the name of the rule
protected void	setLastFocusTerm(Term lastFocusTerm)
protected void	setLastInstantiation(AbstractAuxiliaryContractRule.Instantiation lastInstantiation)
private static void	setUpGoals(Goal goal, ImmutableList<Goal> result, LoopContract contract, AbstractAuxiliaryContractRule.Instantiation instantiation, java.util.Map<LocationVariable,Function> anonOutHeaps, AuxiliaryContract.Variables[] vars, java.util.Map<LocationVariable,Term> modifiesClauses, Term[] assumptions, Term[] usageAssumptions, Term decreasesCheck, Term[] postconditions, Term[] postconditionsNext, Term[] updates, Term nextRemembranceUpdate, Term context, AuxiliaryContractBuilders.GoalsConfigurator configurator, Services services)

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

contractApplied, createAndRegisterAnonymisationVariables, filterAppliedContracts, getApplicableContracts, getApplicableContracts, instantiate, isApplicable

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 LoopContractInternalRule 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

LoopContractInternalRule

private LoopContractInternalRule()

Method Detail

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.

createPostconditions

private static Term[] createPostconditions(java.util.Map<LocationVariable,Term> modifiesClauses,
                                           AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)

Parameters:

localOutVariables - all free program variables modified by the block.

anonymisationHeaps - the anonymization heaps.

conditionsAndClausesBuilder - a ConditionsAndClausesBuilder.

Returns:

the postconditions for the current loop iteration.

createPostconditionsNext

private static Term[] createPostconditionsNext(Term selfTerm,
                                               LoopContract contract,
                                               java.util.List<LocationVariable> heaps,
                                               AuxiliaryContract.Variables nextVariables,
                                               java.util.Map<LocationVariable,Term> modifiesClauses,
                                               Services services)

Parameters:

selfTerm - the self term.

contract - the loop contract being applied.

heaps - the heaps.

nextVariables - the variables for the next loop iteration.

modifiesClauses - the modified clauses

services - services.

Returns:

the postconditions for the next loop iteration.

createContext

private static Term createContext(java.util.List<LocationVariable> heaps,
                                  AuxiliaryContractBuilders.UpdatesBuilder updatesBuilder,
                                  AbstractAuxiliaryContractRule.Instantiation instantiation,
                                  Services services)

Parameters:

heaps - the heaps.

updatesBuilder - an update builder.

instantiation - the instantiation for the current rule application.

services - services.

Returns:

the update for the validity branch.

createUsageAssumptions

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

Parameters:

postconditions - the postconditions.

anonOutHeaps - the heaps used in the anonOut update.

localOutVariables - all free program variables modified by the block.

conditionsAndClausesBuilder - a ConditionsAndClausesBuilder.

Returns:

preconditions for the usage branch.

createUpdates

private static Term[] createUpdates(AbstractAuxiliaryContractRule.Instantiation instantiation,
                                    java.util.List<LocationVariable> heaps,
                                    java.util.Map<LocationVariable,Function> anonOutHeaps,
                                    java.util.Map<LocationVariable,Term> modifiesClauses,
                                    AuxiliaryContractBuilders.UpdatesBuilder updatesBuilder)

Parameters:

instantiation - the instantiation.

heaps - the heaps.

anonOutHeaps - the heaps used in the anonOut update.

modifiesClauses - the modifies clauses.

updatesBuilder - an update builder

Returns:

the updates for the usage branch.

createVars

private static AuxiliaryContract.Variables[] createVars(Goal goal,
                                                        Term selfTerm,
                                                        LoopContract contract,
                                                        Services services)

Parameters:

goal - the current goal.

selfTerm - the self term.

contract - the contract being applied.

services - services.

Returns:

the variables for both the current and the next loop iteration.

setUpGoals

private static void setUpGoals(Goal goal,
                               ImmutableList<Goal> result,
                               LoopContract contract,
                               AbstractAuxiliaryContractRule.Instantiation instantiation,
                               java.util.Map<LocationVariable,Function> anonOutHeaps,
                               AuxiliaryContract.Variables[] vars,
                               java.util.Map<LocationVariable,Term> modifiesClauses,
                               Term[] assumptions,
                               Term[] usageAssumptions,
                               Term decreasesCheck,
                               Term[] postconditions,
                               Term[] postconditionsNext,
                               Term[] updates,
                               Term nextRemembranceUpdate,
                               Term context,
                               AuxiliaryContractBuilders.GoalsConfigurator configurator,
                               Services services)

Parameters:

goal - the current goal.

result - the next goals.

contract - the contract being applied.

instantiation - the instantiation.

anonOutHeaps - the heaps used in the anonOut update.

vars - the variables for both the current and the next loop iteration.

modifiesClauses - the modifies clauses.

assumptions - the preconditions for the validity branch.

usageAssumptions - the preconditions for the usage branch.

decreasesCheck - the decreases check.

postconditions - the postconditions for the current loop iteration.

postconditionsNext - the postconditions for the next loop iteration.

updates - the updates for the usage branch.

nextRemembranceUpdate - the remembrance update for the next loop iteration.

context - the update for the validity branch.

configurator - a configurator.

services - services.

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 LoopContractInternalBuiltInRuleApp createApp(PosInOccurrence occurrence,
                                                    TermServices services)

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