de.uka.ilkd.key.speclang

Class LoopContractImpl

java.lang.Object

de.uka.ilkd.key.speclang.AbstractAuxiliaryContractImpl

de.uka.ilkd.key.speclang.LoopContractImpl

All Implemented Interfaces:

AuxiliaryContract, LoopContract, SpecificationElement

public final class LoopContractImpl
extends AbstractAuxiliaryContractImpl
implements LoopContract

Default implementation for LoopContract.

Author:

lanzinger

See Also:

LoopContractImpl.Creator

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected static class	LoopContractImpl.Combinator This class is used to to combine multiple contracts for the same block and apply them simultaneously.
static class	LoopContractImpl.Creator This class is used to build LoopContractImpls.
private static class	LoopContractImpl.ReplaceTypes

Nested classes/interfaces inherited from interface de.uka.ilkd.key.speclang.AuxiliaryContract

AuxiliaryContract.Terms, AuxiliaryContract.Variables, AuxiliaryContract.VariablesCreator

Field Summary

Fields

Modifier and Type	Field and Description
private BlockContract	blockContract
private StatementBlock	body
private Term	decreases
private Expression	guard
private StatementBlock	head
private ProgramVariable	index
private boolean	internalOnly
private LoopStatement	loop
private java.util.List<Label>	loopLabels
private boolean	onBlock
private LoopContractImpl	replacedEnhancedForVars
private Services	services Services.
private StatementBlock	tail
private ProgramVariable	values

Fields inherited from class de.uka.ilkd.key.speclang.AbstractAuxiliaryContractImpl

baseName, block, hasMod, infFlowSpecs, instantiationSelf, labels, measuredBy, method, modality, modifiesClauses, postconditions, preconditions, transactionApplicable, variables

Constructor Summary

Constructors

Constructor and Description
LoopContractImpl(java.lang.String baseName, LoopStatement loop, 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, Term decreases, ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts, Services services) Construct a loop contract for a loop.
LoopContractImpl(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, Term decreases, ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts, Services services) Construct a loop contract for a block that starts with a loop.

Method Summary

Modifier and Type	Method and Description
static LoopContract	combine(ImmutableSet<LoopContract> contracts, Services services)
private static OpReplacer	createOpReplacer(ProgramVariable index, ProgramVariable values, Services services) Create replacement map for index and values variables.
StatementBlock	getBody()
private static StatementBlock	getBodyStatement(LoopStatement loop, StatementBlock block, Label outerLabel, Label innerLabel, java.util.List<Label> loopLabels, Services services)
Term	getDecreases()
Term	getDecreases(AuxiliaryContract.Variables variables, Services services)
Term	getDecreases(Term heap, Term self, Services services)
java.lang.String	getDisplayName() Returns the displayed name.
Expression	getGuard()
StatementBlock	getHead() This contains any statements that are executed before the loop.
private static StatementBlock	getHeadStatement(LoopStatement loop, StatementBlock block, EnhancedForElimination enhancedForElim)
ProgramVariable	getIndexVariable()
LoopStatement	getLoop()
java.util.List<Label>	getLoopLabels()
java.lang.String	getName() Returns the unique internal name of the specification element.
StatementBlock	getTail()
private static StatementBlock	getTailStatement(LoopStatement loop, StatementBlock block)
java.lang.String	getUniqueName()
ProgramVariable	getValuesVariable()
boolean	isInternalOnly()
boolean	isOnBlock()
LoopContract	replaceEnhancedForVariables(StatementBlock newBlock, Services services) Replaces \index and \values with the proper variables in all terms of this contract.
private static LoopContractImpl	replaceVariable(LoopContractImpl vars, ProgramVariable variable, Services services) Replace the given variable in the given variable map
private static void	replaceVariable(ProgramVariable var, AbstractIntegerLiteral init, java.util.Map<Term,Term> preReplacementMap, java.util.Map<Term,Term> postReplacementMap, LoopContractImpl r, Services services)
private static void	replaceVariable(ProgramVariable var, EmptySeqLiteral init, java.util.Map<Term,Term> preReplacementMap, java.util.Map<Term,Term> postReplacementMap, LoopContractImpl r, Services services)
private static void	replaceVariable(ProgramVariable var, Expression init, java.util.Map<Term,Term> preReplacementMap, java.util.Map<Term,Term> postReplacementMap, LoopContractImpl r, Services services)
private static void	replaceVariable(ProgramVariable var, ProgramVariable init, java.util.Map<Term,Term> preReplacementMap, java.util.Map<Term,Term> postReplacementMap, LoopContractImpl r, Services services)
LoopContract	setBlock(StatementBlock newBlock)
void	setFunctionalContract(FunctionalAuxiliaryContract<?> contract)
LoopContract	setLoop(LoopStatement newLoop)
LoopContract	setTarget(KeYJavaType newKJT, IObserverFunction newPM)
BlockContract	toBlockContract() Returns a BlockContract for AuxiliaryContract.getBlock().
java.lang.String	toString()
LoopContract	update(LoopStatement newLoop, java.util.Map<LocationVariable,Term> newPreconditions, java.util.Map<LocationVariable,Term> newPostconditions, java.util.Map<LocationVariable,Term> newModifiesClauses, ImmutableList<InfFlowSpec> newinfFlowSpecs, AuxiliaryContract.Variables newVariables, Term newMeasuredBy, Term newDecreases)
LoopContract	update(StatementBlock newBlock, java.util.Map<LocationVariable,Term> newPreconditions, java.util.Map<LocationVariable,Term> newPostconditions, java.util.Map<LocationVariable,Term> newModifiesClauses, ImmutableList<InfFlowSpec> newinfFlowSpecs, AuxiliaryContract.Variables newVariables, Term newMeasuredBy, Term newDecreases)
void	visit(Visitor visitor) Accepts a visitor.

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

createReplacementMap, createReplacementMap, equals, getAssignable, getBaseName, getBlock, getEnsures, getFunctionalContracts, getHtmlText, getInfFlowSpecs, getInstantiationSelfTerm, getInstantiationSelfTerm, getKJT, getLabels, getMby, getMby, getMby, getMby, getMethod, getMod, getModality, getModifiesClause, getModifiesClause, getModifiesClause, getModifiesClause, getOrigVars, getPlaceholderVariables, getPlainText, getPlainText, getPost, getPostcondition, getPostcondition, getPostcondition, getPre, getPrecondition, getPrecondition, getPrecondition, getPrecondition, getPrecondition, getRequires, getTarget, getTerm, getTerm, getVariables, getVariablesAsTerms, getVisibility, hashCode, hasInfFlowSpecs, hasMby, hasModifiesClause, isReadOnly, isTransactionApplicable, setInstantiationSelf

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.speclang.AuxiliaryContract

getAssignable, getBaseName, getBlock, getEnsures, getFunctionalContracts, getHtmlText, getInfFlowSpecs, getInstantiationSelfTerm, getInstantiationSelfTerm, getLabels, getMby, getMby, getMby, getMby, getMethod, getMod, getModality, getModifiesClause, getModifiesClause, getModifiesClause, getModifiesClause, getOrigVars, getPlaceholderVariables, getPlainText, getPlainText, getPost, getPostcondition, getPostcondition, getPostcondition, getPre, getPrecondition, getPrecondition, getPrecondition, getPrecondition, getPrecondition, getRequires, getTarget, getVariables, getVariablesAsTerms, hasInfFlowSpecs, hasMby, hasModifiesClause, isReadOnly, isTransactionApplicable, setInstantiationSelf

Methods inherited from interface de.uka.ilkd.key.speclang.SpecificationElement

getKJT, getVisibility

Field Detail

onBlock

private final boolean onBlock

See Also:

LoopContract.isOnBlock()

decreases

private final Term decreases

See Also:

LoopContract.getDecreases()

head

private final StatementBlock head

See Also:

LoopContract.getHead()

guard

private final Expression guard

See Also:

LoopContract.getGuard()

body

private final StatementBlock body

See Also:

LoopContract.getBody()

tail

private final StatementBlock tail

See Also:

LoopContract.getTail()

loop

private final LoopStatement loop

See Also:

LoopContract.getLoop()

index

private final ProgramVariable index

See Also:

LoopContract.getIndexVariable()

values

private final ProgramVariable values

See Also:

LoopContract.getValuesVariable()

services

private final Services services

Services.

loopLabels

private final java.util.List<Label> loopLabels

See Also:

LoopContract.getLoopLabels()

internalOnly

private boolean internalOnly

See Also:

LoopContract.isInternalOnly()

blockContract

private BlockContract blockContract

See Also:

LoopContract.toBlockContract()

replacedEnhancedForVars

private LoopContractImpl replacedEnhancedForVars

See Also:

LoopContract.replaceEnhancedForVariables(StatementBlock, Services)

Constructor Detail

LoopContractImpl

public LoopContractImpl(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,
                        Term decreases,
                        ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
                        Services services)

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

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.

decreases - the contract's decreases clause.

functionalContracts - the functional contracts corresponding to this contract.

services - services.

LoopContractImpl

public LoopContractImpl(java.lang.String baseName,
                        LoopStatement loop,
                        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,
                        Term decreases,
                        ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
                        Services services)

Construct a loop contract for a loop.

Parameters:

baseName - the base name.

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

decreases - the contract's decreases clause.

functionalContracts - the functional contracts corresponding to this contract.

services - services.

Method Detail

combine

public static LoopContract combine(ImmutableSet<LoopContract> contracts,
                                   Services services)

Parameters:

contracts - a set of loop contracts to combine.

services - services.

Returns:

the combination of the specified loop contracts.

createOpReplacer

private static OpReplacer createOpReplacer(ProgramVariable index,
                                           ProgramVariable values,
                                           Services services)

Create replacement map for index and values variables.

Parameters:

index - the index program variable

values - the values program variable

services - the services object

Returns:

the new according op replacer

replaceVariable

private static LoopContractImpl replaceVariable(LoopContractImpl vars,
                                                ProgramVariable variable,
                                                Services services)

Replace the given variable in the given variable map

Parameters:

vars - the old variables

variable - the variable to be replaced

services - the services object

Returns:

the new variables

getHeadStatement

private static StatementBlock getHeadStatement(LoopStatement loop,
                                               StatementBlock block,
                                               EnhancedForElimination enhancedForElim)

Parameters:

loop - a loop.

block - the block containing the loop.

enhancedForElim - the transformation used to transform the loop, or null.

Returns:

the initializers if the loop is a for-loop, null otherwise.

getBodyStatement

private static StatementBlock getBodyStatement(LoopStatement loop,
                                               StatementBlock block,
                                               Label outerLabel,
                                               Label innerLabel,
                                               java.util.List<Label> loopLabels,
                                               Services services)

Parameters:

loop - a loop.

block - the block containing the loop.

outerLabel - the label to use for break statements.

innerLabel - the label to use for continue statements.

loopLabels - all labels belonging to the loop.

services - services.

Returns:

the loop's body. If the loop is a for-loop, it is transformed to a while-loop.

See Also:

InnerBreakAndContinueReplacer

getTailStatement

private static StatementBlock getTailStatement(LoopStatement loop,
                                               StatementBlock block)

Parameters:

loop - a loop.

block - the block containing the loop.

Returns:

all statements in the block after the loop.

getHead

public StatementBlock getHead()

Description copied from interface: LoopContract

This contains any statements that are executed before the loop.

It is only used if the loop is a for loop, in which case it contains the loop initializers

Specified by:

getHead in interface LoopContract

Returns:

statements to execute before the loop.

getGuard

public Expression getGuard()

Specified by:

getGuard in interface LoopContract

Returns:

the loop guard.

getBody

public StatementBlock getBody()

Specified by:

getBody in interface LoopContract

Returns:

the loop body.

getTail

public StatementBlock getTail()

Specified by:

getTail in interface LoopContract

Returns:

all statements after the loop.

getLoop

public LoopStatement getLoop()

Specified by:

getLoop in interface LoopContract

Returns:

a loop of the form while(<getGuard()>) { <getBody()> }

getIndexVariable

public ProgramVariable getIndexVariable()

Specified by:

getIndexVariable in interface LoopContract

Returns:

the index variable if LoopContract.getLoop() is an enhanced for-loop, null otherwise.

See Also:

EnhancedForElimination.getIndexVariable()

getValuesVariable

public ProgramVariable getValuesVariable()

Specified by:

getValuesVariable in interface LoopContract

Returns:

the values variable if LoopContract.getLoop() is an enhanced for-loop, null otherwise.

See Also:

EnhancedForElimination.getValuesVariable()

isOnBlock

public boolean isOnBlock()

Specified by:

isOnBlock in interface LoopContract

Returns:

true if this contract belongs to a block, false if it belongs to a loop.

replaceVariable

private static void replaceVariable(ProgramVariable var,
                                    ProgramVariable init,
                                    java.util.Map<Term,Term> preReplacementMap,
                                    java.util.Map<Term,Term> postReplacementMap,
                                    LoopContractImpl r,
                                    Services services)

replaceVariable

private static void replaceVariable(ProgramVariable var,
                                    AbstractIntegerLiteral init,
                                    java.util.Map<Term,Term> preReplacementMap,
                                    java.util.Map<Term,Term> postReplacementMap,
                                    LoopContractImpl r,
                                    Services services)

replaceVariable

private static void replaceVariable(ProgramVariable var,
                                    EmptySeqLiteral init,
                                    java.util.Map<Term,Term> preReplacementMap,
                                    java.util.Map<Term,Term> postReplacementMap,
                                    LoopContractImpl r,
                                    Services services)

replaceVariable

private static void replaceVariable(ProgramVariable var,
                                    Expression init,
                                    java.util.Map<Term,Term> preReplacementMap,
                                    java.util.Map<Term,Term> postReplacementMap,
                                    LoopContractImpl r,
                                    Services services)

toBlockContract

public BlockContract toBlockContract()

Description copied from interface: LoopContract

Returns a BlockContract for AuxiliaryContract.getBlock(). This is used to apply for-loop and for-each-loops: The block containing the loop is applied using a block contract; inside that block contract's validity branch, the while-loop obtained by transforming the for-loop is applied using a loop contract.

Specified by:

toBlockContract in interface LoopContract

Returns:

a valid BlockContract for AuxiliaryContract.getBlock().

setFunctionalContract

public void setFunctionalContract(FunctionalAuxiliaryContract<?> contract)

Specified by:

setFunctionalContract in interface AuxiliaryContract

Overrides:

setFunctionalContract in class AbstractAuxiliaryContractImpl

Parameters:

contract - the new functional contract.

See Also:

AuxiliaryContract.getFunctionalContracts()

isInternalOnly

public boolean isInternalOnly()

Specified by:

isInternalOnly in interface LoopContract

Returns:

true iff this contract should only be applied using LoopContractInternalRule.

getLoopLabels

public java.util.List<Label> getLoopLabels()

Specified by:

getLoopLabels in interface LoopContract

Returns:

all labels that belong to the loop, or an empty list if the loop is not a labeled statement.

getDecreases

public Term getDecreases()

Specified by:

getDecreases in interface LoopContract

Returns:

this loop contract's decreases clause.

getDecreases

public Term getDecreases(Term heap,
                         Term self,
                         Services services)

Specified by:

getDecreases in interface LoopContract

Parameters:

heap - the heap to use.

self - the self variable to use instead of AuxiliaryContract.getPlaceholderVariables().

services - services.

Returns:

this loop contract's decreases clause on the specified heap.

getDecreases

public Term getDecreases(AuxiliaryContract.Variables variables,
                         Services services)

Specified by:

getDecreases in interface LoopContract

Parameters:

variables - the variables to use instead of AuxiliaryContract.getPlaceholderVariables().

services - services.

Returns:

this loop contract's decreases clause.

visit

public void visit(Visitor visitor)

Description copied from interface: AuxiliaryContract

Accepts a visitor.

Specified by:

visit in interface AuxiliaryContract

Parameters:

visitor - the visitor to accept.

getName

public java.lang.String getName()

Description copied from interface: SpecificationElement

Returns the unique internal name of the specification element.

Specified by:

getName in interface SpecificationElement

getUniqueName

public java.lang.String getUniqueName()

Specified by:

getUniqueName in interface AuxiliaryContract

Returns:

this contract's unique name.

getDisplayName

public java.lang.String getDisplayName()

Description copied from interface: SpecificationElement

Returns the displayed name.

Specified by:

getDisplayName in interface SpecificationElement

update

public LoopContract update(StatementBlock newBlock,
                           java.util.Map<LocationVariable,Term> newPreconditions,
                           java.util.Map<LocationVariable,Term> newPostconditions,
                           java.util.Map<LocationVariable,Term> newModifiesClauses,
                           ImmutableList<InfFlowSpec> newinfFlowSpecs,
                           AuxiliaryContract.Variables newVariables,
                           Term newMeasuredBy,
                           Term newDecreases)

Specified by:

update in interface LoopContract

Parameters:

newBlock - the new block.

newPreconditions - the new preconditions.

newPostconditions - the new postconditions.

newModifiesClauses - the new modifies clauses.

newinfFlowSpecs - the new information flow specifications.

newVariables - the new variables.

newMeasuredBy - the new measured-by clause.

newDecreases - the new decreases clause.

Returns:

a new loop contract with the specified attributes.

update

public LoopContract update(LoopStatement newLoop,
                           java.util.Map<LocationVariable,Term> newPreconditions,
                           java.util.Map<LocationVariable,Term> newPostconditions,
                           java.util.Map<LocationVariable,Term> newModifiesClauses,
                           ImmutableList<InfFlowSpec> newinfFlowSpecs,
                           AuxiliaryContract.Variables newVariables,
                           Term newMeasuredBy,
                           Term newDecreases)

Specified by:

update in interface LoopContract

Parameters:

newLoop - the new loop.

newPreconditions - the new preconditions.

newPostconditions - the new postconditions.

newModifiesClauses - the new modifies clauses.

newinfFlowSpecs - the new information flow specifications.

newVariables - the new variables.

newMeasuredBy - the new measured-by clause.

newDecreases - the new decreases clause.

Returns:

a new loop contract with the specified attributes.

replaceEnhancedForVariables

public LoopContract replaceEnhancedForVariables(StatementBlock newBlock,
                                                Services services)

Description copied from interface: LoopContract

Replaces \index and \values with the proper variables in all terms of this contract.

Specified by:

replaceEnhancedForVariables in interface LoopContract

Parameters:

newBlock - a new block.

services - services.

Returns:

a new loop contract equal to this one except that it belongs to the new block, and \index and \values are replaced by proper variables in all terms.

setBlock

public LoopContract setBlock(StatementBlock newBlock)

Specified by:

setBlock in interface AuxiliaryContract

Specified by:

setBlock in interface LoopContract

Parameters:

newBlock - the new block.

Returns:

a new loop contract equal to this one except that it belongs to a different block.

setLoop

public LoopContract setLoop(LoopStatement newLoop)

Specified by:

setLoop in interface LoopContract

Parameters:

newLoop - the new loop.

Returns:

a new loop contract equal to this one except that it belongs to a different loop.

setTarget

public LoopContract setTarget(KeYJavaType newKJT,
                              IObserverFunction newPM)

Specified by:

setTarget in interface AuxiliaryContract

Specified by:

setTarget in interface LoopContract

Parameters:

newKJT - the type containing the new target method.

newPM - the new target method.

Returns:

a new loop contract equal to this one except that it belongs to a different target.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object