Methods
Modifier and Type |
Method and Description |
String |
getBaseName() |
Term |
getEnsures(LocationVariable heap) |
Term |
getExc() |
Term |
getFreePost(List<LocationVariable> heapContext,
Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
Map<LocationVariable,Term> atPres,
Services services) |
Term |
getFreePost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getFreePost(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
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(List<LocationVariable> heapContext,
Map<LocationVariable,Term> heapTerms,
Term selfTerm,
ImmutableList<Term> paramTerms,
Term resultTerm,
Term excTerm,
Map<LocationVariable,Term> atPres,
Services services) |
Term |
getPost(List<LocationVariable> heapContext,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
Map<LocationVariable,? extends ProgramVariable> atPreVars,
Services services) |
Term |
getPost(LocationVariable heap,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
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,
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,
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,
Map<LocationVariable,Term> atPres,
Services services) |
Term |
getResult() |
Term |
getSelf() |
KeYJavaType |
getSpecifiedIn() |
boolean |
hasResultVar() |
boolean |
isReadOnlyContract(Services services) |