de.uka.ilkd.key.speclang

Class BlockContractImpl.Creator

java.lang.Object

de.uka.ilkd.key.logic.TermBuilder

de.uka.ilkd.key.speclang.AbstractAuxiliaryContractImpl.Creator<BlockContract>

de.uka.ilkd.key.speclang.BlockContractImpl.Creator

Enclosing class:

BlockContractImpl

public static class BlockContractImpl.Creator
extends AbstractAuxiliaryContractImpl.Creator<BlockContract>

This class is used to build BlockContractImpls.

See Also:

AbstractAuxiliaryContractImpl.Creator.create()

Field Summary

Fields inherited from class de.uka.ilkd.key.logic.TermBuilder

services, WD_ANY, WD_FORMULA

Constructor Summary

Constructors

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)

Method Summary

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)

Methods inherited from class de.uka.ilkd.key.speclang.AbstractAuxiliaryContractImpl.Creator

buildPostconditions, buildPreconditions, create

Methods inherited from class de.uka.ilkd.key.logic.TermBuilder

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

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Creator

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)

Parameters:

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.

Method Detail

build

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)

Specified by:

build in class AbstractAuxiliaryContractImpl.Creator<BlockContract>

Parameters:

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.

Returns:

an instance of T with the specified attributes.