public class FunctionalOperationContractImpl extends java.lang.Object implements FunctionalOperationContract
Contract.OriginalVariables
INVALID_ID
Modifier and Type | Method and Description |
---|---|
ContractPO |
createProofObl(InitConfig initConfig)
Returns a proof obligation to the passed initConfig.
|
ProofOblInput |
createProofObl(InitConfig initConfig,
Contract contract)
Returns a proof obligation to the passed contract and initConfig.
|
ProofOblInput |
createProofObl(InitConfig initConfig,
Contract contract,
boolean addSymbolicExecutionLabel)
Returns a proof obligation to the passed contract and initConfig.
|
Term |
getAccessible(ProgramVariable heap) |
Term |
getAnyMod(Term mod,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
Term |
getAssignable(LocationVariable heap) |
java.lang.String |
getBaseName() |
Term |
getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the dependency set of the contract.
|
Term |
getDep(LocationVariable heap,
boolean atPre,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the dependency set of the contract.
|
java.lang.String |
getDisplayName()
Returns the displayed name.
|
Term |
getEnsures(LocationVariable heap) |
Term |
getExc() |
Term |
getFreePost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
getFreePost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getFreePost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
getFreePre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getFreePre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getFreePre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
getGlobalDefs() |
Term |
getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
java.lang.String |
getHTMLText(Services services)
Returns the contract in pretty HTML format.
|
KeYJavaType |
getKJT()
Returns the KeYJavaType representing the class/interface to which the
specification element belongs.
|
Term |
getMby() |
Term |
getMby(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the measured_by clause of the contract.
|
Term |
getMby(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Returns the measured_by clause of the contract.
|
Term |
getMod() |
Term |
getMod(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Returns the modifies clause of the contract.
|
Term |
getMod(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services)
Returns the modifies clause of the contract.
|
Modality |
getModality()
Returns the modality of the contract.
|
java.lang.String |
getName()
Returns the unique internal name of the specification element.
|
Contract.OriginalVariables |
getOrigVars()
Returns the original ProgramVariables to replace them easier.
|
ImmutableList<Term> |
getParams() |
java.lang.String |
getPlainText(Services services)
Returns the contract in pretty plain text format.
|
Term |
getPost() |
Term |
getPost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
getPost(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getPost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the postcondition of the contract.
|
Term |
getPost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the postcondition of the contract.
|
Term |
getPre() |
Term |
getPre(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the precondition of the contract.
|
Term |
getPre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the precondition of the contract.
|
Term |
getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the precondition of the contract.
|
Term |
getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the precondition of the contract.
|
ProofOblInput |
getProofObl(Services services)
Lookup the proof obligation belonging to the contract in the specification repository.
|
protected java.util.Map<Term,Term> |
getReplaceMap(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services)
Deprecated.
|
protected java.util.Map<Term,Term> |
getReplaceMap(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
Term atPre,
Services services)
Deprecated.
|
protected java.util.Map<Term,Term> |
getReplaceMap(java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Get the according replace map for the given variable terms.
|
protected java.util.Map<ProgramVariable,ProgramVariable> |
getReplaceMap(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Get the according replace map for the given variables.
|
Term |
getRepresentsAxiom(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the model method definition for model method contracts
|
Term |
getRepresentsAxiom(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
getRequires(LocationVariable heap) |
Term |
getResult() |
Term |
getSelf() |
KeYJavaType |
getSpecifiedIn() |
IProgramMethod |
getTarget()
Returns the contracted function symbol.
|
static java.lang.String |
getText(FunctionalOperationContract contract,
ImmutableList<Term> contractParams,
Term resultTerm,
Term contractSelf,
Term excTerm,
LocationVariable baseHeap,
Term baseHeapTerm,
java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> atPres,
boolean includeHtmlMarkup,
Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
java.lang.String |
getTypeName()
Returns technical name for the contract type.
|
VisibilityModifier |
getVisibility()
Returns the visibility of the invariant (null for default visibility)
|
boolean |
hasMby()
Tells whether the contract contains a measured_by clause.
|
boolean |
hasModifiesClause(LocationVariable heap)
Returns
true iff the method (according to the contract) does
not modify the heap at all, i.e., iff it is "strictly pure." |
boolean |
hasResultVar() |
boolean |
hasSelfVar()
Checks if a self variable is originally provided.
|
int |
id()
Returns the id number of the contract.
|
boolean |
isReadOnlyContract(Services services) |
FunctionalOperationContract |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
java.lang.String |
proofToString(Services services)
Returns a parseable String representation of the contract.
|
FunctionalOperationContract |
setID(int newId)
Returns a contract which is identical this contract except that the id is set to the new id.
|
Contract |
setTarget(KeYJavaType newKJT,
IObserverFunction newPM)
Returns a contract which is identical to this contract except that the KeYJavaType and
IObserverFunction are set to the new values.
|
boolean |
toBeSaved()
Tells whether, on saving a proof where this contract is available, the contract should be
saved too.
|
java.lang.String |
toString() |
boolean |
transactionApplicableContract() |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
isAuxiliary
public FunctionalOperationContract map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
map
in interface Contract
map
in interface FunctionalOperationContract
map
in interface OperationContract
map
in interface SpecificationElement
op
- the operator to apply.services
- services.protected java.util.Map<ProgramVariable,ProgramVariable> getReplaceMap(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
selfVar
- the self variableparamVars
- the parameter variablesresultVar
- the result variableexcVar
- the exception variableatPreVars
- a map of pre-heaps to their variablesservices
- the services object@Deprecated protected java.util.Map<Term,Term> getReplaceMap(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
@Deprecated protected java.util.Map<Term,Term> getReplaceMap(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, Term atPre, Services services)
protected java.util.Map<Term,Term> getReplaceMap(java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
heapTerms
- the heap termsselfTerm
- the self termparamTerms
- the parameter termsresultTerm
- the result termexcTerm
- the exception variable termatPres
- a map of pre-heaps to their variable termsservices
- the services objectpublic java.lang.String getName()
SpecificationElement
getName
in interface SpecificationElement
public int id()
Contract
public KeYJavaType getKJT()
SpecificationElement
getKJT
in interface SpecificationElement
public IProgramMethod getTarget()
Contract
getTarget
in interface Contract
getTarget
in interface OperationContract
public boolean hasMby()
Contract
public Term getPre(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Contract
public Term getPre(java.util.List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Contract
public Term getPre(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)
Contract
public Term getPre(java.util.List<LocationVariable> heapContext, java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)
Contract
public Term getFreePre(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
getFreePre
in interface OperationContract
public Term getFreePre(java.util.List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
getFreePre
in interface OperationContract
public Term getFreePre(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)
getFreePre
in interface OperationContract
public Term getRequires(LocationVariable heap)
getRequires
in interface Contract
public Term getEnsures(LocationVariable heap)
getEnsures
in interface FunctionalOperationContract
public Term getAssignable(LocationVariable heap)
getAssignable
in interface Contract
public Term getAccessible(ProgramVariable heap)
getAccessible
in interface Contract
public Term getMby(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
Contract
public Term getMby(java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)
Contract
public java.lang.String getPlainText(Services services)
Contract
getPlainText
in interface Contract
services
- services instancepublic java.lang.String getHTMLText(Services services)
Contract
getHTMLText
in interface Contract
services
- services instancepublic static java.lang.String getText(FunctionalOperationContract contract, ImmutableList<Term> contractParams, Term resultTerm, Term contractSelf, Term excTerm, LocationVariable baseHeap, Term baseHeapTerm, java.util.List<LocationVariable> heapContext, java.util.Map<LocationVariable,Term> atPres, boolean includeHtmlMarkup, Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols)
public boolean toBeSaved()
Contract
public java.lang.String proofToString(Services services)
Contract
proofToString
in interface Contract
services
- the services instancepublic Modality getModality()
FunctionalOperationContract
getModality
in interface FunctionalOperationContract
public Term getPost(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
FunctionalOperationContract
getPost
in interface FunctionalOperationContract
heap
- the heap variable.selfVar
- the self variable.paramVars
- the list of parameter variables.resultVar
- the result variable.excVar
- the exception variable.atPreVars
- the map of old variables.services
- the services object.public Term getPost(java.util.List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
getPost
in interface FunctionalOperationContract
public Term getPost(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
FunctionalOperationContract
getPost
in interface FunctionalOperationContract
heap
- the heap variable.heapTerm
- the heap variable term.selfTerm
- the self variable term.paramTerms
- the list of parameter variable terms.resultTerm
- the result variable term.excTerm
- the exception variable term.atPres
- the map of old variable terms.services
- the services object.public Term getPost(java.util.List<LocationVariable> heapContext, java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
getPost
in interface FunctionalOperationContract
public Term getFreePost(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
getFreePost
in interface FunctionalOperationContract
public Term getFreePost(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
getFreePost
in interface FunctionalOperationContract
public Term getFreePost(java.util.List<LocationVariable> heapContext, java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
getFreePost
in interface FunctionalOperationContract
public Term getRepresentsAxiom(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
FunctionalOperationContract
getRepresentsAxiom
in interface FunctionalOperationContract
public Term getRepresentsAxiom(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
getRepresentsAxiom
in interface FunctionalOperationContract
public boolean isReadOnlyContract(Services services)
isReadOnlyContract
in interface FunctionalOperationContract
public Term getAnyMod(Term mod, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
public Term getMod(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
OperationContract
getMod
in interface OperationContract
heap
- the heap variable.selfVar
- the self variable.paramVars
- the list of parameter variables.services
- the services object.public boolean hasModifiesClause(LocationVariable heap)
OperationContract
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 OperationContract
public Term getMod(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
OperationContract
getMod
in interface OperationContract
heap
- the heap variableheapTerm
- the heap variable term.selfTerm
- the self variable term.paramTerms
- the list of parameter variable terms.services
- the services object.public Term getDep(LocationVariable heap, boolean atPre, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Contract
public Term getDep(LocationVariable heap, boolean atPre, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)
Contract
getDep
in interface Contract
heap
- the heap variableatPre
- boolean whether old heap should be usedheapTerm
- the heap variable termselfTerm
- term of self variableparamTerms
- terms of parameter variablesatPres
- terms of variables at previous heapservices
- services objectpublic Term getGlobalDefs()
getGlobalDefs
in interface Contract
public Term getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
getGlobalDefs
in interface Contract
public java.lang.String toString()
toString
in class java.lang.Object
public final ContractPO createProofObl(InitConfig initConfig)
Contract
createProofObl
in interface Contract
initConfig
- the initial configurationpublic ProofOblInput getProofObl(Services services)
Contract
getProofObl
in interface Contract
services
- the services instancepublic ProofOblInput createProofObl(InitConfig initConfig, Contract contract)
Contract
createProofObl
in interface Contract
initConfig
- the initial configurationcontract
- the contractpublic ProofOblInput createProofObl(InitConfig initConfig, Contract contract, boolean addSymbolicExecutionLabel)
Contract
createProofObl
in interface Contract
initConfig
- the initial configurationcontract
- the contractaddSymbolicExecutionLabel
- boolean saying whether symbolic execution api is supportedpublic java.lang.String getDisplayName()
SpecificationElement
getDisplayName
in interface SpecificationElement
public VisibilityModifier getVisibility()
SpecificationElement
getVisibility
in interface SpecificationElement
public boolean transactionApplicableContract()
transactionApplicableContract
in interface Contract
public FunctionalOperationContract setID(int newId)
Contract
public Contract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
Contract
public java.lang.String getTypeName()
Contract
getTypeName
in interface Contract
public boolean hasSelfVar()
Contract
hasSelfVar
in interface Contract
true
self variable is originally provided, false
no self variable
available.public java.lang.String getBaseName()
getBaseName
in interface FunctionalOperationContract
public Term getPre()
getPre
in interface FunctionalOperationContract
public Term getPost()
getPost
in interface FunctionalOperationContract
public Term getMod()
getMod
in interface FunctionalOperationContract
public Term getMby()
getMby
in interface Contract
getMby
in interface FunctionalOperationContract
public Term getSelf()
getSelf
in interface FunctionalOperationContract
public boolean hasResultVar()
hasResultVar
in interface FunctionalOperationContract
public ImmutableList<Term> getParams()
getParams
in interface FunctionalOperationContract
public Term getResult()
getResult
in interface FunctionalOperationContract
public Term getExc()
getExc
in interface FunctionalOperationContract
public KeYJavaType getSpecifiedIn()
getSpecifiedIn
in interface FunctionalOperationContract
public Contract.OriginalVariables getOrigVars()
Contract
getOrigVars
in interface Contract
Copyright © 2003-2019 The KeY-Project.