de.uka.ilkd.key.rule

Class AuxiliaryContractBuilders.VariablesCreatorAndRegistrar

java.lang.Object

de.uka.ilkd.key.rule.AuxiliaryContractBuilders.VariablesCreatorAndRegistrar

Enclosing class:

AuxiliaryContractBuilders

public static final class AuxiliaryContractBuilders.VariablesCreatorAndRegistrar
extends java.lang.Object

This class contains methods to create new variables from the contract's placeholder variables (see AuxiliaryContract.getPlaceholderVariables()), and register them.

Field Summary

Fields

Modifier and Type	Field and Description
private Goal	goal The current goal.
private AuxiliaryContract.Variables	placeholderVariables
private Services	services Services.

Constructor Summary

Constructors

Constructor and Description
VariablesCreatorAndRegistrar(Goal goal, AuxiliaryContract.Variables placeholderVariables, Services services)

Method Summary

Modifier and Type	Method and Description
private <K> java.util.Map<K,LocationVariable>	appendSuffix(java.util.Map<K,LocationVariable> map, java.lang.String suffix)
AuxiliaryContract.Variables	createAndRegister(Term self, boolean existingPO)
AuxiliaryContract.Variables	createAndRegister(Term self, boolean existingPO, ProgramElement pe)
AuxiliaryContract.Variables	createAndRegisterCopies(java.lang.String suffix) Creates and registers copies of the remembrance variables and heaps.
private java.util.Map<Label,ProgramVariable>	createAndRegisterFlags(java.util.Map<Label,ProgramVariable> placeholderFlags)
private java.util.Map<LocationVariable,LocationVariable>	createAndRegisterRemembranceVariables(java.util.Map<LocationVariable,LocationVariable> remembranceVariables)
private LocationVariable	createAndRegisterVariable(ProgramVariable placeholderVariable)
private void	replaceOuterRemembranceVarsInInnerContracts(ProgramElement pe, java.util.Map<LocationVariable,LocationVariable> outerRemembranceHeaps, java.util.Map<LocationVariable,LocationVariable> outerRemembranceVariables) Replace the outer remembrance variables of all contracts on blocks in pe.

Methods inherited from class java.lang.Object

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

Field Detail

goal

private final Goal goal

The current goal.

placeholderVariables

private final AuxiliaryContract.Variables placeholderVariables

See Also:

AuxiliaryContract.getPlaceholderVariables()

services

private final Services services

Services.

Constructor Detail

VariablesCreatorAndRegistrar

public VariablesCreatorAndRegistrar(Goal goal,
                                    AuxiliaryContract.Variables placeholderVariables,
                                    Services services)

Parameters:

goal - If this is not null, all created variables are added to it. If it is null, the variables are instead added to the services' namespace.

placeholderVariables - the placeholders from which to create the variables.

services - services.

Method Detail

createAndRegister

public AuxiliaryContract.Variables createAndRegister(Term self,
                                                     boolean existingPO)

Parameters:

self - the self term

existingPO - true if we are applying a rule in an existing proof obligation, false if we are creating a new proof obligation.

Returns:

the registered variables.

createAndRegister

public AuxiliaryContract.Variables createAndRegister(Term self,
                                                     boolean existingPO,
                                                     ProgramElement pe)

Parameters:

self - the self term

existingPO - true if we are applying a rule in an existing proof obligation, false if we are creating a new proof obligation.

pe - if existingPO == false, all contracts on blocks in this program element will have their remembrance variables replaced by the one created here.

Returns:

the registered variables.

createAndRegisterCopies

public AuxiliaryContract.Variables createAndRegisterCopies(java.lang.String suffix)

Creates and registers copies of the remembrance variables and heaps.

Parameters:

suffix - a suffix for the new variables' names.

Returns:

a AuxiliaryContract.Variables object containing the new ProgramVariables.

appendSuffix

private <K> java.util.Map<K,LocationVariable> appendSuffix(java.util.Map<K,LocationVariable> map,
                                                           java.lang.String suffix)

Parameters:

map - a map containing variables.

suffix - a suffix.

Returns:

the map with the suffix appended to every variable's name.

createAndRegisterFlags

private java.util.Map<Label,ProgramVariable> createAndRegisterFlags(java.util.Map<Label,ProgramVariable> placeholderFlags)

Parameters:

placeholderFlags - the placeholder flags.

Returns:

newly created and registered flags with the same names.

createAndRegisterRemembranceVariables

private java.util.Map<LocationVariable,LocationVariable> createAndRegisterRemembranceVariables(java.util.Map<LocationVariable,LocationVariable> remembranceVariables)

Parameters:

remembranceVariables - the placeholder remembrance variables.

Returns:

newly created and registered remembrance variables with the same names.

createAndRegisterVariable

private LocationVariable createAndRegisterVariable(ProgramVariable placeholderVariable)

Parameters:

placeholderVariable - a placeholder variable

Returns:

a newly created and registered variable with the same name.

replaceOuterRemembranceVarsInInnerContracts

private void replaceOuterRemembranceVarsInInnerContracts(ProgramElement pe,
                                                         java.util.Map<LocationVariable,LocationVariable> outerRemembranceHeaps,
                                                         java.util.Map<LocationVariable,LocationVariable> outerRemembranceVariables)

Replace the outer remembrance variables of all contracts on blocks in pe.

Parameters:

pe - the program elements.

outerRemembranceHeaps - the new outer remembrance heaps.

outerRemembranceVariables - the new outer remembrance variables.

See Also:

createAndRegister(Term, boolean, ProgramElement)