public abstract class AbstractAuxiliaryContractImpl extends java.lang.Object implements AuxiliaryContract
AuxiliaryContract
.Modifier and Type | Class and Description |
---|---|
protected static class |
AbstractAuxiliaryContractImpl.Combinator<T extends AuxiliaryContract>
This class is used to to combine multiple contracts for the same block and apply them
simultaneously.
|
protected static class |
AbstractAuxiliaryContractImpl.Creator<T extends AuxiliaryContract>
This class contains a builder method for
AbstractAuxiliaryContractImpl s
(AbstractAuxiliaryContractImpl.Creator.create() ). |
private static class |
AbstractAuxiliaryContractImpl.ReplacementMap<S extends Sorted>
A map from some type to the same type.
|
private static class |
AbstractAuxiliaryContractImpl.TermReplacementMap
A replacement map for terms.
|
private static class |
AbstractAuxiliaryContractImpl.VariableReplacementMap
A replacement map for variables.
|
AuxiliaryContract.Terms, AuxiliaryContract.Variables, AuxiliaryContract.VariablesCreator
Modifier and Type | Field and Description |
---|---|
protected java.lang.String |
baseName |
protected StatementBlock |
block |
private ImmutableSet<FunctionalAuxiliaryContract<?>> |
functionalContracts |
protected java.util.Map<LocationVariable,java.lang.Boolean> |
hasMod |
protected ImmutableList<InfFlowSpec> |
infFlowSpecs |
protected Term |
instantiationSelf |
protected java.util.List<Label> |
labels |
protected Term |
measuredBy |
protected IProgramMethod |
method |
protected Modality |
modality |
protected java.util.Map<LocationVariable,Term> |
modifiesClauses |
protected java.util.Map<LocationVariable,Term> |
postconditions |
protected java.util.Map<LocationVariable,Term> |
preconditions |
protected boolean |
transactionApplicable |
protected AuxiliaryContract.Variables |
variables |
Constructor and Description |
---|
AbstractAuxiliaryContractImpl(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,
ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts) |
clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait
getUniqueName, setBlock, setTarget, visit
getDisplayName, getName
protected final StatementBlock block
getBlock()
protected final java.util.List<Label> labels
getLabels()
protected final IProgramMethod method
getMethod()
protected final Modality modality
getModality()
protected Term instantiationSelf
getInstantiationSelfTerm()
protected final java.util.Map<LocationVariable,Term> preconditions
protected final java.util.Map<LocationVariable,Term> postconditions
protected final java.util.Map<LocationVariable,Term> modifiesClauses
protected ImmutableList<InfFlowSpec> infFlowSpecs
getInfFlowSpecs()
protected final AuxiliaryContract.Variables variables
getVariables()
protected final boolean transactionApplicable
isTransactionApplicable()
protected final java.util.Map<LocationVariable,java.lang.Boolean> hasMod
hasModifiesClause(LocationVariable)
protected final java.lang.String baseName
getBaseName()
private ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts
public AbstractAuxiliaryContractImpl(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, ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts)
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.functionalContracts
- the functional contracts corresponding to this contract.public java.lang.String getBaseName()
getBaseName
in interface AuxiliaryContract
public StatementBlock getBlock()
getBlock
in interface AuxiliaryContract
public java.util.List<Label> getLabels()
getLabels
in interface AuxiliaryContract
AuxiliaryContract.getBlock()
public IProgramMethod getMethod()
getMethod
in interface AuxiliaryContract
AuxiliaryContract.getBlock()
public KeYJavaType getKJT()
SpecificationElement
getKJT
in interface SpecificationElement
public Modality getModality()
getModality
in interface AuxiliaryContract
public AuxiliaryContract.Variables getPlaceholderVariables()
AuxiliaryContract
getPlaceholderVariables
in interface AuxiliaryContract
AuxiliaryContractBuilders.VariablesCreatorAndRegistrar
public VisibilityModifier getVisibility()
SpecificationElement
getVisibility
in interface SpecificationElement
public boolean isTransactionApplicable()
isTransactionApplicable
in interface AuxiliaryContract
true
if and only if this contract is applicable for transactions.public boolean isReadOnly(Services services)
isReadOnly
in interface AuxiliaryContract
services
- services.true
if and only if this contract is read-only.public boolean hasModifiesClause(LocationVariable heap)
AuxiliaryContract
true
iff the method (according to the contract) does not modify the heap
at all, i.e., iff it is "strictly pure."hasModifiesClause
in interface AuxiliaryContract
heap
- the heap to use.public AuxiliaryContract.Variables getVariables()
getVariables
in interface AuxiliaryContract
public AuxiliaryContract.Terms getVariablesAsTerms(Services services)
getVariablesAsTerms
in interface AuxiliaryContract
services
- services.public Term getTerm(Term term, AuxiliaryContract.Variables variables, Services services)
term
- a term.variables
- replacements for getVariables()
services
- services.getVariables()
replaced.public Term getTerm(Term term, Term heap, AuxiliaryContract.Terms terms, Services services)
term
- a term.heap
- the replacement heapterms
- replacements for getVariables()
services
- services.getVariables()
replaced.public Term getMby()
getMby
in interface AuxiliaryContract
null
otherwise.public Term getMby(AuxiliaryContract.Variables variables, Services services)
getMby
in interface AuxiliaryContract
variables
- variables to use instead of AuxiliaryContract.getPlaceholderVariables()
.services
- services.null
otherwise.public Term getMby(ProgramVariable selfVar, Services services)
getMby
in interface AuxiliaryContract
selfVar
- the self
variable to use instead of AuxiliaryContract.getPlaceholderVariables()
.services
- services.null
otherwise.public Term getMby(java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
getMby
in interface AuxiliaryContract
heapTerms
- the heaps to use.selfTerm
- the self
variable to use instead of AuxiliaryContract.getPlaceholderVariables()
.atPres
- a map from every variable var
to \old(var)
to use instead of
AuxiliaryContract.getPlaceholderVariables()
.services
- services.null
otherwise.public Term getPrecondition(LocationVariable heap, ProgramVariable self, java.util.Map<LocationVariable,LocationVariable> atPres, Services services)
getPrecondition
in interface AuxiliaryContract
heap
- the heap to use.self
- the self
variable to use instead of AuxiliaryContract.getPlaceholderVariables()
.atPres
- a map from every variable var
to \old(var)
to use instead of
AuxiliaryContract.getPlaceholderVariables()
.services
- services.public Term getPrecondition(LocationVariable heapVariable, Term heap, Term self, java.util.Map<LocationVariable,Term> atPres, Services services)
getPrecondition
in interface AuxiliaryContract
heapVariable
- the heap to use.heap
- the heap to use.self
- the self
variable to use to use instead of
AuxiliaryContract.getPlaceholderVariables()
.atPres
- a map from every variable var
to \old(var)
to use instead of
AuxiliaryContract.getPlaceholderVariables()
.services
- services.public Term getPrecondition(LocationVariable heap, Services services)
getPrecondition
in interface AuxiliaryContract
heap
- the heap to use.services
- services.public Term getPrecondition(LocationVariable heap, AuxiliaryContract.Variables variables, Services services)
getPrecondition
in interface AuxiliaryContract
heap
- the heap to use.variables
- the variables to use instead of AuxiliaryContract.getPlaceholderVariables()
.services
- services.variables
.public Term getPrecondition(LocationVariable heapVariable, Term heap, AuxiliaryContract.Terms terms, Services services)
getPrecondition
in interface AuxiliaryContract
heapVariable
- the heap to use.heap
- the heap to use.terms
- the terms to use instead of AuxiliaryContract.getPlaceholderVariables()
.services
- services.public Term getPostcondition(LocationVariable heap, AuxiliaryContract.Variables variables, Services services)
getPostcondition
in interface AuxiliaryContract
heap
- the heap to use.variables
- the variables to use instead of AuxiliaryContract.getPlaceholderVariables()
.services
- services.public Term getPostcondition(LocationVariable heapVariable, Term heap, AuxiliaryContract.Terms terms, Services services)
getPostcondition
in interface AuxiliaryContract
heapVariable
- the heap to use.heap
- the heap to use.terms
- the terms to use instead of AuxiliaryContract.getPlaceholderVariables()
.services
- services.public Term getPostcondition(LocationVariable heap, Services services)
getPostcondition
in interface AuxiliaryContract
heap
- the heap to use.services
- services.public Term getModifiesClause(LocationVariable heap, ProgramVariable self, Services services)
getModifiesClause
in interface AuxiliaryContract
heap
- the heap to use.self
- the self
variable to use instead of AuxiliaryContract.getPlaceholderVariables()
.services
- services.public Term getModifiesClause(LocationVariable heapVariable, Term heap, Term self, Services services)
getModifiesClause
in interface AuxiliaryContract
heapVariable
- the heap to use.heap
- the heap to use.self
- the self
variable to use instead of AuxiliaryContract.getPlaceholderVariables()
.services
- services.public Term getModifiesClause(LocationVariable heap, AuxiliaryContract.Variables variables, Services services)
getModifiesClause
in interface AuxiliaryContract
heap
- the heap to use.variables
- the variables to use instead of AuxiliaryContract.getPlaceholderVariables()
.services
- services.public Term getModifiesClause(LocationVariable heap, Services services)
getModifiesClause
in interface AuxiliaryContract
heap
- the heap to use.services
- services.public Term getPre(Services services)
getPre
in interface AuxiliaryContract
services
- services.public Term getRequires(LocationVariable heap)
getRequires
in interface AuxiliaryContract
heap
- the heap to use.public Term getPost(Services services)
getPost
in interface AuxiliaryContract
services
- services.public Term getEnsures(LocationVariable heap)
getEnsures
in interface AuxiliaryContract
heap
- the heap to use.public Term getMod(Services services)
getMod
in interface AuxiliaryContract
services
- services.public ImmutableList<InfFlowSpec> getInfFlowSpecs()
getInfFlowSpecs
in interface AuxiliaryContract
public boolean hasMby()
hasMby
in interface AuxiliaryContract
true
if and only if this contract has a measured-by clause.AuxiliaryContract.getMby()
public boolean hasInfFlowSpecs()
hasInfFlowSpecs
in interface AuxiliaryContract
true
if and only if this contract has information flow specs.AuxiliaryContract.getInfFlowSpecs()
public void setInstantiationSelf(Term selfInstantiation)
setInstantiationSelf
in interface AuxiliaryContract
selfInstantiation
- the new instantiation self term.AuxiliaryContract.getInstantiationSelfTerm()
public Term getInstantiationSelfTerm()
getInstantiationSelfTerm
in interface AuxiliaryContract
self
variable as a term.public Term getInstantiationSelfTerm(TermServices services)
getInstantiationSelfTerm
in interface AuxiliaryContract
services
- services.public IProgramMethod getTarget()
getTarget
in interface AuxiliaryContract
public Term getAssignable(LocationVariable heap)
getAssignable
in interface AuxiliaryContract
heap
- the heap to use.public java.lang.String getHtmlText(Services services)
getHtmlText
in interface AuxiliaryContract
services
- services.public java.lang.String getPlainText(Services services)
getPlainText
in interface AuxiliaryContract
services
- services.public java.lang.String getPlainText(Services services, AuxiliaryContract.Terms terms)
getPlainText
in interface AuxiliaryContract
services
- services.terms
- the terms to use instead of AuxiliaryContract.getPlaceholderVariables()
.public Contract.OriginalVariables getOrigVars()
getOrigVars
in interface AuxiliaryContract
OriginalVariables
.AuxiliaryContract.getVariables()
public boolean equals(java.lang.Object obj)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public ImmutableSet<FunctionalAuxiliaryContract<?>> getFunctionalContracts()
getFunctionalContracts
in interface AuxiliaryContract
FunctionalAuxiliaryContract
s with a valid id that correspond to this
BlockSpecificationElement
.
Unless this contract is a combination of other contracts, the resulting set will
only contain one element.public void setFunctionalContract(FunctionalAuxiliaryContract<?> contract)
setFunctionalContract
in interface AuxiliaryContract
contract
- the new functional contract.AuxiliaryContract.getFunctionalContracts()
protected java.util.Map<ProgramVariable,ProgramVariable> createReplacementMap(AuxiliaryContract.Variables newVariables, Services services)
newVariables
- new variables.services
- services.getVariables()
to its counterpart in
newVariables
.protected java.util.Map<Term,Term> createReplacementMap(Term newHeap, AuxiliaryContract.Terms newTerms, Services services)
newHeap
- new base heap.newTerms
- new terms.services
- services.getVariables().termify()
to its counterpart in
newTerms
, and from the base heap to heap
.private java.lang.String getHtmlMods(LocationVariable baseHeap, HeapLDT heapLDT, Services services)
baseHeap
- base heap.heapLDT
- heap LDT.services
- services.private java.lang.String getHtmlPres(LocationVariable baseHeap, HeapLDT heapLDT, Services services)
baseHeap
- base heap.heapLDT
- heap LDT.services
- services.private java.lang.String getHtmlPosts(LocationVariable baseHeap, HeapLDT heapLDT, Services services)
baseHeap
- base heap.heapLDT
- heap LDT.services
- services.private java.lang.String getPlainMods(Term self, LocationVariable baseHeap, HeapLDT heapLDT, Services services)
self
- the self termbaseHeap
- base heap.heapLDT
- heap LDT.services
- services.private java.lang.String getPlainPres(AuxiliaryContract.Terms terms, LocationVariable baseHeap, HeapLDT heapLDT, Services services)
terms
- the terms to use.baseHeap
- base heap.heapLDT
- heap LDT.services
- services.private java.lang.String getPlainPosts(AuxiliaryContract.Terms terms, LocationVariable baseHeap, HeapLDT heapLDT, Services services)
terms
- the terms to use.baseHeap
- base heap.heapLDT
- heap LDT.services
- services.