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 |
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) |
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
getDisplayName, getKJT, getName, getVisibility
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)
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.LoopContract toLoopContract()
LoopContract
from which this contract was generated, or null
.LoopContract.toBlockContract()