de.uka.ilkd.key.rule

Class AuxiliaryContractBuilders.UpdatesBuilder

java.lang.Object

de.uka.ilkd.key.logic.TermBuilder

de.uka.ilkd.key.rule.AuxiliaryContractBuilders.UpdatesBuilder

Enclosing class:

AuxiliaryContractBuilders

public static final class AuxiliaryContractBuilders.UpdatesBuilder
extends TermBuilder

This class is used to build the various updates that are needed for block/loop contract rules.

Field Summary

Fields

Modifier and Type	Field and Description
private AuxiliaryContract.Variables	variables

Fields inherited from class de.uka.ilkd.key.logic.TermBuilder

services, WD_ANY, WD_FORMULA

Constructor Summary

Constructors

Constructor and Description
UpdatesBuilder(AuxiliaryContract.Variables variables, Services services)

Method Summary

Modifier and Type	Method and Description
Term	buildAnonInUpdate(java.util.Map<LocationVariable,Function> anonymisationHeaps)
Term	buildAnonOutUpdate(java.util.Map<LocationVariable,Function> anonymisationHeaps, java.util.Map<LocationVariable,Term> modifiesClauses)
Term	buildAnonOutUpdate(ProgramElement el, java.util.Map<LocationVariable,Function> anonymisationHeaps, java.util.Map<LocationVariable,Term> modifiesClauses)
Term	buildAnonOutUpdate(ProgramElement el, java.util.Map<LocationVariable,Function> anonymisationHeaps, java.util.Map<LocationVariable,Term> modifiesClauses, java.lang.String prefix)
Term	buildAnonOutUpdate(java.util.Set<LocationVariable> vars, java.util.Map<LocationVariable,Function> anonymisationHeaps, java.util.Map<LocationVariable,Term> modifiesClauses, java.lang.String prefix)
private Term	buildLocalVariablesAnonUpdate(java.util.Collection<LocationVariable> vars, java.lang.String prefix)
Term	buildOuterRemembranceUpdate()
Term	buildRemembranceUpdate(java.util.List<LocationVariable> heaps)

Methods inherited from class de.uka.ilkd.key.logic.TermBuilder

acc, add, addLabel, addLabel, all, all, allClose, allFields, allLocs, allObjects, and, and, and, andPreserveLabels, andPreserveLabels, andSC, andSC, andSC, anon, anonUpd, apply, apply, apply, applyElementary, applyElementary, applyElementary, applyParallel, applyParallel, applyParallel, applySequential, applySequential, applyUpdatePairsSequential, arr, arrayRange, arrayStore, box, bprod, bsum, cast, classErroneous, classInitializationInProgress, classInitialized, classPrepared, convertToBoolean, convertToFormula, create, created, created, createdInHeap, createdLocs, cTerm, deepNonNull, dia, disjoint, dot, dot, dot, dotArr, dotLength, elementary, elementary, elementOf, empty, equals, ex, ex, exactInstance, excVar, excVar, FALSE, ff, fieldStore, forallHeaps, frame, frameStrictlyEmpty, freshLocs, func, func, func, func, func, func, geq, getBaseHeap, getMeasuredByEmpty, getSorts, goBelowUpdates, goBelowUpdates2, gt, heapAtPreVar, heapAtPreVar, ife, ifEx, ifEx, imp, imp, impPreserveLabels, inByte, inChar, index, indexOf, infiniteUnion, infiniteUnion, inInt, initialized, inLong, inShort, instance, intersect, intersect, intersect, inv, inv, label, label, leq, lt, max, measuredBy, measuredByCheck, measuredByEmpty, min, newName, newName, newName, not, notPreserveLabels, NULL, one, open, or, or, or, orPreserveLabels, orPreserveLabels, orSC, orSC, orSC, pair, parallel, parallel, parallel, parallel, parallel, paramVars, paramVars, parseTerm, parseTerm, permissionsFor, permissionsFor, prec, prod, prog, prog, reach, reachableValue, reachableValue, reachableValue, resultVar, resultVar, select, select, selfVar, selfVar, selfVar, selfVar, seq, seq, seqConcat, seqDef, seqEmpty, seqGet, seqLen, seqReverse, seqSingleton, seqSub, sequential, sequential, sequential, setComprehension, setComprehension, setMinus, shortBaseName, shortcut, singleton, skip, staticDot, staticDot, staticFieldStore, staticInv, staticInv, store, strictlyNothing, subset, subst, subst, sum, tf, TRUE, tt, union, union, union, unionToSet, unlabel, unlabelRecursive, values, var, var, var, var, var, var, wd, wd, wd, wellFormed, wellFormed, zero, zTerm, zTerm

Methods inherited from class java.lang.Object

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

Field Detail

variables

private final AuxiliaryContract.Variables variables

See Also:

AuxiliaryContract.getVariables()

Constructor Detail

UpdatesBuilder

public UpdatesBuilder(AuxiliaryContract.Variables variables,
                      Services services)

Parameters:

variables - the variables for the contract being applied.

services - services.

Method Detail

buildRemembranceUpdate

public Term buildRemembranceUpdate(java.util.List<LocationVariable> heaps)

Parameters:

heaps - the heaps.

Returns:

a remembrance update for the specified heaps.

buildOuterRemembranceUpdate

public Term buildOuterRemembranceUpdate()

Returns:

an outer remembrance update.

buildAnonOutUpdate

public Term buildAnonOutUpdate(java.util.Map<LocationVariable,Function> anonymisationHeaps,
                               java.util.Map<LocationVariable,Term> modifiesClauses)

Parameters:

anonymisationHeaps - anonymization heaps.

modifiesClauses - modifies clauses for the specified heaps.

Returns:

an anonymization update for the specified modifies clauses.

buildAnonOutUpdate

public Term buildAnonOutUpdate(ProgramElement el,
                               java.util.Map<LocationVariable,Function> anonymisationHeaps,
                               java.util.Map<LocationVariable,Term> modifiesClauses)

Parameters:

el - a program element

anonymisationHeaps - anonymization heaps.

modifiesClauses - modifies clauses for the specified heaps.

Returns:

an anonymization update for the specified modifies clauses and for every modified variable that occurs in the specified program element.

buildAnonOutUpdate

public Term buildAnonOutUpdate(ProgramElement el,
                               java.util.Map<LocationVariable,Function> anonymisationHeaps,
                               java.util.Map<LocationVariable,Term> modifiesClauses,
                               java.lang.String prefix)

Parameters:

el - a program element

anonymisationHeaps - anonymization heaps.

modifiesClauses - modifies clauses for the specified heaps.

prefix - a prefix for the name of the anon functions.

Returns:

an anonymization update for the specified modifies clauses and for every modified variable that occurs in the specified program element.

buildAnonOutUpdate

public Term buildAnonOutUpdate(java.util.Set<LocationVariable> vars,
                               java.util.Map<LocationVariable,Function> anonymisationHeaps,
                               java.util.Map<LocationVariable,Term> modifiesClauses,
                               java.lang.String prefix)

Parameters:

vars - a set of variables

anonymisationHeaps - anonymization heaps.

modifiesClauses - modifies clauses for the specified heaps.

prefix - a prefix for the name of the anon functions.

Returns:

an anonymization update for the specified modifies clauses and for every variable in the specified set.

buildAnonInUpdate

public Term buildAnonInUpdate(java.util.Map<LocationVariable,Function> anonymisationHeaps)

Parameters:

anonymisationHeaps - anonymization heaps.

Returns:

an anonymization update for all heap locations.

buildLocalVariablesAnonUpdate

private Term buildLocalVariablesAnonUpdate(java.util.Collection<LocationVariable> vars,
                                           java.lang.String prefix)

Parameters:

vars - a collection of variables.

prefix - a prefix for the name of the anonymization constants.

Returns:

an anonymization update for the specified variables.