public static final class AuxiliaryContractBuilders.VariablesCreatorAndRegistrar
extends java.lang.Object
AuxiliaryContract.getPlaceholderVariables()
), and register them.Constructor and Description |
---|
VariablesCreatorAndRegistrar(Goal goal,
AuxiliaryContract.Variables placeholderVariables,
Services services) |
Modifier and Type | Method and Description |
---|---|
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.
|
public VariablesCreatorAndRegistrar(Goal goal, AuxiliaryContract.Variables placeholderVariables, Services services)
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.public AuxiliaryContract.Variables createAndRegister(Term self, boolean existingPO)
self
- the self termexistingPO
- true
if we are applying a rule in an existing proof obligation,
false
if we are creating a new proof obligation.public AuxiliaryContract.Variables createAndRegister(Term self, boolean existingPO, ProgramElement pe)
self
- the self termexistingPO
- 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.public AuxiliaryContract.Variables createAndRegisterCopies(java.lang.String suffix)
suffix
- a suffix for the new variables' names.AuxiliaryContract.Variables
object containing the new ProgramVariables
.Copyright © 2003-2019 The KeY-Project.