public interface AuxiliaryContract extends SpecificationElement
BlockContract
and LoopContract
.Modifier and Type | Interface and Description |
---|---|
static class |
AuxiliaryContract.Terms |
static class |
AuxiliaryContract.Variables
This class contains all new variables that are introduced during a
AuxiliaryContract 's instantiation. |
static class |
AuxiliaryContract.VariablesCreator |
getDisplayName, getKJT, getName, getVisibility
ImmutableSet<FunctionalAuxiliaryContract<?>> getFunctionalContracts()
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.void setFunctionalContract(FunctionalAuxiliaryContract<?> contract)
contract
- the new functional contract.getFunctionalContracts()
StatementBlock getBlock()
java.util.List<Label> getLabels()
getBlock()
IProgramMethod getMethod()
getBlock()
Modality getModality()
AuxiliaryContract.Variables getPlaceholderVariables()
AuxiliaryContractBuilders.VariablesCreatorAndRegistrar
boolean isTransactionApplicable()
true
if and only if this contract is applicable for transactions.boolean isReadOnly(Services services)
services
- services.true
if and only if this contract is read-only.java.lang.String getBaseName()
java.lang.String getUniqueName()
boolean hasModifiesClause(LocationVariable heap)
true
iff the method (according to the contract) does not modify the heap
at all, i.e., iff it is "strictly pure."heap
- the heap to use.Term getInstantiationSelfTerm()
self
variable as a term.Term getPrecondition(LocationVariable heap, Services services)
heap
- the heap to use.services
- services.Term getPrecondition(LocationVariable heap, AuxiliaryContract.Variables variables, Services services)
heap
- the heap to use.variables
- the variables to use instead of getPlaceholderVariables()
.services
- services.variables
.Term getPrecondition(LocationVariable heap, ProgramVariable self, java.util.Map<LocationVariable,LocationVariable> atPres, Services services)
heap
- the heap to use.self
- the self
variable to use instead of getPlaceholderVariables()
.atPres
- a map from every variable var
to \old(var)
to use instead of
getPlaceholderVariables()
.services
- services.Term getPrecondition(LocationVariable heapVariable, Term heap, Term self, java.util.Map<LocationVariable,Term> atPres, Services services)
heapVariable
- the heap to use.heap
- the heap to use.self
- the self
variable to use to use instead of
getPlaceholderVariables()
.atPres
- a map from every variable var
to \old(var)
to use instead of
getPlaceholderVariables()
.services
- services.Term getPrecondition(LocationVariable heapVariable, Term heap, AuxiliaryContract.Terms terms, Services services)
heapVariable
- the heap to use.heap
- the heap to use.terms
- the terms to use instead of getPlaceholderVariables()
.services
- services.Term getPostcondition(LocationVariable heap, AuxiliaryContract.Variables variables, Services services)
heap
- the heap to use.variables
- the variables to use instead of getPlaceholderVariables()
.services
- services.Term getPostcondition(LocationVariable heapVariable, Term heap, AuxiliaryContract.Terms terms, Services services)
heapVariable
- the heap to use.heap
- the heap to use.terms
- the terms to use instead of getPlaceholderVariables()
.services
- services.Term getPostcondition(LocationVariable heap, Services services)
heap
- the heap to use.services
- services.Term getModifiesClause(LocationVariable heap, ProgramVariable self, Services services)
heap
- the heap to use.self
- the self
variable to use instead of getPlaceholderVariables()
.services
- services.Term getModifiesClause(LocationVariable heapVariable, Term heap, Term self, Services services)
heapVariable
- the heap to use.heap
- the heap to use.self
- the self
variable to use instead of getPlaceholderVariables()
.services
- services.Term getModifiesClause(LocationVariable heap, AuxiliaryContract.Variables variables, Services services)
heap
- the heap to use.variables
- the variables to use instead of getPlaceholderVariables()
.services
- services.Term getModifiesClause(LocationVariable heap, Services services)
heap
- the heap to use.services
- services.Term getRequires(LocationVariable heap)
heap
- the heap to use.Term getEnsures(LocationVariable heap)
heap
- the heap to use.Term getAssignable(LocationVariable heap)
heap
- the heap to use.void visit(Visitor visitor)
visitor
- the visitor to accept.java.lang.String getHtmlText(Services services)
services
- services.java.lang.String getPlainText(Services services)
services
- services.java.lang.String getPlainText(Services services, AuxiliaryContract.Terms terms)
services
- services.terms
- the terms to use instead of getPlaceholderVariables()
.IProgramMethod getTarget()
boolean hasMby()
true
if and only if this contract has a measured-by clause.getMby()
Term getMby()
null
otherwise.Term getMby(AuxiliaryContract.Variables variables, Services services)
variables
- variables to use instead of getPlaceholderVariables()
.services
- services.null
otherwise.Term getMby(ProgramVariable selfVar, Services services)
selfVar
- the self
variable to use instead of getPlaceholderVariables()
.services
- services.null
otherwise.Term getMby(java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
heapTerms
- the heaps to use.selfTerm
- the self
variable to use instead of getPlaceholderVariables()
.atPres
- a map from every variable var
to \old(var)
to use instead of
getPlaceholderVariables()
.services
- services.null
otherwise.boolean hasInfFlowSpecs()
true
if and only if this contract has information flow specs.getInfFlowSpecs()
void setInstantiationSelf(Term selfInstantiation)
selfInstantiation
- the new instantiation self term.getInstantiationSelfTerm()
Term getInstantiationSelfTerm(TermServices services)
services
- services.Term getPre(Services services)
services
- services.Term getPost(Services services)
services
- services.Term getMod(Services services)
services
- services.ImmutableList<InfFlowSpec> getInfFlowSpecs()
AuxiliaryContract.Variables getVariables()
AuxiliaryContract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
newKJT
- the type containing the new target method.newPM
- the new target method.AuxiliaryContract setBlock(StatementBlock newBlock)
newBlock
- the new block.AuxiliaryContract.Terms getVariablesAsTerms(Services services)
services
- services.Contract.OriginalVariables getOrigVars()
OriginalVariables
.getVariables()