All Methods Instance Methods Abstract Methods
Modifier and Type |
Method and Description |
Term |
getAssignable(LocationVariable heap) |
StatementBlock |
getBlock() |
Term |
getEnsures(LocationVariable heap) |
String |
getHtmlText(Services services) |
ImmutableList<InfFlowSpec> |
getInfFlowSpecs()
Returns the original information flow specification clause of the contract.
|
Term |
getInstantiationSelfTerm(TermServices services)
Returns the term internally used for self or a newly instantiated one.
|
JoinProcedure |
getJoinProcedure() |
List<Label> |
getLabels() |
IProgramMethod |
getMethod() |
Term |
getMod(Services services)
Returns the original modifies clause of the contract.
|
Modality |
getModality() |
Term |
getModifiesClause(LocationVariable heap,
ProgramVariable self,
Services services) |
Term |
getModifiesClause(LocationVariable heap,
Services services) |
Term |
getModifiesClause(LocationVariable heapVariable,
Term heap,
Term self,
Services services) |
Contract.OriginalVariables |
getOrigVars() |
BlockContract.Variables |
getPlaceholderVariables() |
String |
getPlainText(Services services,
BlockContract.Terms terms) |
Term |
getPost(Services services)
Returns the original postcondition of the contract.
|
Term |
getPostcondition(LocationVariable heap,
BlockContract.Variables variables,
Services services) |
Term |
getPostcondition(LocationVariable heap,
Services services) |
Term |
getPostcondition(LocationVariable heapVariable,
Term heap,
BlockContract.Terms terms,
Services services) |
Term |
getPre(Services services)
Returns the original precondition of the contract.
|
Term |
getPrecondition(LocationVariable heap,
ProgramVariable self,
Map<LocationVariable,LocationVariable> remembranceHeaps,
Services services) |
Term |
getPrecondition(LocationVariable heap,
Services services) |
Term |
getPrecondition(LocationVariable heapVariable,
Term heap,
Term self,
Map<LocationVariable,Term> remembranceHeaps,
Services services) |
Term |
getRequires(LocationVariable heap) |
IProgramMethod |
getTarget()
Returns the method in which the block is located.
|
String |
getUniqueName() |
BlockContract.Variables |
getVariables()
Returns the original used variables like self, result etc..
|
BlockContract.Terms |
getVariablesAsTerms(Services services)
Returns the original used variables like self, result etc. as terms.
|
boolean |
hasInfFlowSpecs() |
boolean |
hasJoinProcedure() |
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 |
isReadOnly(Services services) |
boolean |
isTransactionApplicable() |
BlockContract |
setBlock(StatementBlock newBlock) |
void |
setInstantiationSelf(Term selfInstantiation) |
BlockContract |
setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
BlockContract |
update(StatementBlock newBlock,
Map<LocationVariable,Term> newPreconditions,
Map<LocationVariable,Term> newPostconditions,
Map<LocationVariable,Term> newModifiesClauses,
ImmutableList<InfFlowSpec> newInfFlowSpecs,
JoinProcedure newJoinProcedure,
BlockContract.Variables newVariables) |
void |
visit(Visitor visitor) |