public interface LoopContract extends AuxiliaryContract
A contract for a block that begins with a loop.
When a loop contract is encountered in an existing proof, a LoopContract
is used. To
generate a new proof obligation for a block contract, use FunctionalLoopContract
instead.
AuxiliaryContract.Terms, AuxiliaryContract.Variables, AuxiliaryContract.VariablesCreator
Modifier and Type | Method and Description |
---|---|
StatementBlock |
getBody() |
Term |
getDecreases() |
Term |
getDecreases(AuxiliaryContract.Variables variables,
Services services) |
Term |
getDecreases(Term heap,
Term self,
Services services) |
Expression |
getGuard() |
StatementBlock |
getHead()
This contains any statements that are executed before the loop.
|
ProgramVariable |
getIndexVariable() |
LoopStatement |
getLoop() |
java.util.List<Label> |
getLoopLabels() |
StatementBlock |
getTail() |
ProgramVariable |
getValuesVariable() |
boolean |
isInternalOnly() |
boolean |
isOnBlock() |
LoopContract |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
LoopContract |
replaceEnhancedForVariables(StatementBlock newBlock,
Services services)
Replaces
\index and \values with the proper variables in all terms of this
contract. |
LoopContract |
setBlock(StatementBlock newBlock) |
LoopContract |
setLoop(LoopStatement newLoop) |
LoopContract |
setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
BlockContract |
toBlockContract()
Returns a
BlockContract for AuxiliaryContract.getBlock() . |
LoopContract |
update(LoopStatement newLoop,
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,
Term newDecreases) |
LoopContract |
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,
Term newDecreases) |
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
Term getDecreases()
Term getDecreases(Term heap, Term self, Services services)
heap
- the heap to use.self
- the self
variable to use instead of AuxiliaryContract.getPlaceholderVariables()
.services
- services.Term getDecreases(AuxiliaryContract.Variables variables, Services services)
variables
- the variables to use instead of AuxiliaryContract.getPlaceholderVariables()
.services
- services.StatementBlock getHead()
This contains any statements that are executed before the loop.
It is only used if the loop is a for loop, in which case it contains the loop initializers
Expression getGuard()
StatementBlock getBody()
StatementBlock getTail()
LoopStatement getLoop()
while(<getGuard()>) { <getBody()> }
java.util.List<Label> getLoopLabels()
boolean isOnBlock()
true
if this contract belongs to a block,
false
if it belongs to a loop.LoopContract 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, Term newDecreases)
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.newDecreases
- the new decreases clause.LoopContract update(LoopStatement newLoop, 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, Term newDecreases)
newLoop
- the new loop.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.newDecreases
- the new decreases clause.ProgramVariable getIndexVariable()
getLoop()
is an enhanced for-loop,
null
otherwise.EnhancedForElimination.getIndexVariable()
ProgramVariable getValuesVariable()
getLoop()
is an enhanced for-loop,
null
otherwise.EnhancedForElimination.getValuesVariable()
LoopContract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
setTarget
in interface AuxiliaryContract
newKJT
- the type containing the new target method.newPM
- the new target method.LoopContract setBlock(StatementBlock newBlock)
setBlock
in interface AuxiliaryContract
newBlock
- the new block.LoopContract 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 setLoop(LoopStatement newLoop)
newLoop
- the new loop.LoopContract replaceEnhancedForVariables(StatementBlock newBlock, Services services)
\index
and \values
with the proper variables in all terms of this
contract.newBlock
- a new block.services
- services.\index
and \values
are replaced by proper variables in all terms.boolean isInternalOnly()
true
iff this contract should only be applied using
LoopContractInternalRule
.BlockContract toBlockContract()
BlockContract
for AuxiliaryContract.getBlock()
.
This is used to apply for-loop and for-each-loops: The block containing the loop is applied
using a block contract; inside that block contract's validity branch, the while-loop
obtained by transforming the for-loop is applied using a loop contract.BlockContract
for AuxiliaryContract.getBlock()
.Copyright © 2003-2019 The KeY-Project.