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 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,
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.
|
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.
|
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.
|
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.
|
java.lang.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.
|
default boolean |
isAuxiliary() |
java.lang.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
default boolean isAuxiliary()
true
if any only if this contract does not necessarily need to be proven in
its own proof obligation. E.g., this is true for FunctionalBlockContract
s and
FunctionalLoopContract
s.int id()
IObserverFunction getTarget()
boolean hasMby()
Contract.OriginalVariables getOrigVars()
Term getPre(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
heap
- heap variableselfVar
- self variableparamVars
- parameter variablesatPreVars
- variables at previous heapservices
- services objectTerm getPre(java.util.List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
heapContext
- heap contextselfVar
- self variableparamVars
- parameter variablesatPreVars
- variables at previous heapservices
- services objectTerm getPre(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)
heap
- heap variableheapTerm
- heap termselfTerm
- self termparamTerms
- parameter termsatPres
- terms of variables at previous heapservices
- services objectTerm 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)
heapContext
- heap contextheapTerms
- heap termsselfTerm
- term of self variableparamTerms
- terms of parameter variablesatPres
- terms of variables at previous heapservices
- services objectTerm getDep(LocationVariable heap, boolean atPre, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
heap
- the heap variableatPre
- boolean whether old heap should be usedselfVar
- self variableparamVars
- parameter variablesatPreVars
- variables at previous heapservices
- services objectTerm getDep(LocationVariable heap, boolean atPre, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)
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 objectTerm 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)
selfVar
- the self variableparamVars
- the parameter variablesservices
- services objectTerm getMby(java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)
heapTerms
- terms for the heap contextselfTerm
- term of self variableparamTerms
- terms of parameter variablesatPres
- terms of variables at previous heapservices
- services objectjava.lang.String getHTMLText(Services services)
services
- services instancejava.lang.String getPlainText(Services services)
services
- services instanceboolean toBeSaved()
boolean transactionApplicableContract()
java.lang.String proofToString(Services services)
services
- the services instanceContractPO createProofObl(InitConfig initConfig)
initConfig
- the initial configurationProofOblInput getProofObl(Services services)
services
- the services instanceProofOblInput createProofObl(InitConfig initConfig, Contract contract)
initConfig
- the initial configurationcontract
- the contractProofOblInput createProofObl(InitConfig initConfig, Contract contract, boolean supportSymbolicExecutionAPI)
initConfig
- the initial configurationcontract
- the contractsupportSymbolicExecutionAPI
- boolean saying whether symbolic execution api is supportedContract setID(int newId)
newId
- the new id valueContract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
newKJT
- the new KeYJavaTypenewPM
- the new observer functionjava.lang.String getTypeName()
boolean hasSelfVar()
true
self variable is originally provided, false
no self variable
available.