public class LoopInfFlowUnfoldTacletBuilder extends AbstractInfFlowUnfoldTacletBuilder
AbstractInfFlowTacletBuilder.QuantifiableVariableVisitor| Modifier and Type | Field and Description |
|---|---|
private ExecutionContext |
executionContext |
private Term |
guard |
private LoopSpecification |
loopInv |
UNFOLD, unfoldCounterservices, 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, setReplacewithaddVarconds, collectQuantifiableVariables, createTermSV, createTermSV, createVariableSV, eqAtLocs, eqAtLocsPostacc, 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, zTermprivate 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 AbstractInfFlowUnfoldTacletBuilderTerm createFindTerm(IFProofObligationVars ifVars)
createFindTerm in class AbstractInfFlowUnfoldTacletBuilder