public interface FunctionalOperationContract extends OperationContract
Contract.OriginalVariables
INVALID_ID
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getBaseName() |
Term |
getEnsures(LocationVariable heap) |
Term |
getExc() |
Term |
getFreePost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
getFreePost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getFreePost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
getMby() |
Term |
getMod() |
Modality |
getModality()
Returns the modality of the contract.
|
ImmutableList<Term> |
getParams() |
Term |
getPost() |
Term |
getPost(java.util.List<LocationVariable> heapContext,
java.util.Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
getPost(java.util.List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getPost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the postcondition of the contract.
|
Term |
getPost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services)
Returns the postcondition of the contract.
|
Term |
getPre() |
Term |
getRepresentsAxiom(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services)
Returns the model method definition for model method contracts
|
Term |
getRepresentsAxiom(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
java.util.Map<LocationVariable,Term> atPres,
Services services) |
Term |
getResult() |
Term |
getSelf() |
KeYJavaType |
getSpecifiedIn() |
boolean |
hasResultVar() |
boolean |
isReadOnlyContract(Services services) |
getFreePre, getFreePre, getFreePre, getMod, getMod, getTarget, hasModifiesClause
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, setID, setTarget, toBeSaved, transactionApplicableContract
getDisplayName, getKJT, getName, getVisibility
Modality getModality()
boolean isReadOnlyContract(Services services)
Term getEnsures(LocationVariable heap)
Term getPost(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Term getPost(java.util.List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Term getPost(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
Term getPost(java.util.List<LocationVariable> heapContext, java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
Term getFreePost(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Term getFreePost(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
Term getFreePost(java.util.List<LocationVariable> heapContext, java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
Term getRepresentsAxiom(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)
Term getRepresentsAxiom(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, java.util.Map<LocationVariable,Term> atPres, Services services)
java.lang.String getBaseName()
Term getPre()
Term getPost()
Term getMod()
Term getSelf()
ImmutableList<Term> getParams()
Term getResult()
Term getExc()
KeYJavaType getSpecifiedIn()
boolean hasResultVar()