public interface InformationFlowContract extends Contract
Contract.OriginalVariables
INVALID_ID
Modifier and Type | Method and Description |
---|---|
boolean |
equals(Contract c) |
Term |
getAtPre() |
java.lang.String |
getBaseName() |
Term |
getDep()
Returns the dependency set of the contract.
|
Term |
getExc()
Get the exception-variable which is used in this contract.
|
ImmutableList<InfFlowSpec> |
getInfFlowSpecs()
Returns the set of views.
|
Term |
getMby()
Returns the original measured_by clause of the contract.
|
Term |
getMod()
Returns the original modifies clause of the contract.
|
Modality |
getModality()
Returns the modality of the contract.
|
ImmutableList<Term> |
getParams()
Get the parameter-variables which is used in this contract.
|
java.lang.String |
getPODisplayName()
For generating contract name of SymbolicExecutionPO
|
Term |
getPre()
Returns the original precondition of the contract.
|
Term |
getResult()
Get the result-variable which is used in this contract.
|
Term |
getSelf()
Get the self-variable which is used in this contract.
|
KeYJavaType |
getSpecifiedIn() |
IProgramMethod |
getTarget()
Returns the contracted function symbol.
|
boolean |
hasInfFlowSpec() |
boolean |
hasModifiesClause()
Returns
true iff the method (according to the contract) does
not modify the heap at all, i.e., iff it is "strictly pure." |
boolean |
isReadOnlyContract() |
InformationFlowContract |
setID(int newId)
Return a new contract which equals this contract except that the id is
set to the new id.
|
InformationFlowContract |
setModality(Modality modality) |
InformationFlowContract |
setModifies(Term modifies) |
InformationFlowContract |
setName(java.lang.String name) |
InformationFlowContract |
setTarget(KeYJavaType newKJT,
IObserverFunction newPM)
Return a new contract which equals this contract except that the
the KeYJavaType and ObserverFunction are set to the new values.
|
createProofObl, createProofObl, createProofObl, getAccessible, getAssignable, getDep, getDep, getGlobalDefs, getGlobalDefs, getHTMLText, getMby, getMby, getOrigVars, getPlainText, getPre, getPre, getPre, getPre, getProofObl, getRequires, getTypeName, hasMby, hasSelfVar, id, isAuxiliary, proofToString, toBeSaved, transactionApplicableContract
getDisplayName, getKJT, getName, getVisibility
java.lang.String getBaseName()
IProgramMethod getTarget()
Contract
KeYJavaType getSpecifiedIn()
boolean hasModifiesClause()
true
iff the method (according to the contract) does
not modify the heap at all, i.e., iff it is "strictly pure."Term getPre()
Term getMod()
Term getMby()
Term getExc()
Term getAtPre()
boolean isReadOnlyContract()
Modality getModality()
InformationFlowContract setName(java.lang.String name)
InformationFlowContract setModality(Modality modality)
InformationFlowContract setModifies(Term modifies)
InformationFlowContract setID(int newId)
Term getSelf()
ImmutableList<Term> getParams()
InformationFlowContract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
Term getResult()
boolean equals(Contract c)
java.lang.String getPODisplayName()
Term getDep()
ImmutableList<InfFlowSpec> getInfFlowSpecs()
boolean hasInfFlowSpec()