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." |
OperationContract |
map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
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
OperationContract map(java.util.function.UnaryOperator<Term> op, Services services)
SpecificationElement
map
in interface Contract
map
in interface SpecificationElement
op
- the operator to apply.services
- services.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)
heapVar
- the heap variable.selfVar
- the self variable.paramVars
- the list of parameter variables.services
- the services object.Term getMod(LocationVariable heapVar, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
heapVar
- the heap variableheapTerm
- the heap variable term.selfTerm
- the self variable term.paramTerms
- the list of parameter variable terms.services
- the services object.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)
Copyright © 2003-2019 The KeY-Project.