public static class LoopContractImpl.Creator extends AbstractAuxiliaryContractImpl.Creator<LoopContract>
LoopContractImpl
s.Modifier and Type | Field and Description |
---|---|
private Term |
decreases |
private LoopStatement |
loop
null if this contracts belongs to a block instead of a loop,
the loop this contract belongs to otherwise. |
services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
Creator(java.lang.String baseName,
LoopStatement loop,
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,
Term decreases,
Services services)
Creates loop contract for a loop.
|
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,
Term decreases,
Services services)
Creates loop contract for a block that starts with a loop.
|
Modifier and Type | Method and Description |
---|---|
protected LoopContract |
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) |
protected java.util.Map<LocationVariable,Term> |
buildPreconditions() |
buildPostconditions, 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
private Term decreases
LoopContract.getDecreases()
private LoopStatement loop
null
if this contracts belongs to a block instead of a loop,
the loop this contract belongs to otherwise.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, Term decreases, 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.decreases
- the decreases term.services
- services.public Creator(java.lang.String baseName, LoopStatement loop, 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, Term decreases, Services services)
baseName
- the contract's base name.loop
- the loop 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.decreases
- the decreases term.services
- services.protected LoopContract 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<LoopContract>
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.protected java.util.Map<LocationVariable,Term> buildPreconditions()
buildPreconditions
in class AbstractAuxiliaryContractImpl.Creator<LoopContract>