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. |
private static class |
LoopContractImpl.ReplaceTypes |
AuxiliaryContract.Terms, AuxiliaryContract.Variables, AuxiliaryContract.VariablesCreator
Modifier and Type | Field and Description |
---|---|
private BlockContract |
blockContract |
private StatementBlock |
body |
private Term |
decreases |
private Expression |
guard |
private StatementBlock |
head |
private ProgramVariable |
index |
private boolean |
internalOnly |
private LoopStatement |
loop |
private java.util.List<Label> |
loopLabels |
private boolean |
onBlock |
private LoopContractImpl |
replacedEnhancedForVars |
private Services |
services
Services.
|
private StatementBlock |
tail |
private ProgramVariable |
values |
baseName, block, 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,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
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,
Term measuredBy,
java.util.Map<LocationVariable,Term> postconditions,
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) |
private static OpReplacer |
createOpReplacer(ProgramVariable index,
ProgramVariable values,
Services services)
Create replacement map for index and values variables.
|
StatementBlock |
getBody() |
private static StatementBlock |
getBodyStatement(LoopStatement loop,
StatementBlock block,
Label outerLabel,
Label innerLabel,
java.util.List<Label> loopLabels,
Services services) |
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.
|
private static StatementBlock |
getHeadStatement(LoopStatement loop,
StatementBlock block,
EnhancedForElimination enhancedForElim) |
ProgramVariable |
getIndexVariable() |
LoopStatement |
getLoop() |
java.util.List<Label> |
getLoopLabels() |
java.lang.String |
getName()
Returns the unique internal name of the specification element.
|
StatementBlock |
getTail() |
private static StatementBlock |
getTailStatement(LoopStatement loop,
StatementBlock block) |
java.lang.String |
getUniqueName() |
ProgramVariable |
getValuesVariable() |
boolean |
isInternalOnly() |
boolean |
isOnBlock() |
LoopContract |
replaceEnhancedForVariables(StatementBlock newBlock,
Services services)
Replaces
\index and \values with the proper variables in all terms of this
contract. |
private static LoopContractImpl |
replaceVariable(LoopContractImpl vars,
ProgramVariable variable,
Services services)
Replace the given variable in the given variable map
|
private static void |
replaceVariable(ProgramVariable var,
AbstractIntegerLiteral init,
java.util.Map<Term,Term> preReplacementMap,
java.util.Map<Term,Term> postReplacementMap,
LoopContractImpl r,
Services services) |
private static void |
replaceVariable(ProgramVariable var,
EmptySeqLiteral init,
java.util.Map<Term,Term> preReplacementMap,
java.util.Map<Term,Term> postReplacementMap,
LoopContractImpl r,
Services services) |
private static void |
replaceVariable(ProgramVariable var,
Expression init,
java.util.Map<Term,Term> preReplacementMap,
java.util.Map<Term,Term> postReplacementMap,
LoopContractImpl r,
Services services) |
private static void |
replaceVariable(ProgramVariable var,
ProgramVariable init,
java.util.Map<Term,Term> preReplacementMap,
java.util.Map<Term,Term> postReplacementMap,
LoopContractImpl r,
Services services) |
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> newPostconditions,
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> newPostconditions,
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, 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, 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, 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, getVariables, getVariablesAsTerms, hasInfFlowSpecs, hasMby, hasModifiesClause, isReadOnly, isTransactionApplicable, setInstantiationSelf
getKJT, getVisibility
private final boolean onBlock
LoopContract.isOnBlock()
private final Term decreases
LoopContract.getDecreases()
private final StatementBlock head
LoopContract.getHead()
private final Expression guard
LoopContract.getGuard()
private final StatementBlock body
LoopContract.getBody()
private final StatementBlock tail
LoopContract.getTail()
private final LoopStatement loop
LoopContract.getLoop()
private final ProgramVariable index
LoopContract.getIndexVariable()
private final ProgramVariable values
LoopContract.getValuesVariable()
private final Services services
private final java.util.List<Label> loopLabels
LoopContract.getLoopLabels()
private boolean internalOnly
LoopContract.isInternalOnly()
private BlockContract blockContract
LoopContract.toBlockContract()
private LoopContractImpl replacedEnhancedForVars
public LoopContractImpl(java.lang.String baseName, StatementBlock block, java.util.List<Label> labels, IProgramMethod method, Modality modality, java.util.Map<LocationVariable,Term> preconditions, Term measuredBy, java.util.Map<LocationVariable,Term> postconditions, 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, Term measuredBy, java.util.Map<LocationVariable,Term> postconditions, 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.private static OpReplacer createOpReplacer(ProgramVariable index, ProgramVariable values, Services services)
index
- the index program variablevalues
- the values program variableservices
- the services objectprivate static LoopContractImpl replaceVariable(LoopContractImpl vars, ProgramVariable variable, Services services)
vars
- the old variablesvariable
- the variable to be replacedservices
- the services objectprivate static StatementBlock getHeadStatement(LoopStatement loop, StatementBlock block, EnhancedForElimination enhancedForElim)
loop
- a loop.block
- the block containing the loop.enhancedForElim
- the transformation used to transform the loop, or null
.null
otherwise.private static StatementBlock getBodyStatement(LoopStatement loop, StatementBlock block, Label outerLabel, Label innerLabel, java.util.List<Label> loopLabels, Services services)
loop
- a loop.block
- the block containing the loop.outerLabel
- the label to use for break statements.innerLabel
- the label to use for continue statements.loopLabels
- all labels belonging to the loop.services
- services.InnerBreakAndContinueReplacer
private static StatementBlock getTailStatement(LoopStatement loop, StatementBlock block)
loop
- a loop.block
- the block containing the loop.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.private static void replaceVariable(ProgramVariable var, ProgramVariable init, java.util.Map<Term,Term> preReplacementMap, java.util.Map<Term,Term> postReplacementMap, LoopContractImpl r, Services services)
private static void replaceVariable(ProgramVariable var, AbstractIntegerLiteral init, java.util.Map<Term,Term> preReplacementMap, java.util.Map<Term,Term> postReplacementMap, LoopContractImpl r, Services services)
private static void replaceVariable(ProgramVariable var, EmptySeqLiteral init, java.util.Map<Term,Term> preReplacementMap, java.util.Map<Term,Term> postReplacementMap, LoopContractImpl r, Services services)
private static void replaceVariable(ProgramVariable var, Expression init, java.util.Map<Term,Term> preReplacementMap, java.util.Map<Term,Term> postReplacementMap, LoopContractImpl r, Services services)
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 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)
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> newPostconditions, 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