de.uka.ilkd.key.speclang

Interface FunctionalOperationContract

All Superinterfaces:

Contract, OperationContract, SpecificationElement

All Known Implementing Classes:

FunctionalOperationContractImpl

public interface FunctionalOperationContract
extends OperationContract

A contract about an operation (i.e., a method or a constructor), consisting of a precondition, a postcondition, a modifies clause, a measured-by clause, and a modality.

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.speclang.Contract

Contract.OriginalVariables

Field Summary

Fields inherited from interface de.uka.ilkd.key.speclang.Contract

INVALID_ID

Method Summary

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)

Methods inherited from interface de.uka.ilkd.key.speclang.OperationContract

getFreePre, getFreePre, getFreePre, getMod, getMod, getTarget, hasModifiesClause

Methods inherited from interface de.uka.ilkd.key.speclang.Contract

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

Methods inherited from interface de.uka.ilkd.key.speclang.SpecificationElement

getDisplayName, getKJT, getName, getVisibility

Method Detail

getModality

Modality getModality()

Returns the modality of the contract.

isReadOnlyContract

boolean isReadOnlyContract(Services services)

getEnsures

Term getEnsures(LocationVariable heap)

getPost

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.

getPost

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)

getPost

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.

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)

getFreePost

Term getFreePost(LocationVariable heap,
                 ProgramVariable selfVar,
                 ImmutableList<ProgramVariable> paramVars,
                 ProgramVariable resultVar,
                 ProgramVariable excVar,
                 java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
                 Services services)

getFreePost

Term getFreePost(LocationVariable heap,
                 Term heapTerm,
                 Term selfTerm,
                 ImmutableList<Term> paramTerms,
                 Term resultTerm,
                 Term excTerm,
                 java.util.Map<LocationVariable,Term> atPres,
                 Services services)

getFreePost

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)

getRepresentsAxiom

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

getRepresentsAxiom

Term getRepresentsAxiom(LocationVariable heap,
                        Term heapTerm,
                        Term selfTerm,
                        ImmutableList<Term> paramTerms,
                        Term resultTerm,
                        Term excTerm,
                        java.util.Map<LocationVariable,Term> atPres,
                        Services services)

getBaseName

java.lang.String getBaseName()

getPre

Term getPre()

getPost

Term getPost()

getMod

Term getMod()

getMby

Term getMby()

Specified by:

getMby in interface Contract

getSelf

Term getSelf()

getParams

ImmutableList<Term> getParams()

getResult

Term getResult()

getExc

Term getExc()

getSpecifiedIn

KeYJavaType getSpecifiedIn()

hasResultVar

boolean hasResultVar()