public interface OperationContract extends Contract
Contract.OriginalVariables
INVALID_ID
Modifier and Type | Method and Description |
---|---|
Term |
getFreePre(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getFreePre(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getFreePre(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
getMod(LocationVariable heapVar,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Returns the modifies clause of the contract.
|
Term |
getMod(LocationVariable heapVar,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services)
Returns the modifies clause of the contract.
|
IProgramMethod |
getTarget()
Returns the contracted function symbol.
|
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." |
createProofObl, createProofObl, createProofObl, getAccessible, getAssignable, getDep, getDep, getGlobalDefs, getGlobalDefs, getHTMLText, getMby, getMby, getMby, getOrigVars, getPlainText, getPre, getPre, getPre, getPre, getProofObl, getRequires, getTypeName, hasMby, hasSelfVar, id, isAuxiliary, proofToString, setID, setTarget, toBeSaved, transactionApplicableContract
getDisplayName, getKJT, getName, getVisibility
IProgramMethod getTarget()
Contract
boolean hasModifiesClause(LocationVariable heap)
true
iff the method (according to the contract) does
not modify the heap at all, i.e., iff it is "strictly pure."Term getMod(LocationVariable heapVar, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
Term getMod(LocationVariable heapVar, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
Term getFreePre(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Term getFreePre(java.util.List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Term getFreePre(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)