public static final class AuxiliaryContractBuilders.ConditionsAndClausesBuilder extends TermBuilder
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 |
services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
ConditionsAndClausesBuilder(AuxiliaryContract contract,
java.util.List<LocationVariable> heaps,
AuxiliaryContract.Variables variables,
Term self,
Services services) |
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
protected final AuxiliaryContract.Terms terms
AuxiliaryContract.getVariables()
,
AuxiliaryContract.Variables#termify(Term)
private final AuxiliaryContract contract
private final java.util.List<LocationVariable> heaps
private final AuxiliaryContract.Variables variables
AuxiliaryContract.getVariables()
public ConditionsAndClausesBuilder(AuxiliaryContract contract, java.util.List<LocationVariable> heaps, AuxiliaryContract.Variables variables, Term self, Services services)
contract
- the contract being applied.heaps
- the heaps.variables
- the variables.self
- the self term.services
- services.public AuxiliaryContract.Terms getTerms()
public Term buildPrecondition()
public Term buildWellFormedHeapsCondition()
public Term buildReachableInCondition(ImmutableSet<ProgramVariable> localInVariables)
localInVariables
- all free local variables in the block.public Term buildReachableOutCondition(ImmutableSet<ProgramVariable> localOutVariables)
localOutVariables
- all free local variables modified by the block.public Term buildReachableCondition(ImmutableSet<ProgramVariable> variables)
variables
- a set of variables.public java.util.Map<LocationVariable,Term> buildModifiesClauses()
public Term buildDecreasesCheck()
public Term buildPostcondition()
public Term buildFrameCondition(java.util.Map<LocationVariable,Term> modifiesClauses)
modifiesClauses
- the contract's modifies clausesprivate java.util.Map<LocationVariable,java.util.Map<Term,Term>> constructRemembranceVariables()
private LocationVariable getBaseHeapFunction()
public Term buildWellFormedAnonymisationHeapsCondition(java.util.Map<LocationVariable,Function> anonymisationHeaps)
anonymisationHeaps
- anonymisation heaps.public Term buildAtMostOneFlagSetCondition()
true
.public Term buildSelfConditions(java.util.List<LocationVariable> heaps, IProgramMethod pm, KeYJavaType selfKJT, Term self, Services services)
self
variable
(self != null & self.created == true & exactInstance(self)
)heaps
- the heaps.pm
- the method containg the block.selfKJT
- the self variable's type.self
- the self variable.services
- services.self
variable.private java.util.List<Term> buildFlagsNotSetConditions(java.util.Collection<ProgramVariable> flags)
flags
- a collection of boolean variables.false
.private Term buildFlagNotSetCondition(ProgramVariable flag)
flag
- a boolean variable.false
.