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
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
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> newPostconditions, 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> newPostconditions, 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 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()
.