abstract class AbstractInfFlowUnfoldTacletBuilder extends AbstractInfFlowTacletBuilder
AbstractInfFlowTacletBuilder.QuantifiableVariableVisitor
Modifier and Type | Field and Description |
---|---|
private IFProofObligationVars |
ifVars |
private Term |
replacewith |
private static java.lang.String |
SCHEMA_PREFIX |
(package private) static java.lang.String |
UNFOLD |
(package private) static int |
unfoldCounter
Counter to allow several side-proofs.
|
services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
AbstractInfFlowUnfoldTacletBuilder(Services services) |
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 static final java.lang.String SCHEMA_PREFIX
static final java.lang.String UNFOLD
static int unfoldCounter
private IFProofObligationVars ifVars
private Term replacewith
public AbstractInfFlowUnfoldTacletBuilder(Services services)
public void setInfFlowVars(IFProofObligationVars ifVars)
public void setReplacewith(Term replacewith)
public Taclet buildTaclet()
private IFProofObligationVars generateApplicationDataSVs(IFProofObligationVars ifVars, Services services)
private ProofObligationVars generateApplicationDataSVs(java.lang.String schemaPrefix, ProofObligationVars poVars, Services services)
private static Term replace(Term term, IFProofObligationVars origVars, IFProofObligationVars schemaVars, Services services)
private static Term replace(Term term, ProofObligationVars origVars, ProofObligationVars schemaVars, Services services)
private static Term replace(Term term, StateVars origVars, StateVars schemaVars, Services services)
private static StateVars filterSchemaVars(StateVars origVars, StateVars schemaVars)
abstract Name getTacletName()
abstract Term createFindTerm(IFProofObligationVars ifVars)