de.uka.ilkd.key.rule

Class AuxiliaryContractBuilders.ConditionsAndClausesBuilder

java.lang.Object

de.uka.ilkd.key.logic.TermBuilder

de.uka.ilkd.key.rule.AuxiliaryContractBuilders.ConditionsAndClausesBuilder

Enclosing class:

AuxiliaryContractBuilders

public static final class AuxiliaryContractBuilders.ConditionsAndClausesBuilder
extends TermBuilder

This class is used to build various sub-formulas used in the block/loop contract rules.s

Field Summary

Fields

Modifier and Type	Field and Description
private AuxiliaryContract	contract The contract being applied
private java.util.List<LocationVariable>	heaps The heaps.
protected AuxiliaryContract.Terms	terms
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
ConditionsAndClausesBuilder(AuxiliaryContract contract, java.util.List<LocationVariable> heaps, AuxiliaryContract.Variables variables, Term self, Services services)

Method Summary

Modifier and Type	Method and Description
Term	buildAtMostOneFlagSetCondition()
Term	buildDecreasesCheck()
private Term	buildFlagNotSetCondition(ProgramVariable flag)
private java.util.List<Term>	buildFlagsNotSetConditions(java.util.Collection<ProgramVariable> flags)
Term	buildFrameCondition(java.util.Map<LocationVariable,Term> modifiesClauses)
java.util.Map<LocationVariable,Term>	buildModifiesClauses()
Term	buildPostcondition()
Term	buildPrecondition()
Term	buildReachableCondition(ImmutableSet<ProgramVariable> variables)
Term	buildReachableInCondition(ImmutableSet<ProgramVariable> localInVariables)
Term	buildReachableOutCondition(ImmutableSet<ProgramVariable> localOutVariables)
Term	buildSelfConditions(java.util.List<LocationVariable> heaps, IProgramMethod pm, KeYJavaType selfKJT, Term self, Services services) Builds the assumptions for the self variable ({@code self !
Term	buildWellFormedAnonymisationHeapsCondition(java.util.Map<LocationVariable,Function> anonymisationHeaps)
Term	buildWellFormedHeapsCondition()
private java.util.Map<LocationVariable,java.util.Map<Term,Term>>	constructRemembranceVariables()
private LocationVariable	getBaseHeapFunction()
AuxiliaryContract.Terms	getTerms()

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

terms

protected final AuxiliaryContract.Terms terms

See Also:

AuxiliaryContract.getVariables(), AuxiliaryContract.Variables#termify(Term)

contract

private final AuxiliaryContract contract

The contract being applied

heaps

private final java.util.List<LocationVariable> heaps

The heaps.

variables

private final AuxiliaryContract.Variables variables

See Also:

AuxiliaryContract.getVariables()

Constructor Detail

ConditionsAndClausesBuilder

public ConditionsAndClausesBuilder(AuxiliaryContract contract,
                                   java.util.List<LocationVariable> heaps,
                                   AuxiliaryContract.Variables variables,
                                   Term self,
                                   Services services)

Parameters:

contract - the contract being applied.

heaps - the heaps.

variables - the variables.

self - the self term.

services - services.

Method Detail

getTerms

public AuxiliaryContract.Terms getTerms()

Returns:

the termified variables.

buildPrecondition

public Term buildPrecondition()

Returns:

the contract's precondition.

buildWellFormedHeapsCondition

public Term buildWellFormedHeapsCondition()

Returns:

the condition that all heaps are well-formed.

buildReachableInCondition

public Term buildReachableInCondition(ImmutableSet<ProgramVariable> localInVariables)

Parameters:

localInVariables - all free local variables in the block.

Returns:

the condition that all of those variables have valid values.

buildReachableOutCondition

public Term buildReachableOutCondition(ImmutableSet<ProgramVariable> localOutVariables)

Parameters:

localOutVariables - all free local variables modified by the block.

Returns:

the condition that all of those variables have valid values.

buildReachableCondition

public Term buildReachableCondition(ImmutableSet<ProgramVariable> variables)

Parameters:

variables - a set of variables.

Returns:

the condition that all of those variables have valid values.

buildModifiesClauses

public java.util.Map<LocationVariable,Term> buildModifiesClauses()

Returns:

the contract's modifies clause.

buildDecreasesCheck

public Term buildDecreasesCheck()

Returns:

the loop contract's decreases clause.

buildPostcondition

public Term buildPostcondition()

Returns:

the contract's postcondition.

buildFrameCondition

public Term buildFrameCondition(java.util.Map<LocationVariable,Term> modifiesClauses)

Parameters:

modifiesClauses - the contract's modifies clauses

Returns:

the contract's framing condition.

constructRemembranceVariables

private java.util.Map<LocationVariable,java.util.Map<Term,Term>> constructRemembranceVariables()

Returns:

a map from every variable to its remembrance variable, for every heap.

getBaseHeapFunction

private LocationVariable getBaseHeapFunction()

Returns:

the base heap.

buildWellFormedAnonymisationHeapsCondition

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

Parameters:

anonymisationHeaps - anonymisation heaps.

Returns:

the condition that all anonymisation heaps are well-formed.

buildAtMostOneFlagSetCondition

public Term buildAtMostOneFlagSetCondition()

Returns:

the condition that at most one flag for abrupt termination is true.

buildSelfConditions

public Term buildSelfConditions(java.util.List<LocationVariable> heaps,
                                IProgramMethod pm,
                                KeYJavaType selfKJT,
                                Term self,
                                Services services)

Builds the assumptions for the self variable (self != null & self.created == true & exactInstance(self))

Parameters:

heaps - the heaps.

pm - the method containg the block.

selfKJT - the self variable's type.

self - the self variable.

services - services.

Returns:

the assumptions for the self variable.

buildFlagsNotSetConditions

private java.util.List<Term> buildFlagsNotSetConditions(java.util.Collection<ProgramVariable> flags)

Parameters:

flags - a collection of boolean variables.

Returns:

the condition that all flags are false.

buildFlagNotSetCondition

private Term buildFlagNotSetCondition(ProgramVariable flag)

Parameters:

flag - a boolean variable.

Returns:

the condition that the flag is false.