public final class InfFlowLoopInvariantTacletBuilder extends AbstractInfFlowContractAppTacletBuilder
AbstractInfFlowTacletBuilder.QuantifiableVariableVisitor
Modifier and Type | Field and Description |
---|---|
private ExecutionContext |
executionContext |
private Term |
guard |
private LoopSpecification |
loopinvariant |
USE_IF
services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
InfFlowLoopInvariantTacletBuilder(Services services) |
Modifier and Type | Method and Description |
---|---|
(package private) Term |
buildContractApplications(ProofObligationVars contAppData,
ProofObligationVars contAppData2,
Services services) |
(package private) Name |
generateName() |
(package private) Term |
generateSchemaAssumes(ProofObligationVars schemaDataAssumes,
Services services) |
(package private) Term |
generateSchemaFind(ProofObligationVars schemaDataFind,
Services services) |
(package private) Term |
getContractApplPred(ProofObligationVars appData) |
void |
setExecutionContext(ExecutionContext context) |
void |
setGuard(Term guard) |
void |
setInvariant(LoopSpecification invariant) |
buildContractApplPredTerm, buildTaclet, generateApplicationDataSVs, setContextUpdate, setProofObligationVars
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 loopinvariant
private ExecutionContext executionContext
private Term guard
public InfFlowLoopInvariantTacletBuilder(Services services)
public void setInvariant(LoopSpecification invariant)
public void setExecutionContext(ExecutionContext context)
public void setGuard(Term guard)
Name generateName()
generateName
in class AbstractInfFlowContractAppTacletBuilder
Term generateSchemaAssumes(ProofObligationVars schemaDataAssumes, Services services)
generateSchemaAssumes
in class AbstractInfFlowContractAppTacletBuilder
Term generateSchemaFind(ProofObligationVars schemaDataFind, Services services)
generateSchemaFind
in class AbstractInfFlowContractAppTacletBuilder
Term getContractApplPred(ProofObligationVars appData)
getContractApplPred
in class AbstractInfFlowContractAppTacletBuilder
Term buildContractApplications(ProofObligationVars contAppData, ProofObligationVars contAppData2, Services services)
buildContractApplications
in class AbstractInfFlowContractAppTacletBuilder