de.uka.ilkd.key.rule

Class BlockContractExternalRule

java.lang.Object

de.uka.ilkd.key.rule.AbstractAuxiliaryContractRule

de.uka.ilkd.key.rule.AbstractBlockContractRule

de.uka.ilkd.key.rule.BlockContractExternalRule

All Implemented Interfaces:

BuiltInRule, Rule

public final class BlockContractExternalRule
extends AbstractBlockContractRule

Rule for the application of BlockContracts.

This splits the goal into two branches:

1. Precondition
2. Usage

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

Author:

lanzinger

See Also:

BlockContractExternalBuiltInRuleApp

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

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[]	createAssumptions(ImmutableSet<ProgramVariable> localOutVariables, java.util.Map<LocationVariable,Function> anonymisationHeaps, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder)
private static Term[]	createPreconditions(AbstractAuxiliaryContractRule.Instantiation instantiation, BlockContract 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, AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder, 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)

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

BlockContractExternalRule

private BlockContractExternalRule()

Method Detail

createPreconditions

private static Term[] createPreconditions(AbstractAuxiliaryContractRule.Instantiation instantiation,
                                          BlockContract contract,
                                          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,
                                    AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder,
                                    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.

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 AbstractBlockContractRule

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