public class FunctionalOperationContractImpl extends Object implements FunctionalOperationContract
Contract.OriginalVariables
Modifier and Type | Field and Description |
---|---|
(package private) String |
baseName |
(package private) Term |
globalDefs |
(package private) Map<LocationVariable,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) String |
name |
(package private) Map<LocationVariable,LocationVariable> |
originalAtPreVars |
(package private) Map<LocationVariable,Term> |
originalAxioms |
(package private) Map<ProgramVariable,Term> |
originalDeps |
(package private) ProgramVariable |
originalExcVar |
(package private) Map<LocationVariable,Term> |
originalFreePosts |
(package private) Map<LocationVariable,Term> |
originalFreePres |
(package private) Term |
originalMby |
(package private) Map<LocationVariable,Term> |
originalMods |
(package private) ImmutableList<ProgramVariable> |
originalParamVars |
(package private) Map<LocationVariable,Term> |
originalPosts |
(package private) 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(String baseName,
String name,
KeYJavaType kjt,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Map<LocationVariable,Term> pres,
Map<LocationVariable,Term> freePres,
Term mby,
Map<LocationVariable,Term> posts,
Map<LocationVariable,Term> freePosts,
Map<LocationVariable,Term> axioms,
Map<LocationVariable,Term> mods,
Map<ProgramVariable,Term> accessibles,
Map<LocationVariable,Boolean> hasRealMod,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
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 contract and 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) |
String |
getBaseName() |
Term |
getDep(LocationVariable heap,
boolean atPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
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,
Map<LocationVariable,Term> atPres,
Services services)
Returns the dependency set of the contract.
|
String |
getDisplayName()
Returns the displayed name.
|
Term |
getEnsures(LocationVariable heap) |
Term |
getExc() |
Term |
getFreePost(List<LocationVariable> heapContext,
Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
Map<LocationVariable,Term> atPres,
Services services) |
Term |
getFreePost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getFreePost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
Map<LocationVariable,Term> atPres,
Services services) |
Term |
getFreePre(List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getFreePre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getFreePre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Map<LocationVariable,Term> atPres,
Services services) |
Term |
getGlobalDefs() |
Term |
getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
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(Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
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.
|
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() |
String |
getPlainText(Services services)
Returns the contract in pretty plain text format.
|
Term |
getPost() |
Term |
getPost(List<LocationVariable> heapContext,
Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
Map<LocationVariable,Term> atPres,
Services services) |
Term |
getPost(List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getPost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
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,
Map<LocationVariable,Term> atPres,
Services services)
Returns the postcondition of the contract.
|
Term |
getPre() |
Term |
getPre(List<LocationVariable> heapContext,
Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Map<LocationVariable,Term> atPres,
Services services) |
Term |
getPre(List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getPre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the precondition of the contract.
|
Term |
getPre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
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 Map<Term,Term> |
getReplaceMap(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services)
Deprecated.
|
protected Map<Term,Term> |
getReplaceMap(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
Term atPre,
Services services)
Deprecated.
|
protected Map<Term,Term> |
getReplaceMap(Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
Map<LocationVariable,Term> atPres,
Services services) |
protected Map<ProgramVariable,ProgramVariable> |
getReplaceMap(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getRepresentsAxiom(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
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,
Map<LocationVariable,Term> atPres,
Services services) |
Term |
getRequires(LocationVariable heap) |
Term |
getResult() |
Term |
getSelf() |
KeYJavaType |
getSpecifiedIn() |
IProgramMethod |
getTarget()
Returns the contracted function symbol.
|
private String |
getText(boolean includeHtmlMarkup,
Services services) |
static String |
getText(FunctionalOperationContract contract,
ImmutableList<Term> contractParams,
Term resultTerm,
Term contractSelf,
Term excTerm,
LocationVariable baseHeap,
Term baseHeapTerm,
List<LocationVariable> heapContext,
Map<LocationVariable,Term> atPres,
boolean includeHtmlMarkup,
Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
private static String |
getText(IProgramMethod pm,
Operator originalResultVar,
Operator originalSelfVar,
ImmutableList<? extends SVSubstitute> originalParamVars,
ProgramVariable originalExcVar,
boolean hasMby,
Term originalMby,
Map<LocationVariable,Term> originalMods,
Map<LocationVariable,Boolean> hasRealModifiesClause,
Term globalDefs,
Map<LocationVariable,Term> originalPres,
Map<LocationVariable,Term> originalFreePres,
Map<LocationVariable,Term> originalPosts,
Map<LocationVariable,Term> originalFreePosts,
Map<LocationVariable,Term> originalAxioms,
Modality modality,
boolean transaction,
boolean includeHtmlMarkup,
Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
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) |
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.
|
String |
toString() |
boolean |
transactionApplicableContract() |
protected final TermBuilder TB
private final TermServices services
final String baseName
final String name
final KeYJavaType kjt
final IProgramMethod pm
final KeYJavaType specifiedIn
final Modality modality
final Map<LocationVariable,Term> originalPres
final Map<LocationVariable,Term> originalFreePres
final Term originalMby
final Map<LocationVariable,Term> originalPosts
final Map<LocationVariable,Term> originalFreePosts
final Map<LocationVariable,Term> originalAxioms
final Map<LocationVariable,Term> originalMods
final Map<ProgramVariable,Term> originalDeps
final ProgramVariable originalSelfVar
final ImmutableList<ProgramVariable> originalParamVars
final ProgramVariable originalResultVar
final ProgramVariable originalExcVar
final Map<LocationVariable,LocationVariable> originalAtPreVars
final Term globalDefs
final int id
final boolean transaction
final boolean toBeSaved
final Map<LocationVariable,Boolean> hasRealModifiesClause
#hasModifiesClause()
FunctionalOperationContractImpl(String baseName, String name, KeYJavaType kjt, IProgramMethod pm, KeYJavaType specifiedIn, Modality modality, Map<LocationVariable,Term> pres, Map<LocationVariable,Term> freePres, Term mby, Map<LocationVariable,Term> posts, Map<LocationVariable,Term> freePosts, Map<LocationVariable,Term> axioms, Map<LocationVariable,Term> mods, Map<ProgramVariable,Term> accessibles, Map<LocationVariable,Boolean> hasRealMod, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, 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 Map<ProgramVariable,ProgramVariable> getReplaceMap(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
@Deprecated protected Map<Term,Term> getReplaceMap(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
@Deprecated protected Map<Term,Term> getReplaceMap(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, Term atPre, Services services)
protected Map<Term,Term> getReplaceMap(Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, Map<LocationVariable,Term> atPres, Services services)
private ImmutableList<ProgramVariable> addGhostParams(ImmutableList<ProgramVariable> paramVars)
private ImmutableList<Term> addGhostParamTerms(ImmutableList<Term> paramVars)
public 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, Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Contract
public Term getPre(List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
public Term getPre(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Map<LocationVariable,Term> atPres, Services services)
Contract
public Term getPre(List<LocationVariable> heapContext, Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Map<LocationVariable,Term> atPres, Services services)
public Term getFreePre(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
getFreePre
in interface OperationContract
public Term getFreePre(List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
getFreePre
in interface OperationContract
public Term getFreePre(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, 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(Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Map<LocationVariable,Term> atPres, Services services)
Contract
public String getPlainText(Services services)
Contract
getPlainText
in interface Contract
public String getHTMLText(Services services)
Contract
getHTMLText
in interface Contract
public static String getText(FunctionalOperationContract contract, ImmutableList<Term> contractParams, Term resultTerm, Term contractSelf, Term excTerm, LocationVariable baseHeap, Term baseHeapTerm, List<LocationVariable> heapContext, Map<LocationVariable,Term> atPres, boolean includeHtmlMarkup, Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols)
private static String getText(IProgramMethod pm, Operator originalResultVar, Operator originalSelfVar, ImmutableList<? extends SVSubstitute> originalParamVars, ProgramVariable originalExcVar, boolean hasMby, Term originalMby, Map<LocationVariable,Term> originalMods, Map<LocationVariable,Boolean> hasRealModifiesClause, Term globalDefs, Map<LocationVariable,Term> originalPres, Map<LocationVariable,Term> originalFreePres, Map<LocationVariable,Term> originalPosts, Map<LocationVariable,Term> originalFreePosts, Map<LocationVariable,Term> originalAxioms, Modality modality, boolean transaction, boolean includeHtmlMarkup, Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols)
public boolean toBeSaved()
Contract
public String proofToString(Services services)
Contract
proofToString
in interface Contract
public Modality getModality()
FunctionalOperationContract
getModality
in interface FunctionalOperationContract
public Term getPost(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
FunctionalOperationContract
getPost
in interface FunctionalOperationContract
public Term getPost(List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, 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, Map<LocationVariable,Term> atPres, Services services)
FunctionalOperationContract
getPost
in interface FunctionalOperationContract
public Term getPost(List<LocationVariable> heapContext, Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, Map<LocationVariable,Term> atPres, Services services)
getPost
in interface FunctionalOperationContract
public Term getFreePost(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, 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, Map<LocationVariable,Term> atPres, Services services)
getFreePost
in interface FunctionalOperationContract
public Term getFreePost(List<LocationVariable> heapContext, Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, Map<LocationVariable,Term> atPres, Services services)
getFreePost
in interface FunctionalOperationContract
public Term getRepresentsAxiom(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, 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, 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, Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Contract
public Term getDep(LocationVariable heap, boolean atPre, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Map<LocationVariable,Term> atPres, Services services)
Contract
public 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 final ContractPO createProofObl(InitConfig initConfig)
Contract
createProofObl
in interface Contract
public ProofOblInput getProofObl(Services services)
Contract
getProofObl
in interface Contract
public ProofOblInput createProofObl(InitConfig initConfig, Contract contract)
Contract
createProofObl
in interface Contract
public ProofOblInput createProofObl(InitConfig initConfig, Contract contract, boolean addSymbolicExecutionLabel)
Contract
createProofObl
in interface Contract
public 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 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 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