public class LoopInfFlowUnfoldTacletBuilder extends AbstractInfFlowUnfoldTacletBuilder
AbstractInfFlowTacletBuilder.QuantifiableVariableVisitor
Modifier and Type | Field and Description |
---|---|
private ExecutionContext |
executionContext |
private Term |
guard |
private LoopInvariant |
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(LoopInvariant loopInv) |
buildTaclet, setInfFlowVars, setReplacewith
addVarconds, collectQuantifiableVariables, createTermSV, createTermSV, createVariableSV
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, deepNonNull, dia, disjoint, dot, dot, dot, dotArr, dotLength, elementary, elementary, elementOf, empty, eqAtLocs, eqAtLocsPost, 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, 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 LoopInvariant loopInv
private ExecutionContext executionContext
private Term guard
public LoopInfFlowUnfoldTacletBuilder(Services services)
public void setLoopInv(LoopInvariant 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