public class FunctionalOperationContractImpl extends java.lang.Object implements FunctionalOperationContract
Contract.OriginalVariables
Modifier and Type | Field and Description |
---|---|
(package private) java.lang.String |
baseName |
(package private) Term |
globalDefs |
(package private) java.util.Map<LocationVariable,java.lang.Boolean> |
hasRealModifiesClause
If a method is strictly pure, it has no modifies clause which could
be anonymised.
|
(package private) int |
id |
(package private) KeYJavaType |
kjt |
(package private) Modality |
modality |
(package private) java.lang.String |
name |
(package private) java.util.Map<LocationVariable,LocationVariable> |
originalAtPreVars |
(package private) java.util.Map<LocationVariable,Term> |
originalAxioms |
(package private) java.util.Map<ProgramVariable,Term> |
originalDeps |
(package private) ProgramVariable |
originalExcVar |
(package private) java.util.Map<LocationVariable,Term> |
originalFreePosts |
(package private) java.util.Map<LocationVariable,Term> |
originalFreePres |
(package private) Term |
originalMby |
(package private) java.util.Map<LocationVariable,Term> |
originalMods |
(package private) ImmutableList<ProgramVariable> |
originalParamVars |
(package private) java.util.Map<LocationVariable,Term> |
originalPosts |
(package private) java.util.Map<LocationVariable,Term> |
originalPres |
(package private) ProgramVariable |
originalResultVar |
(package private) ProgramVariable |
originalSelfVar |
(package private) IProgramMethod |
pm |
private TermServices |
services |
(package private) KeYJavaType |
specifiedIn |
protected TermBuilder |
TB |
(package private) boolean |
toBeSaved |
(package private) boolean |
transaction |
INVALID_ID
Constructor and Description |
---|
FunctionalOperationContractImpl(java.lang.String baseName,
java.lang.String name,
KeYJavaType kjt,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
java.util.Map<LocationVariable,Term> pres,
java.util.Map<LocationVariable,Term> freePres,
Term mby,
java.util.Map<LocationVariable,Term> posts,
java.util.Map<LocationVariable,Term> freePosts,
java.util.Map<LocationVariable,Term> axioms,
java.util.Map<LocationVariable,Term> mods,
java.util.Map<ProgramVariable,Term> accessibles,
java.util.Map<LocationVariable,java.lang.Boolean> hasRealMod,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Term globalDefs,
int id,
boolean toBeSaved,
boolean transaction,
TermServices services)
Creates an operation contract.
|
Modifier and Type | Method and Description |
---|---|
private ImmutableList<ProgramVariable> |
addGhostParams(ImmutableList<ProgramVariable> paramVars)
Make sure ghost parameters appear in the list of parameter variables.
|
private ImmutableList<Term> |
addGhostParamTerms(ImmutableList<Term> paramVars)
Make sure ghost parameters appear in the list of parameter variables.
|
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) |
private Term |
getAnyMod(LocationVariable heap,
Term mod,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
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) |
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) |
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.
|
private java.lang.String |
getText(boolean includeHtmlMarkup,
Services services) |
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) |
private static java.lang.String |
getText(IProgramMethod pm,
Operator originalResultVar,
Operator originalSelfVar,
ImmutableList<? extends SVSubstitute> originalParamVars,
ProgramVariable originalExcVar,
boolean hasMby,
Term originalMby,
java.util.Map<LocationVariable,Term> originalMods,
java.util.Map<LocationVariable,java.lang.Boolean> hasRealModifiesClause,
Term globalDefs,
java.util.Map<LocationVariable,Term> originalPres,
java.util.Map<LocationVariable,Term> originalFreePres,
java.util.Map<LocationVariable,Term> originalPosts,
java.util.Map<LocationVariable,Term> originalFreePosts,
java.util.Map<LocationVariable,Term> originalAxioms,
Modality modality,
boolean transaction,
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) |
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
protected final TermBuilder TB
private final TermServices services
final java.lang.String baseName
final java.lang.String name
final KeYJavaType kjt
final IProgramMethod pm
final KeYJavaType specifiedIn
final Modality modality
final java.util.Map<LocationVariable,Term> originalPres
final java.util.Map<LocationVariable,Term> originalFreePres
final Term originalMby
final java.util.Map<LocationVariable,Term> originalPosts
final java.util.Map<LocationVariable,Term> originalFreePosts
final java.util.Map<LocationVariable,Term> originalAxioms
final java.util.Map<LocationVariable,Term> originalMods
final java.util.Map<ProgramVariable,Term> originalDeps
final ProgramVariable originalSelfVar
final ImmutableList<ProgramVariable> originalParamVars
final ProgramVariable originalResultVar
final ProgramVariable originalExcVar
final java.util.Map<LocationVariable,LocationVariable> originalAtPreVars
final Term globalDefs
final int id
final boolean transaction
final boolean toBeSaved
final java.util.Map<LocationVariable,java.lang.Boolean> hasRealModifiesClause
#hasModifiesClause()
FunctionalOperationContractImpl(java.lang.String baseName, java.lang.String name, KeYJavaType kjt, IProgramMethod pm, KeYJavaType specifiedIn, Modality modality, java.util.Map<LocationVariable,Term> pres, java.util.Map<LocationVariable,Term> freePres, Term mby, java.util.Map<LocationVariable,Term> posts, java.util.Map<LocationVariable,Term> freePosts, java.util.Map<LocationVariable,Term> axioms, java.util.Map<LocationVariable,Term> mods, java.util.Map<ProgramVariable,Term> accessibles, java.util.Map<LocationVariable,java.lang.Boolean> hasRealMod, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,LocationVariable> atPreVars, Term globalDefs, int id, boolean toBeSaved, boolean transaction, TermServices services)
ContractFactory
.baseName
- base name of the contract (does not have to be unique)pm
- the IProgramMethod to which the contract belongsmodality
- the modality of the contractmby
- the measured_by clause of the contractselfVar
- the variable used for the receiver objectparamVars
- the variables used for the operation parametersresultVar
- the variables used for the operation resultexcVar
- the variable used for the thrown exceptionglobalDefs
- definitions for the whole contractservices
- TODOpre
- the precondition of the contractpost
- the postcondition of the contractmod
- the modifies clause of the contractheapAtPreVar
- the variable used for the pre-heapprotected java.util.Map<ProgramVariable,ProgramVariable> getReplaceMap(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
@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)
private ImmutableList<ProgramVariable> addGhostParams(ImmutableList<ProgramVariable> paramVars)
private ImmutableList<Term> addGhostParamTerms(ImmutableList<Term> paramVars)
public 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 instanceprivate java.lang.String getText(boolean includeHtmlMarkup, Services services)
public 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)
private static java.lang.String getText(IProgramMethod pm, Operator originalResultVar, Operator originalSelfVar, ImmutableList<? extends SVSubstitute> originalParamVars, ProgramVariable originalExcVar, boolean hasMby, Term originalMby, java.util.Map<LocationVariable,Term> originalMods, java.util.Map<LocationVariable,java.lang.Boolean> hasRealModifiesClause, Term globalDefs, java.util.Map<LocationVariable,Term> originalPres, java.util.Map<LocationVariable,Term> originalFreePres, java.util.Map<LocationVariable,Term> originalPosts, java.util.Map<LocationVariable,Term> originalFreePosts, java.util.Map<LocationVariable,Term> originalAxioms, Modality modality, boolean transaction, 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
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
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
private Term getAnyMod(LocationVariable heap, Term mod, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
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
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