public final class BlockContractImpl extends AbstractAuxiliaryContractImpl implements BlockContract
BlockContract
.BlockContractImpl.Creator
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
BlockContractImpl s. |
AuxiliaryContract.Terms, AuxiliaryContract.Variables, AuxiliaryContract.VariablesCreator
Modifier and Type | Field and Description |
---|---|
private LoopContract |
loopContract |
baseName, block, hasMod, infFlowSpecs, instantiationSelf, labels, measuredBy, method, modality, modifiesClauses, postconditions, preconditions, transactionApplicable, variables
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) |
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.
|
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
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
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
getKJT, getVisibility
private LoopContract loopContract
toLoopContract()
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)
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.public static BlockContract combine(ImmutableSet<BlockContract> contracts, Services services)
contracts
- a set of block contracts to combine.services
- services.void setLoopContract(LoopContract loopContract)
loopContract
- the loop contract from which this block contract was created.toLoopContract()
public LoopContract toLoopContract()
toLoopContract
in interface BlockContract
LoopContract
from which this contract was generated, or null
.LoopContract.toBlockContract()
public void setFunctionalContract(FunctionalAuxiliaryContract<?> contract)
setFunctionalContract
in interface AuxiliaryContract
setFunctionalContract
in class AbstractAuxiliaryContractImpl
contract
- the new functional contract.AuxiliaryContract.getFunctionalContracts()
public void visit(Visitor visitor)
AuxiliaryContract
visit
in interface AuxiliaryContract
visitor
- the visitor to accept.public java.lang.String getName()
SpecificationElement
getName
in interface SpecificationElement
public java.lang.String getUniqueName()
getUniqueName
in interface AuxiliaryContract
public java.lang.String getDisplayName()
SpecificationElement
getDisplayName
in interface SpecificationElement
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)
update
in interface BlockContract
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.public BlockContract setBlock(StatementBlock newBlock)
setBlock
in interface AuxiliaryContract
setBlock
in interface BlockContract
newBlock
- the new block.public BlockContract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
setTarget
in interface AuxiliaryContract
setTarget
in interface BlockContract
newKJT
- the type containing the new target method.newPM
- the new target method.public java.lang.String toString()
toString
in class java.lang.Object