de.uka.ilkd.key.speclang

Class AbstractAuxiliaryContractImpl.Creator<T extends AuxiliaryContract>

java.lang.Object

de.uka.ilkd.key.logic.TermBuilder

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

Type Parameters:

T - the type of the subclass.

Direct Known Subclasses:

BlockContractImpl.Creator, LoopContractImpl.Creator

Enclosing class:

AbstractAuxiliaryContractImpl

protected abstract static class AbstractAuxiliaryContractImpl.Creator<T extends AuxiliaryContract>
extends TermBuilder

This class contains a builder method for AbstractAuxiliaryContractImpls (create()). It should be overridden in every subclass.

Field Summary

Fields

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

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
private java.util.Map<LocationVariable,Term>	addNegatedDivergesConditionToPreconditions(java.util.Map<LocationVariable,Term> preconditions)
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)
private Term	buildAbruptTerminationCondition(java.util.Map<Label,ProgramVariable> flags)
private Term	buildBreakTerminationCondition()
private Term	buildContinueTerminationCondition()
private Term	buildExceptionIsNullCondition()
private Term	buildFlagIsCondition(ProgramVariable flag, Term truth)
private java.util.Map<LocationVariable,Term>	buildModifiesClauses()
private Term	buildNormalTerminationCondition()
private Term	buildNormalTerminationCondition(java.util.Map<Label,ProgramVariable> flags)
private Term	buildPostcondition(LocationVariable heap)
protected java.util.Map<LocationVariable,Term>	buildPostconditions()
protected java.util.Map<LocationVariable,Term>	buildPreconditions()
private Term	buildReturnTerminationCondition()
private Term	buildThrowPostcondition()
private Term	buildThrowTerminationCondition()
private Term	conditionPostcondition(ProgramVariable flag, Term postcondition)
private Term	conditionPostconditions(java.util.Map<Label,ProgramVariable> flags, java.util.Map<Label,Term> postconditions)
ImmutableSet<T>	create()
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)
private boolean	divergesConditionCannotBeExpressedByAModality()

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

baseName

private final java.lang.String baseName

See Also:

AuxiliaryContract.getBaseName()

block

private final StatementBlock block

See Also:

AuxiliaryContract.getBlock()

labels

private final java.util.List<Label> labels

See Also:

AuxiliaryContract.getLabels()

method

private final IProgramMethod method

See Also:

AuxiliaryContract.getMethod()

behavior

private final Behavior behavior

This contract's behavior.

variables

private final AuxiliaryContract.Variables variables

See Also:

AuxiliaryContract.getVariables()

measuredBy

private final Term measuredBy

See Also:

AuxiliaryContract.getMby()

requires

private final java.util.Map<LocationVariable,Term> requires

See Also:

AuxiliaryContract.getRequires(LocationVariable)

ensures

private final java.util.Map<LocationVariable,Term> ensures

Postcondition for normal termination.

infFlowSpecs

private final ImmutableList<InfFlowSpec> infFlowSpecs

See Also:

AuxiliaryContract.getInfFlowSpecs()

breaks

private final java.util.Map<Label,Term> breaks

Postconditions for abrupt termination with break statements.

continues

private final java.util.Map<Label,Term> continues

Postconditions for abrupt termination with continue statements.

returns

private final Term returns

Postcondition for abrupt termination with return statements.

signals

private final Term signals

Postcondition for abrupt termination due to an uncaught exception.

signalsOnly

private final Term signalsOnly

A term specifying which uncaught exceptions may occur.

diverges

private final Term diverges

A diverges term.

assignables

private final java.util.Map<LocationVariable,Term> assignables

A map from every heap to an assignable term.

heaps

private final ImmutableList<LocationVariable> heaps

A list of heaps used in this contract.

hasMod

private final java.util.Map<LocationVariable,java.lang.Boolean> hasMod

A map specifying on which heaps this contract has a modifies clause.

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

Method Detail

create

public ImmutableSet<T> create()

Returns:

a new contract.

buildPreconditions

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

Returns:

the contract's preconditions.

buildPostconditions

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

Returns:

the contract's postconditions.

buildPostcondition

private Term buildPostcondition(LocationVariable heap)

Parameters:

heap - the heap to use.

Returns:

the contract's postcondition on the specified heap.

conditionPostconditions

private Term conditionPostconditions(java.util.Map<Label,ProgramVariable> flags,
                                     java.util.Map<Label,Term> postconditions)

Parameters:

flags - abrupt termination flags.

postconditions - postconditions for abrupt termination.

Returns:

a postcondition created conjunctively from the specified postconditions.

conditionPostcondition

private Term conditionPostcondition(ProgramVariable flag,
                                    Term postcondition)

Parameters:

flag - an abrupt termination flag.

postcondition - a postcondition for abrupt termination with the specifed flag.

Returns:

a part of the postcondition.

buildThrowPostcondition

private Term buildThrowPostcondition()

Returns:

the postcondition for abrupt termination due to an uncaught exception.

buildNormalTerminationCondition

private Term buildNormalTerminationCondition()

Returns:

a term corresponding to Behavior.NORMAL_BEHAVIOR

buildBreakTerminationCondition

private Term buildBreakTerminationCondition()

Returns:

a term corresponding to Behavior.BREAK_BEHAVIOR

buildContinueTerminationCondition

private Term buildContinueTerminationCondition()

Returns:

a term corresponding to Behavior.CONTINUE_BEHAVIOR

buildReturnTerminationCondition

private Term buildReturnTerminationCondition()

Returns:

a term corresponding to Behavior.RETURN_BEHAVIOR

buildThrowTerminationCondition

private Term buildThrowTerminationCondition()

Returns:

a term corresponding to Behavior.EXCEPTIONAL_BEHAVIOR

buildNormalTerminationCondition

private Term buildNormalTerminationCondition(java.util.Map<Label,ProgramVariable> flags)

Parameters:

flags - a map containing all abrupt termination flags.

Returns:

a term corresponding to Behavior.NORMAL_BEHAVIOR

buildAbruptTerminationCondition

private Term buildAbruptTerminationCondition(java.util.Map<Label,ProgramVariable> flags)

Parameters:

flags - a map containing all abrupt termination flags.

Returns:

a term equivalent to the negation of buildNormalTerminationCondition()

buildFlagIsCondition

private Term buildFlagIsCondition(ProgramVariable flag,
                                  Term truth)

Parameters:

flag - a boolean variable.

truth - a boolean term.

Returns:

a term which is true iff the flag is equal to the term.

buildExceptionIsNullCondition

private Term buildExceptionIsNullCondition()

Returns:

a term which is true iff variables.exception == null.

buildModifiesClauses

private java.util.Map<LocationVariable,Term> buildModifiesClauses()

Returns:

the contract's modifies clauses.

create

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)

Parameters:

preconditions - the contracts' preconditions.

postconditions - the contracts' postconditions.

modifiesClauses - the contracts' modifies clauses.

infFlowSpecs - the contracts' information flow specifications.

Returns:

a set of one or two contracts (depending on whether the diverges clause is trivial (i.e., true or false) or not.

build

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)

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.

divergesConditionCannotBeExpressedByAModality

private boolean divergesConditionCannotBeExpressedByAModality()

Returns:

true iff the diverges condition can be expressed by a modality.

addNegatedDivergesConditionToPreconditions

private java.util.Map<LocationVariable,Term> addNegatedDivergesConditionToPreconditions(java.util.Map<LocationVariable,Term> preconditions)

Parameters:

preconditions - a map containing the contract's preconditions.

Returns:

a map with the negated diverges condition added to every precondition.