public final class DependencyContractImpl extends java.lang.Object implements DependencyContract
Contract.OriginalVariables
Modifier and Type | Field and Description |
---|---|
(package private) java.lang.String |
baseName |
(package private) Term |
globalDefs |
(package private) int |
id |
(package private) KeYJavaType |
kjt |
(package private) java.lang.String |
name |
(package private) java.util.Map<LocationVariable,? extends ProgramVariable> |
originalAtPreVars |
(package private) java.util.Map<ProgramVariable,Term> |
originalDeps |
(package private) Term |
originalMby |
(package private) ImmutableList<ProgramVariable> |
originalParamVars |
(package private) java.util.Map<LocationVariable,Term> |
originalPres |
(package private) ProgramVariable |
originalSelfVar |
(package private) KeYJavaType |
specifiedIn |
(package private) IObserverFunction |
target |
INVALID_ID
Constructor and Description |
---|
DependencyContractImpl(java.lang.String baseName,
KeYJavaType kjt,
IObserverFunction target,
KeYJavaType specifiedIn,
java.util.Map<LocationVariable,Term> pres,
Term mby,
java.util.Map<ProgramVariable,Term> deps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars)
Deprecated.
|
DependencyContractImpl(java.lang.String baseName,
java.lang.String name,
KeYJavaType kjt,
IObserverFunction target,
KeYJavaType specifiedIn,
java.util.Map<LocationVariable,Term> pres,
Term mby,
java.util.Map<ProgramVariable,Term> deps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Term globalDefs,
int 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 |
getAssignable(LocationVariable heap) |
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 |
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.
|
java.lang.String |
getName()
Returns the unique internal name of the specification element.
|
Contract.OriginalVariables |
getOrigVars()
Returns the original ProgramVariables to replace them easier.
|
java.lang.String |
getPlainText(Services services)
Returns the contract in pretty plain text format.
|
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.
|
Term |
getRequires(LocationVariable heap) |
IObserverFunction |
getTarget()
Returns the contracted function symbol.
|
private java.lang.String |
getText(boolean includeHtmlMarkup,
Services services) |
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 |
hasSelfVar()
Checks if a self variable is originally provided.
|
int |
id()
Returns the id number of the contract.
|
java.lang.String |
proofToString(Services services)
Returns a parseable String representation of the contract.
|
DependencyContract |
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
final java.lang.String baseName
final java.lang.String name
final KeYJavaType kjt
final IObserverFunction target
final KeYJavaType specifiedIn
final java.util.Map<LocationVariable,Term> originalPres
final Term originalMby
final java.util.Map<ProgramVariable,Term> originalDeps
final ProgramVariable originalSelfVar
final ImmutableList<ProgramVariable> originalParamVars
final java.util.Map<LocationVariable,? extends ProgramVariable> originalAtPreVars
final Term globalDefs
final int id
DependencyContractImpl(java.lang.String baseName, java.lang.String name, KeYJavaType kjt, IObserverFunction target, KeYJavaType specifiedIn, java.util.Map<LocationVariable,Term> pres, Term mby, java.util.Map<ProgramVariable,Term> deps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Term globalDefs, int id)
@Deprecated DependencyContractImpl(java.lang.String baseName, KeYJavaType kjt, IObserverFunction target, KeYJavaType specifiedIn, java.util.Map<LocationVariable,Term> pres, Term mby, java.util.Map<ProgramVariable,Term> deps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars)
public java.lang.String getName()
SpecificationElement
getName
in interface SpecificationElement
public int id()
Contract
public KeYJavaType getKJT()
SpecificationElement
getKJT
in interface SpecificationElement
public IObserverFunction getTarget()
Contract
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 getRequires(LocationVariable heap)
getRequires
in interface Contract
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 boolean toBeSaved()
Contract
public java.lang.String proofToString(Services services)
Contract
proofToString
in interface Contract
services
- the services instancepublic 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 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 final 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 ProofOblInput createProofObl(InitConfig initConfig, Contract contract)
Contract
createProofObl
in interface Contract
initConfig
- the initial configurationcontract
- the contractpublic 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 DependencyContract 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 Contract.OriginalVariables getOrigVars()
Contract
getOrigVars
in interface Contract