public interface Contract extends SpecificationElement
Modifier and Type | Interface and Description |
---|---|
static class |
Contract.OriginalVariables
Class for storing the original variables without always distinguishing
several different cases depending on which variables are present/needed
in order to provide a general interface.
|
Modifier and Type | Field and Description |
---|---|
static int |
INVALID_ID |
Modifier and Type | Method and Description |
---|---|
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 supportSymbolicExecutionAPI)
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,
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.
|
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.
|
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.
|
Contract.OriginalVariables |
getOrigVars()
Returns the original ProgramVariables to replace them easier.
|
String |
getPlainText(Services services)
Returns the contract in pretty plain text format.
|
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.
|
Term |
getRequires(LocationVariable heap) |
IObserverFunction |
getTarget()
Returns the contracted function symbol.
|
String |
getTypeName()
Returns technical name for the contract type.
|
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.
|
String |
proofToString(Services services)
Returns a parseable String representation of the contract.
|
Contract |
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.
|
boolean |
transactionApplicableContract() |
getDisplayName, getKJT, getName, getVisibility
static final int INVALID_ID
int id()
IObserverFunction getTarget()
boolean hasMby()
Contract.OriginalVariables getOrigVars()
Term getPre(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Term getPre(List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Term getPre(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Map<LocationVariable,Term> atPres, Services services)
Term getPre(List<LocationVariable> heapContext, Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Map<LocationVariable,Term> atPres, Services services)
Term getDep(LocationVariable heap, boolean atPre, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Term getDep(LocationVariable heap, boolean atPre, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Map<LocationVariable,Term> atPres, Services services)
Term getRequires(LocationVariable heap)
Term getAssignable(LocationVariable heap)
Term getAccessible(ProgramVariable heap)
Term getGlobalDefs()
Term getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
Term getMby()
Term getMby(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
Term getMby(Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Map<LocationVariable,Term> atPres, Services services)
String getPlainText(Services services)
boolean toBeSaved()
boolean transactionApplicableContract()
String proofToString(Services services)
ContractPO createProofObl(InitConfig initConfig)
ProofOblInput getProofObl(Services services)
ProofOblInput createProofObl(InitConfig initConfig, Contract contract)
ProofOblInput createProofObl(InitConfig initConfig, Contract contract, boolean supportSymbolicExecutionAPI)
Contract setID(int newId)
Contract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
String getTypeName()
boolean hasSelfVar()
true
self variable is originally provided,
false
no self variable available.