T
- the type of the subclass.protected abstract static class AbstractAuxiliaryContractImpl.Creator<T extends AuxiliaryContract> extends TermBuilder
AbstractAuxiliaryContractImpl
s
(create()
). It should be overridden in every subclass.Modifier and Type | Field and Description |
---|---|
private java.util.Map<LocationVariable,Term> |
assignables
A map from every heap to an assignable term.
|
private java.lang.String |
baseName |
private Behavior |
behavior
This contract's behavior.
|
private StatementBlock |
block |
private java.util.Map<Label,Term> |
breaks
Postconditions for abrupt termination with
break statements. |
private java.util.Map<Label,Term> |
continues
Postconditions for abrupt termination with
continue statements. |
private Term |
diverges
A diverges term.
|
private java.util.Map<LocationVariable,Term> |
ensures
Postcondition for normal termination.
|
private java.util.Map<LocationVariable,java.lang.Boolean> |
hasMod
A map specifying on which heaps this contract has a modifies clause.
|
private ImmutableList<LocationVariable> |
heaps
A list of heaps used in this contract.
|
private ImmutableList<InfFlowSpec> |
infFlowSpecs |
private java.util.List<Label> |
labels |
private Term |
measuredBy |
private IProgramMethod |
method |
private java.util.Map<LocationVariable,Term> |
requires |
private Term |
returns
Postcondition for abrupt termination with
return statements. |
private Term |
signals
Postcondition for abrupt termination due to an uncaught exception.
|
private Term |
signalsOnly
A term specifying which uncaught exceptions may occur.
|
private AuxiliaryContract.Variables |
variables |
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) |
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 final java.lang.String baseName
AuxiliaryContract.getBaseName()
private final StatementBlock block
AuxiliaryContract.getBlock()
private final java.util.List<Label> labels
AuxiliaryContract.getLabels()
private final IProgramMethod method
AuxiliaryContract.getMethod()
private final Behavior behavior
private final AuxiliaryContract.Variables variables
AuxiliaryContract.getVariables()
private final Term measuredBy
AuxiliaryContract.getMby()
private final java.util.Map<LocationVariable,Term> requires
private final java.util.Map<LocationVariable,Term> ensures
private final ImmutableList<InfFlowSpec> infFlowSpecs
AuxiliaryContract.getInfFlowSpecs()
private final java.util.Map<Label,Term> breaks
break
statements.private final java.util.Map<Label,Term> continues
continue
statements.private final Term returns
return
statements.private final Term signals
private final Term signalsOnly
private final Term diverges
private final java.util.Map<LocationVariable,Term> assignables
private final ImmutableList<LocationVariable> heaps
private final java.util.Map<LocationVariable,java.lang.Boolean> hasMod
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
termintation.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.public ImmutableSet<T> create()
protected java.util.Map<LocationVariable,Term> buildPreconditions()
protected java.util.Map<LocationVariable,Term> buildPostconditions()
private Term buildPostcondition(LocationVariable heap)
heap
- the heap to use.private Term conditionPostconditions(java.util.Map<Label,ProgramVariable> flags, java.util.Map<Label,Term> postconditions)
flags
- abrupt termination flags.postconditions
- postconditions for abrupt termination.private Term conditionPostcondition(ProgramVariable flag, Term postcondition)
flag
- an abrupt termination flag.postcondition
- a postcondition for abrupt termination with the specifed flag.private Term buildThrowPostcondition()
private Term buildNormalTerminationCondition()
Behavior.NORMAL_BEHAVIOR
private Term buildBreakTerminationCondition()
Behavior.BREAK_BEHAVIOR
private Term buildContinueTerminationCondition()
Behavior.CONTINUE_BEHAVIOR
private Term buildReturnTerminationCondition()
Behavior.RETURN_BEHAVIOR
private Term buildThrowTerminationCondition()
Behavior.EXCEPTIONAL_BEHAVIOR
private Term buildNormalTerminationCondition(java.util.Map<Label,ProgramVariable> flags)
flags
- a map containing all abrupt termination flags.Behavior.NORMAL_BEHAVIOR
private Term buildAbruptTerminationCondition(java.util.Map<Label,ProgramVariable> flags)
flags
- a map containing all abrupt termination flags.buildNormalTerminationCondition()
private Term buildFlagIsCondition(ProgramVariable flag, Term truth)
flag
- a boolean variable.truth
- a boolean term.private Term buildExceptionIsNullCondition()
variables.exception == null
.private java.util.Map<LocationVariable,Term> buildModifiesClauses()
private ImmutableSet<T> create(java.util.Map<LocationVariable,Term> preconditions, java.util.Map<LocationVariable,Term> postconditions, java.util.Map<LocationVariable,Term> modifiesClauses, ImmutableList<InfFlowSpec> infFlowSpecs)
preconditions
- the contracts' preconditions.postconditions
- the contracts' postconditions.modifiesClauses
- the contracts' modifies clauses.infFlowSpecs
- the contracts' information flow specifications.diverges
clause
is trivial (i.e., true
or false
) or not.protected abstract T 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)
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.private boolean divergesConditionCannotBeExpressedByAModality()
true
iff the diverges condition can be expressed by a modality.private java.util.Map<LocationVariable,Term> addNegatedDivergesConditionToPreconditions(java.util.Map<LocationVariable,Term> preconditions)
preconditions
- a map containing the contract's preconditions.