de.uka.ilkd.key.rule

Class AuxiliaryContractBuilders

java.lang.Object

de.uka.ilkd.key.rule.AuxiliaryContractBuilders

public final class AuxiliaryContractBuilders
extends java.lang.Object

This contains various builders used in building formulae and terms for block and loop contracts.

Author:

wacker, lanzinger

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	AuxiliaryContractBuilders.ConditionsAndClausesBuilder This class is used to build various sub-formulas used in the block/loop contract rules.s
static class	AuxiliaryContractBuilders.GoalsConfigurator This class contains methods to add the premisses for the block contract rule to the goal.
static class	AuxiliaryContractBuilders.UpdatesBuilder This class is used to build the various updates that are needed for block/loop contract rules.
static class	AuxiliaryContractBuilders.ValidityProgramConstructor This class is used to construct block' from block (see Wacker 2012, 3.3).
static class	AuxiliaryContractBuilders.VariablesCreatorAndRegistrar 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
static java.lang.String	ANON_IN_PREFIX Prefix for all anonymization constants in AuxiliaryContractBuilders.UpdatesBuilder.buildAnonInUpdate(Map).
static java.lang.String	ANON_OUT_PREFIX Prefix for all anonymization constants in AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(Map, Map).

Constructor Summary

Constructors

Modifier	Constructor and Description
private	AuxiliaryContractBuilders()

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

ANON_IN_PREFIX

public static final java.lang.String ANON_IN_PREFIX

Prefix for all anonymization constants in AuxiliaryContractBuilders.UpdatesBuilder.buildAnonInUpdate(Map).

See Also:

Constant Field Values

ANON_OUT_PREFIX

public static final java.lang.String ANON_OUT_PREFIX

Prefix for all anonymization constants in AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(Map, Map).

See Also:

Constant Field Values

Constructor Detail

AuxiliaryContractBuilders

private AuxiliaryContractBuilders()