de.uka.ilkd.key.rule

Class BlockContractInternalRule

java.lang.Object

de.uka.ilkd.key.rule.AbstractAuxiliaryContractRule

de.uka.ilkd.key.rule.AbstractBlockContractRule

de.uka.ilkd.key.rule.BlockContractInternalRule

All Implemented Interfaces:

BuiltInRule, Rule

public final class BlockContractInternalRule
extends AbstractBlockContractRule

Rule for the application of BlockContracts.

This splits the goal into two branches:

1. Validity
2. Precondition
3. Usage

Author:

wacker, lanzinger

See Also:

BlockContractInternalBuiltInRuleApp

Nested Class Summary

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

AbstractBlockContractRule.BlockContractHint, AbstractBlockContractRule.InfFlowValidityData, AbstractBlockContractRule.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 BlockContractInternalRule	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	BlockContractInternalRule()

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.
BlockContractInternalBuiltInRuleApp	createApp(PosInOccurrence occurrence, TermServices services)
private static Term[]	createAssumptions(ImmutableSet<ProgramVariable> localOutVariables, java.util.Map<LocationVariable,Function> anonymisationHeaps, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)
private static Term[]	createPreconditions(BlockContract contract, Term self, 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)
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)
private void	setUpValidityGoal(ImmutableList<Goal> result, boolean isInfFlow, BlockContract contract, BlockContractInternalBuiltInRuleApp application, AbstractAuxiliaryContractRule.Instantiation instantiation, java.util.List<LocationVariable> heaps, java.util.Map<LocationVariable,Function> anonymisationHeaps, ImmutableSet<ProgramVariable> localInVariables, ImmutableSet<ProgramVariable> localOutVariables, AuxiliaryContract.Variables variables, Term[] preconditions, Term[] assumptions, Term frameCondition, Term[] updates, AuxiliaryContractBuilders.GoalsConfigurator configurator, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder, Services services) Sets up the validity goal as the first goal in the list.
private static ImmutableList<Goal>	splitIntoGoals(Goal goal, BlockContract contract, java.util.List<LocationVariable> heaps, ImmutableSet<ProgramVariable> localInVariables, java.util.Map<LocationVariable,Function> anonymisationHeaps, Term contextUpdate, Term remembranceUpdate, ImmutableSet<ProgramVariable> localOutVariables, AuxiliaryContractBuilders.GoalsConfigurator configurator, Services services)

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

buildAfterVar, buildBodyPreservesSequent, buildInfFlowPostAssumption, buildInfFlowPreAssumption, buildLocalOutsAtPost, buildLocalOutsAtPre, contractApplied, createAndRegisterAnonymisationVariables, filterAppliedContracts, getApplicableContracts, getApplicableContracts, instantiate, setUpInfFlowPartOfUsageGoal, setUpInfFlowValidityGoal

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

BlockContractInternalRule

private BlockContractInternalRule()

Method Detail

createPreconditions

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

Parameters:

contract - the contract being applied.

self - the self term.

heaps - the heaps.

localInVariables - all free program variables in the block.

conditionsAndClausesBuilder - a ConditionsAndClausesBuilder.

services - services.

Returns:

the preconditions.

createAssumptions

private static Term[] createAssumptions(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:

the postconditions.

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 modified clauses.

services - services.

Returns:

the updates.

splitIntoGoals

private static ImmutableList<Goal> splitIntoGoals(Goal goal,
                                                  BlockContract contract,
                                                  java.util.List<LocationVariable> heaps,
                                                  ImmutableSet<ProgramVariable> localInVariables,
                                                  java.util.Map<LocationVariable,Function> anonymisationHeaps,
                                                  Term contextUpdate,
                                                  Term remembranceUpdate,
                                                  ImmutableSet<ProgramVariable> localOutVariables,
                                                  AuxiliaryContractBuilders.GoalsConfigurator configurator,
                                                  Services services)

Parameters:

goal - the current goal.

contract - the contract being applied.

heaps - the heaps.

localInVariables - all free program variables in the block.

anonymisationHeaps - the anonymization heaps.

contextUpdate - the context update.

remembranceUpdate - the remembrance update.

localOutVariables - all free program variables modified by the block.

configurator - a configurator.

services - services.

Returns:

a list containing the new goals.

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

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 AbstractBlockContractRule

setUpValidityGoal

private void setUpValidityGoal(ImmutableList<Goal> result,
                               boolean isInfFlow,
                               BlockContract contract,
                               BlockContractInternalBuiltInRuleApp application,
                               AbstractAuxiliaryContractRule.Instantiation instantiation,
                               java.util.List<LocationVariable> heaps,
                               java.util.Map<LocationVariable,Function> anonymisationHeaps,
                               ImmutableSet<ProgramVariable> localInVariables,
                               ImmutableSet<ProgramVariable> localOutVariables,
                               AuxiliaryContract.Variables variables,
                               Term[] preconditions,
                               Term[] assumptions,
                               Term frameCondition,
                               Term[] updates,
                               AuxiliaryContractBuilders.GoalsConfigurator configurator,
                               AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder,
                               Services services)

Sets up the validity goal as the first goal in the list.

Parameters:

result - the new goals.

isInfFlow - whether or not this is an information flow proof.

contract - the block contract being applied.

application - the rule application.

instantiation - the instantiation.

heaps - the heaps.

anonymisationHeaps - the anonymization heaps.

localInVariables - all free program variables in the block.

localOutVariables - all free program variables modified by the block.

variables - the variables.

preconditions - the preconditions.

assumptions - the postconditions.

frameCondition - the framing condition.

updates - the updates.

configurator - a Configurator.

conditionsAndClausesBuilder - a ConditionsAndClausesBuilder

services - services.