public static class BlockContractImpl.Creator extends AbstractAuxiliaryContractImpl.Creator<BlockContract>
BlockContractImpl
s.services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
Creator(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Behavior behavior,
AuxiliaryContract.Variables variables,
java.util.Map<LocationVariable,Term> requires,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
ImmutableList<InfFlowSpec> infFlowSpecs,
java.util.Map<Label,Term> breaks,
java.util.Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
java.util.Map<LocationVariable,Term> assignables,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected BlockContract |
build(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod) |
buildPostconditions, buildPreconditions, create
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
public Creator(java.lang.String baseName, StatementBlock block, java.util.List<Label> labels, IProgramMethod method, Behavior behavior, AuxiliaryContract.Variables variables, java.util.Map<LocationVariable,Term> requires, Term measuredBy, java.util.Map<LocationVariable,Term> ensures, ImmutableList<InfFlowSpec> infFlowSpecs, java.util.Map<Label,Term> breaks, java.util.Map<Label,Term> continues, Term returns, Term signals, Term signalsOnly, Term diverges, java.util.Map<LocationVariable,Term> assignables, java.util.Map<LocationVariable,java.lang.Boolean> hasMod, Services services)
baseName
- the contract's base name.block
- the block the contract belongs to.labels
- all labels belonging to the block.method
- the method containing the block.behavior
- the contract's behavior.variables
- the variables.requires
- the contract's precondition.measuredBy
- the contract's measured-by clause.ensures
- the contracts postcondition due to normal termination.infFlowSpecs
- the contract's information flow specifications.breaks
- the contract's postconditions for abrupt termination with break
statements.continues
- the contract's postconditions for abrupt termination with continue
statements.returns
- the contract's postcondition for abrupt termination with return
statements.signals
- the contract's postcondition for abrupt termination due to abrupt termination.signalsOnly
- a term specifying which uncaught exceptions may occur.diverges
- a diverges clause.assignables
- map from every heap to an assignable term.hasMod
- map specifying on which heaps this contract has a modifies clause.services
- services.protected BlockContract build(java.lang.String baseName, StatementBlock block, java.util.List<Label> labels, IProgramMethod method, Modality modality, java.util.Map<LocationVariable,Term> preconditions, Term measuredBy, java.util.Map<LocationVariable,Term> postconditions, java.util.Map<LocationVariable,Term> modifiesClauses, ImmutableList<InfFlowSpec> infFlowSpecs, AuxiliaryContract.Variables variables, boolean transactionApplicable, java.util.Map<LocationVariable,java.lang.Boolean> hasMod)
build
in class AbstractAuxiliaryContractImpl.Creator<BlockContract>
baseName
- the base name.block
- the block this contract belongs to.labels
- all labels belonging to the block.method
- the method containing the block.modality
- this contract's modality.preconditions
- this contract's preconditions on every heap.measuredBy
- this contract's measured-by term.postconditions
- this contract's postconditions on every heap.modifiesClauses
- this contract's modifies clauses on every heap.infFlowSpecs
- this contract's information flow specifications.variables
- this contract's variables.transactionApplicable
- whether or not this contract is applicable for transactions.hasMod
- a map specifying on which heaps this contract has a modified clause.T
with the specified attributes.