public class LoopInfFlowUnfoldTacletBuilder extends AbstractInfFlowUnfoldTacletBuilder
AbstractInfFlowTacletBuilder.QuantifiableVariableVisitor
Modifier and Type | Field and Description |
---|---|
private ExecutionContext |
executionContext |
private Term |
guard |
private LoopSpecification |
loopInv |
UNFOLD, unfoldCounter
services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
LoopInfFlowUnfoldTacletBuilder(Services services) |
Modifier and Type | Method and Description |
---|---|
(package private) Term |
createFindTerm(IFProofObligationVars ifVars) |
(package private) Name |
getTacletName() |
void |
setExecutionContext(ExecutionContext context) |
void |
setGuard(Term guard) |
void |
setLoopInv(LoopSpecification loopInv) |
buildTaclet, setInfFlowVars, setReplacewith
addVarconds, collectQuantifiableVariables, createTermSV, createTermSV, createVariableSV, eqAtLocs, eqAtLocsPost
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
private LoopSpecification loopInv
private ExecutionContext executionContext
private Term guard
public LoopInfFlowUnfoldTacletBuilder(Services services)
public void setLoopInv(LoopSpecification loopInv)
public void setExecutionContext(ExecutionContext context)
public void setGuard(Term guard)
Name getTacletName()
getTacletName
in class AbstractInfFlowUnfoldTacletBuilder
Term createFindTerm(IFProofObligationVars ifVars)
createFindTerm
in class AbstractInfFlowUnfoldTacletBuilder