public final class InfFlowLoopInvariantTacletBuilder extends TermBuilder
services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
InfFlowLoopInvariantTacletBuilder(Services services) |
Modifier and Type | Method and Description |
---|---|
Term |
buildContractApplPredTerm() |
Taclet |
buildTaclet(Goal goal)
Builds the taclet.
|
Term |
eqAtLocs(Services services,
Term heap1,
Term locset1,
Term heap2,
Term locset2)
Get eqAtLocs function as a term.
|
Term |
eqAtLocsPost(Services services,
Term heap1Pre,
Term heap1Post,
Term locset1,
Term heap2Pre,
Term heap2Post,
Term locset2)
Get eqAtLocsPost function as a term.
|
void |
setContextUpdate(Term... contextUpdates) |
void |
setExecutionContext(ExecutionContext context) |
void |
setGuard(Term guard) |
void |
setInvariant(LoopSpecification invariant) |
void |
setProofObligationVars(ProofObligationVars poVars) |
acc, add, addLabel, addLabel, addLabelToAllSubs, addLabelToAllSubs, 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, replace, 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
public InfFlowLoopInvariantTacletBuilder(Services services)
public void setInvariant(LoopSpecification invariant)
public void setExecutionContext(ExecutionContext context)
public void setGuard(Term guard)
public void setContextUpdate(Term... contextUpdates)
public void setProofObligationVars(ProofObligationVars poVars)
public Term buildContractApplPredTerm()
public Taclet buildTaclet(Goal goal)
goal
- the goalpublic Term eqAtLocs(Services services, Term heap1, Term locset1, Term heap2, Term locset2)
services
- the Services object.heap1
- the first heap term.locset1
- the first location set term.heap2
- the first heap term.locset2
- the first location set term.public Term eqAtLocsPost(Services services, Term heap1Pre, Term heap1Post, Term locset1, Term heap2Pre, Term heap2Post, Term locset2)
services
- the Services object.heap1Pre
- the first pre-heap term.heap1Post
- the first post-heap term.locset1
- the first location set term.heap2Pre
- the second pre-heap term.heap2Post
- the second post-heap term.locset2
- the second location set term.Copyright © 2003-2019 The KeY-Project.