de.uka.ilkd.key.speclang

Class LoopContractImpl.Creator

java.lang.Object

de.uka.ilkd.key.logic.TermBuilder

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

de.uka.ilkd.key.speclang.LoopContractImpl.Creator

Enclosing class:

LoopContractImpl

public static class LoopContractImpl.Creator
extends AbstractAuxiliaryContractImpl.Creator<LoopContract>

This class is used to build LoopContractImpls.

See Also:

AbstractAuxiliaryContractImpl.Creator.create()

Field Summary

Fields

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.

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, 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.

Method Summary

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()

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

buildPostconditions, 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

Field Detail

decreases

private Term decreases

See Also:

LoopContract.getDecreases()

loop

private LoopStatement loop

null if this contracts belongs to a block instead of a loop, the loop this contract belongs to otherwise.

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,
               Term decreases,
               Services services)

Creates loop contract for a block that starts with a loop.

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.

decreases - the decreases term.

services - services.

Creator

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)

Creates loop contract for a loop.

Parameters:

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.

Method Detail

build

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)

Specified by:

build in class AbstractAuxiliaryContractImpl.Creator<LoopContract>

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.

buildPreconditions

protected java.util.Map<LocationVariable,Term> buildPreconditions()

Overrides:

buildPreconditions in class AbstractAuxiliaryContractImpl.Creator<LoopContract>

Returns:

the contract's preconditions.