de.uka.ilkd.key.speclang

Interface BlockContract

All Superinterfaces:

AuxiliaryContract, SpecificationElement

All Known Implementing Classes:

BlockContractImpl

public interface BlockContract
extends AuxiliaryContract

A block contract.

When a block contract is encountered in an existing proof, a BlockContract is used. To generate a new proof obligation for a block contract, use FunctionalBlockContract instead.

Author:

wacker, lanzinger

Nested Class Summary

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

AuxiliaryContract.Terms, AuxiliaryContract.Variables, AuxiliaryContract.VariablesCreator

Method Summary

Modifier and Type	Method and Description
BlockContract	setBlock(StatementBlock newBlock)
BlockContract	setTarget(KeYJavaType newKJT, IObserverFunction newPM)
LoopContract	toLoopContract()
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)

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, getUniqueName, getVariables, getVariablesAsTerms, hasInfFlowSpecs, hasMby, hasModifiesClause, isReadOnly, isTransactionApplicable, setFunctionalContract, setInstantiationSelf, visit

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

getDisplayName, getKJT, getName, getVisibility

Method Detail

update

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)

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.

setTarget

BlockContract setTarget(KeYJavaType newKJT,
                        IObserverFunction newPM)

Specified by:

setTarget in interface AuxiliaryContract

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.

setBlock

BlockContract setBlock(StatementBlock newBlock)

Specified by:

setBlock in interface AuxiliaryContract

Parameters:

newBlock - the new block.

Returns:

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

toLoopContract

LoopContract toLoopContract()

Returns:

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

See Also:

LoopContract.toBlockContract()