public final class LoopContractImpl extends AbstractAuxiliaryContractImpl implements LoopContract
LoopContract
.LoopContractImpl.Creator
Modifier and Type | Class and Description |
---|---|
protected static class |
LoopContractImpl.Combinator
This class is used to to combine multiple contracts for the same block and apply them
simultaneously.
|
static class |
LoopContractImpl.Creator
This class is used to build
LoopContractImpl s. |
AuxiliaryContract.Terms, AuxiliaryContract.Variables, AuxiliaryContract.VariablesCreator
baseName, block, freePostconditions, freePreconditions, hasMod, infFlowSpecs, instantiationSelf, labels, measuredBy, method, modality, modifiesClauses, postconditions, preconditions, transactionApplicable, variables
Constructor and Description |
---|
LoopContractImpl(java.lang.String baseName,
LoopStatement loop,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a loop.
|
LoopContractImpl(java.lang.String baseName,
StatementBlock block,
java.util.List<Label> labels,
IProgramMethod method,
Modality modality,
java.util.Map<LocationVariable,Term> preconditions,
java.util.Map<LocationVariable,Term> freePreconditions,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
java.util.Map<LocationVariable,Term> freePostconditions,
java.util.Map<LocationVariable,Term> modifiesClauses,
ImmutableList<InfFlowSpec> infFlowSpecs,
AuxiliaryContract.Variables variables,
boolean transactionApplicable,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
Term decreases,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts,
Services services)
Construct a loop contract for a block that starts with a loop.
|
Modifier and Type | Method and Description |
---|---|
static LoopContract |
combine(ImmutableSet<LoopContract> contracts,
Services services) |
StatementBlock |
getBody() |
Term |
getDecreases() |
Term |
getDecreases(AuxiliaryContract.Variables variables,
Services services) |
Term |
getDecreases(Term heap,
Term self,
Services services) |
java.lang.String |
getDisplayName()
Returns the displayed name.
|
Expression |
getGuard() |
StatementBlock |
getHead()
This contains any statements that are executed before the loop.
|
ProgramVariable |
getIndexVariable() |
LoopStatement |
getLoop() |
java.util.List<Label> |
getLoopLabels() |
java.lang.String |
getName()
Returns the unique internal name of the specification element.
|
StatementBlock |
getTail() |
java.lang.String |
getUniqueName() |
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) |
void |
setFunctionalContract(FunctionalAuxiliaryContract<?> contract) |
LoopContract |
setLoop(LoopStatement newLoop) |
LoopContract |
setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
BlockContract |
toBlockContract()
Returns a
BlockContract for AuxiliaryContract.getBlock() . |
java.lang.String |
toString() |
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) |
void |
visit(Visitor visitor)
Accepts a visitor.
|
createReplacementMap, createReplacementMap, equals, getAssignable, getBaseName, getBlock, getEnsures, getEnsuresFree, getFreePost, getFreePostcondition, getFreePostcondition, getFreePostcondition, getFreePre, getFreePrecondition, getFreePrecondition, getFreePrecondition, getFreePrecondition, getFreePrecondition, 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, getRequiresFree, 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, 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, getVariables, getVariablesAsTerms, hasInfFlowSpecs, hasMby, hasModifiesClause, isReadOnly, isTransactionApplicable, setInstantiationSelf
getKJT, getVisibility
public LoopContractImpl(java.lang.String baseName, StatementBlock block, java.util.List<Label> labels, IProgramMethod method, Modality modality, java.util.Map<LocationVariable,Term> preconditions, java.util.Map<LocationVariable,Term> freePreconditions, Term measuredBy, java.util.Map<LocationVariable,Term> postconditions, java.util.Map<LocationVariable,Term> freePostconditions, java.util.Map<LocationVariable,Term> modifiesClauses, ImmutableList<InfFlowSpec> infFlowSpecs, AuxiliaryContract.Variables variables, boolean transactionApplicable, java.util.Map<LocationVariable,java.lang.Boolean> hasMod, Term decreases, ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts, Services services)
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.decreases
- the contract's decreases clause.functionalContracts
- the functional contracts corresponding to this contract.services
- services.public LoopContractImpl(java.lang.String baseName, LoopStatement loop, java.util.List<Label> labels, IProgramMethod method, Modality modality, java.util.Map<LocationVariable,Term> preconditions, java.util.Map<LocationVariable,Term> freePreconditions, Term measuredBy, java.util.Map<LocationVariable,Term> postconditions, java.util.Map<LocationVariable,Term> freePostconditions, java.util.Map<LocationVariable,Term> modifiesClauses, ImmutableList<InfFlowSpec> infFlowSpecs, AuxiliaryContract.Variables variables, boolean transactionApplicable, java.util.Map<LocationVariable,java.lang.Boolean> hasMod, Term decreases, ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts, Services services)
baseName
- the base name.loop
- the loop 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.decreases
- the contract's decreases clause.functionalContracts
- the functional contracts corresponding to this contract.services
- services.public static LoopContract combine(ImmutableSet<LoopContract> contracts, Services services)
contracts
- a set of loop contracts to combine.services
- services.public StatementBlock getHead()
LoopContract
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
getHead
in interface LoopContract
public Expression getGuard()
getGuard
in interface LoopContract
public StatementBlock getBody()
getBody
in interface LoopContract
public StatementBlock getTail()
getTail
in interface LoopContract
public LoopStatement getLoop()
getLoop
in interface LoopContract
while(<getGuard()>) { <getBody()> }
public ProgramVariable getIndexVariable()
getIndexVariable
in interface LoopContract
LoopContract.getLoop()
is an enhanced for-loop,
null
otherwise.EnhancedForElimination.getIndexVariable()
public ProgramVariable getValuesVariable()
getValuesVariable
in interface LoopContract
LoopContract.getLoop()
is an enhanced for-loop,
null
otherwise.EnhancedForElimination.getValuesVariable()
public boolean isOnBlock()
isOnBlock
in interface LoopContract
true
if this contract belongs to a block,
false
if it belongs to a loop.public BlockContract toBlockContract()
LoopContract
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.toBlockContract
in interface LoopContract
BlockContract
for AuxiliaryContract.getBlock()
.public void setFunctionalContract(FunctionalAuxiliaryContract<?> contract)
setFunctionalContract
in interface AuxiliaryContract
setFunctionalContract
in class AbstractAuxiliaryContractImpl
contract
- the new functional contract.AuxiliaryContract.getFunctionalContracts()
public boolean isInternalOnly()
isInternalOnly
in interface LoopContract
true
iff this contract should only be applied using
LoopContractInternalRule
.public java.util.List<Label> getLoopLabels()
getLoopLabels
in interface LoopContract
public Term getDecreases()
getDecreases
in interface LoopContract
public Term getDecreases(Term heap, Term self, Services services)
getDecreases
in interface LoopContract
heap
- the heap to use.self
- the self
variable to use instead of AuxiliaryContract.getPlaceholderVariables()
.services
- services.public Term getDecreases(AuxiliaryContract.Variables variables, Services services)
getDecreases
in interface LoopContract
variables
- the variables to use instead of AuxiliaryContract.getPlaceholderVariables()
.services
- services.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 LoopContract map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
map
in interface AuxiliaryContract
map
in interface LoopContract
map
in interface SpecificationElement
op
- the operator to apply.services
- services.public 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)
update
in interface LoopContract
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.public 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)
update
in interface LoopContract
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.public LoopContract replaceEnhancedForVariables(StatementBlock newBlock, Services services)
LoopContract
\index
and \values
with the proper variables in all terms of this
contract.replaceEnhancedForVariables
in interface LoopContract
newBlock
- a new block.services
- services.\index
and \values
are replaced by proper variables in all terms.public LoopContract setBlock(StatementBlock newBlock)
setBlock
in interface AuxiliaryContract
setBlock
in interface LoopContract
newBlock
- the new block.public LoopContract setLoop(LoopStatement newLoop)
setLoop
in interface LoopContract
newLoop
- the new loop.public LoopContract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
setTarget
in interface AuxiliaryContract
setTarget
in interface LoopContract
newKJT
- the type containing the new target method.newPM
- the new target method.public java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.