de.uka.ilkd.key.speclang

Class BlockContractImpl

java.lang.Object

de.uka.ilkd.key.speclang.AbstractAuxiliaryContractImpl

de.uka.ilkd.key.speclang.BlockContractImpl

All Implemented Interfaces:

AuxiliaryContract, BlockContract, SpecificationElement

public final class BlockContractImpl
extends AbstractAuxiliaryContractImpl
implements BlockContract

Default implementation of BlockContract.

Author:

wacker, lanzinger

See Also:

BlockContractImpl.Creator

Nested Class Summary

Nested Classes

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

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 LoopContract	loopContract

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

BlockContractImpl(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, ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts)

Method Summary

Modifier and Type	Method and Description
static BlockContract	combine(ImmutableSet<BlockContract> contracts, Services services)
java.lang.String	getDisplayName() Returns the displayed name.
java.lang.String	getName() Returns the unique internal name of the specification element.
java.lang.String	getUniqueName()
BlockContract	setBlock(StatementBlock newBlock)
void	setFunctionalContract(FunctionalAuxiliaryContract<?> contract)
(package private) void	setLoopContract(LoopContract loopContract)
BlockContract	setTarget(KeYJavaType newKJT, IObserverFunction newPM)
LoopContract	toLoopContract()
java.lang.String	toString()
BlockContract	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)
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

loopContract

private LoopContract loopContract

See Also:

toLoopContract()

Constructor Detail

BlockContractImpl

public BlockContractImpl(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,
                         ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts)

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.

functionalContracts - the functional contracts corresponding to this contract.

Method Detail

combine

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

Parameters:

contracts - a set of block contracts to combine.

services - services.

Returns:

the combination of the specified block contracts.

setLoopContract

void setLoopContract(LoopContract loopContract)

Parameters:

loopContract - the loop contract from which this block contract was created.

See Also:

toLoopContract()

toLoopContract

public LoopContract toLoopContract()

Specified by:

toLoopContract in interface BlockContract

Returns:

the LoopContract from which this contract was generated, or null.

See Also:

LoopContract.toBlockContract()

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

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

Specified by:

update in interface BlockContract

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.

Returns:

a new block contract with the specified attributes.

setBlock

public BlockContract setBlock(StatementBlock newBlock)

Specified by:

setBlock in interface AuxiliaryContract

Specified by:

setBlock in interface BlockContract

Parameters:

newBlock - the new block.

Returns:

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

setTarget

public BlockContract setTarget(KeYJavaType newKJT,
                               IObserverFunction newPM)

Specified by:

setTarget in interface AuxiliaryContract

Specified by:

setTarget in interface BlockContract

Parameters:

newKJT - the type containing the new target method.

newPM - the new target method.

Returns:

a new block 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