public static class LoopContractImpl.Creator extends AbstractAuxiliaryContractImpl.Creator<LoopContract>
LoopContractImpl
s.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,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
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,
java.util.Map<LocationVariable,Term> requiresFree,
Term measuredBy,
java.util.Map<LocationVariable,Term> ensures,
java.util.Map<LocationVariable,Term> ensuresFree,
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,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
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() |
buildFreePostconditions, buildFreePreconditions, buildPostconditions, create
acc, add, addLabel, addLabel, addLabelToAllSubs, addLabelToAllSubs, 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, replace, 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, java.util.Map<LocationVariable,Term> requiresFree, Term measuredBy, java.util.Map<LocationVariable,Term> ensures, java.util.Map<LocationVariable,Term> ensuresFree, 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, java.util.Map<LocationVariable,Term> requiresFree, Term measuredBy, java.util.Map<LocationVariable,Term> ensures, java.util.Map<LocationVariable,Term> ensuresFree, 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, java.util.Map<LocationVariable,Term> freePreconditions, Term measuredBy, java.util.Map<LocationVariable,Term> postconditions, java.util.Map<LocationVariable,Term> freePostconditions, 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>
Copyright © 2003-2019 The KeY-Project.