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.
AuxiliaryContract.Terms, AuxiliaryContract.Variables, AuxiliaryContract.VariablesCreator
Modifier and Type | Method and Description |
---|---|
BlockContract |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
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> newFreePreconditions,
java.util.Map<LocationVariable,Term> newPostconditions,
java.util.Map<LocationVariable,Term> newFreePostconditions,
java.util.Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newInfFlowSpecs,
AuxiliaryContract.Variables newVariables,
Term newMeasuredBy) |
getAssignable, getBaseName, getBlock, getEnsures, getEnsuresFree, getFreePost, getFreePostcondition, getFreePostcondition, getFreePostcondition, getFreePre, getFreePrecondition, getFreePrecondition, getFreePrecondition, getFreePrecondition, getFreePrecondition, 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, getRequiresFree, getTarget, getUniqueName, getVariables, getVariablesAsTerms, hasInfFlowSpecs, hasMby, hasModifiesClause, isReadOnly, isTransactionApplicable, setFunctionalContract, setInstantiationSelf, visit
getDisplayName, getKJT, getName, getVisibility
BlockContract update(StatementBlock newBlock, java.util.Map<LocationVariable,Term> newPreconditions, java.util.Map<LocationVariable,Term> newFreePreconditions, java.util.Map<LocationVariable,Term> newPostconditions, java.util.Map<LocationVariable,Term> newFreePostconditions, java.util.Map<LocationVariable,Term> newModifiesClauses, ImmutableList<InfFlowSpec> newInfFlowSpecs, AuxiliaryContract.Variables newVariables, Term newMeasuredBy)
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.BlockContract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
setTarget
in interface AuxiliaryContract
newKJT
- the type containing the new target method.newPM
- the new target method.BlockContract setBlock(StatementBlock newBlock)
setBlock
in interface AuxiliaryContract
newBlock
- the new block.BlockContract map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
map
in interface AuxiliaryContract
map
in interface SpecificationElement
op
- the operator to apply.services
- services.LoopContract toLoopContract()
LoopContract
from which this contract was generated, or null
.LoopContract.toBlockContract()
Copyright © 2003-2019 The KeY-Project.