public final class InfFlowLoopInvariantTacletBuilder extends AbstractInfFlowContractAppTacletBuilder
AbstractInfFlowTacletBuilder.QuantifiableVariableVisitor| Modifier and Type | Field and Description |
|---|---|
private ExecutionContext |
executionContext |
private Term |
guard |
private LoopSpecification |
loopinvariant |
USE_IFservices, 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, setProofObligationVarsaddVarconds, 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 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 AbstractInfFlowContractAppTacletBuilderTerm generateSchemaAssumes(ProofObligationVars schemaDataAssumes, Services services)
generateSchemaAssumes in class AbstractInfFlowContractAppTacletBuilderTerm generateSchemaFind(ProofObligationVars schemaDataFind, Services services)
generateSchemaFind in class AbstractInfFlowContractAppTacletBuilderTerm getContractApplPred(ProofObligationVars appData)
getContractApplPred in class AbstractInfFlowContractAppTacletBuilderTerm buildContractApplications(ProofObligationVars contAppData, ProofObligationVars contAppData2, Services services)
buildContractApplications in class AbstractInfFlowContractAppTacletBuilder