de.uka.ilkd.key.speclang

Class AbstractAuxiliaryContractImpl.Combinator<T extends AuxiliaryContract>

java.lang.Object

de.uka.ilkd.key.logic.TermBuilder

de.uka.ilkd.key.speclang.AbstractAuxiliaryContractImpl.Combinator<T>

Type Parameters:

T - the type of the subclass.

Direct Known Subclasses:

BlockContractImpl.Combinator, LoopContractImpl.Combinator

Enclosing class:

AbstractAuxiliaryContractImpl

protected abstract static class AbstractAuxiliaryContractImpl.Combinator<T extends AuxiliaryContract>
extends TermBuilder

This class is used to to combine multiple contracts for the same block and apply them simultaneously. It should be overridden in every subclass.

Field Summary

Fields

Modifier and Type	Field and Description
protected T[]	contracts The contracts to combine.
protected java.util.Map<LocationVariable,Term>	modifiesClauses
protected AuxiliaryContract.Variables	placeholderVariables
protected java.util.Map<LocationVariable,Term>	postconditions
protected java.util.Map<LocationVariable,Term>	preconditions
protected java.util.Map<LocationVariable,LocationVariable>	remembranceVariables

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

services, WD_ANY, WD_FORMULA

Constructor Summary

Constructors

Constructor and Description
Combinator(T[] contracts, Services services)

Method Summary

Modifier and Type	Method and Description
protected void	addConditionsFrom(T contract)
private void	addModifiesClauseFrom(T contract, LocationVariable heap)
private void	addPostconditionFrom(Term postcondition, T contract, LocationVariable heap)
private Term	addPreconditionFrom(T contract, LocationVariable heap)
private Term	andPossiblyNull(Term currentCondition, Term additionalCondition)
protected abstract T	combine()
private Term	orPossiblyNull(Term currentCondition, Term additionalCondition)
private Term	preify(Term formula)
private T[]	sort(T[] contracts)
private Term	unionPossiblyNull(Term currentLocationSet, Term additionalLocationSet)

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

contracts

protected final T extends AuxiliaryContract[] contracts

The contracts to combine.

placeholderVariables

protected AuxiliaryContract.Variables placeholderVariables

See Also:

AuxiliaryContract.getPlaceholderVariables()

remembranceVariables

protected java.util.Map<LocationVariable,LocationVariable> remembranceVariables

See Also:

Variables#remembranceLocalVariables

preconditions

protected final java.util.Map<LocationVariable,Term> preconditions

See Also:

AuxiliaryContract.getPrecondition(LocationVariable, Services)

postconditions

protected final java.util.Map<LocationVariable,Term> postconditions

See Also:

AuxiliaryContract.getPostcondition(LocationVariable, Services)

modifiesClauses

protected final java.util.Map<LocationVariable,Term> modifiesClauses

See Also:

AuxiliaryContract.getModifiesClause(LocationVariable, Services)

Constructor Detail

Combinator

public Combinator(T[] contracts,
                  Services services)

Parameters:

contracts - the contracts to combine.

services - services.

Method Detail

sort

private T[] sort(T[] contracts)

Parameters:

contracts - the contract's to sort.

Returns:

an array containg the specified contracts sorted alphabetically by name.

combine

protected abstract T combine()

Returns:

the combined contract.

addConditionsFrom

protected void addConditionsFrom(T contract)

Parameters:

contract - the contract whose conditions to add.

addPreconditionFrom

private Term addPreconditionFrom(T contract,
                                 LocationVariable heap)

Parameters:

contract - the contract whose precondition to add.

heap - the heap to use.

Returns:

the precondition.

addPostconditionFrom

private void addPostconditionFrom(Term postcondition,
                                  T contract,
                                  LocationVariable heap)

Parameters:

postcondition - the postcondition to add.

contract - the contract the postcondition belongs to.

heap - the heap to use.

addModifiesClauseFrom

private void addModifiesClauseFrom(T contract,
                                   LocationVariable heap)

Parameters:

contract - the contract whose modified clause to add.

heap - the heap to use.

orPossiblyNull

private Term orPossiblyNull(Term currentCondition,
                            Term additionalCondition)

Parameters:

currentCondition - a condition or null.

additionalCondition - a condition.

Returns:

the disjunction of the conditions.

andPossiblyNull

private Term andPossiblyNull(Term currentCondition,
                             Term additionalCondition)

Parameters:

currentCondition - a condition or null.

additionalCondition - a condition.

Returns:

the conjunction of the conditions.

unionPossiblyNull

private Term unionPossiblyNull(Term currentLocationSet,
                               Term additionalLocationSet)

Parameters:

currentLocationSet - a location set or null.

additionalLocationSet - a location set.

Returns:

the union of the location sets.

preify

private Term preify(Term formula)

Parameters:

formula - a formula.

Returns:

the formula with all variables replaced by the remembrance variables.