FunctionalOperationContractImpl (KeY API Documentation)

java.lang.Object
- de.uka.ilkd.key.speclang.FunctionalOperationContractImpl

All Implemented Interfaces:

Contract, FunctionalOperationContract, OperationContract, SpecificationElement
```
public class FunctionalOperationContractImpl
extends java.lang.Object
implements FunctionalOperationContract
```
Standard implementation of the OperationContract interface.

Nested Class Summary
- Nested classes/interfaces inherited from interface de.uka.ilkd.key.speclang.Contract
  Contract.OriginalVariables

Field Summary

Fields
Modifier and Type	Field and Description
`(package private) java.lang.String`	`baseName`
`(package private) Term`	`globalDefs`
`(package private) java.util.Map<LocationVariable,java.lang.Boolean>`	`hasRealModifiesClause` If a method is strictly pure, it has no modifies clause which could be anonymised.
`(package private) int`	`id`
`(package private) KeYJavaType`	`kjt`
`(package private) Modality`	`modality`
`(package private) java.lang.String`	`name`
`(package private) java.util.Map<LocationVariable,LocationVariable>`	`originalAtPreVars`
`(package private) java.util.Map<LocationVariable,Term>`	`originalAxioms`
`(package private) java.util.Map<ProgramVariable,Term>`	`originalDeps`
`(package private) ProgramVariable`	`originalExcVar`
`(package private) java.util.Map<LocationVariable,Term>`	`originalFreePosts`
`(package private) java.util.Map<LocationVariable,Term>`	`originalFreePres`
`(package private) Term`	`originalMby`
`(package private) java.util.Map<LocationVariable,Term>`	`originalMods`
`(package private) ImmutableList<ProgramVariable>`	`originalParamVars`
`(package private) java.util.Map<LocationVariable,Term>`	`originalPosts`
`(package private) java.util.Map<LocationVariable,Term>`	`originalPres`
`(package private) ProgramVariable`	`originalResultVar`
`(package private) ProgramVariable`	`originalSelfVar`
`(package private) IProgramMethod`	`pm`
`private TermServices`	`services`
`(package private) KeYJavaType`	`specifiedIn`
`protected TermBuilder`	`TB`
`(package private) boolean`	`toBeSaved`
`(package private) boolean`	`transaction`

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

Constructor Summary

Constructors
Constructor and Description
FunctionalOperationContractImpl(java.lang.String baseName, java.lang.String name, KeYJavaType kjt, IProgramMethod pm, KeYJavaType specifiedIn, Modality modality, java.util.Map<LocationVariable,Term> pres, java.util.Map<LocationVariable,Term> freePres, Term mby, java.util.Map<LocationVariable,Term> posts, java.util.Map<LocationVariable,Term> freePosts, java.util.Map<LocationVariable,Term> axioms, java.util.Map<LocationVariable,Term> mods, java.util.Map<ProgramVariable,Term> accessibles, java.util.Map<LocationVariable,java.lang.Boolean> hasRealMod, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,LocationVariable> atPreVars, Term globalDefs, int id, boolean toBeSaved, boolean transaction, TermServices services) Creates an operation contract.

Method Summary

All Methods Static Methods Instance Methods Concrete Methods Deprecated Methods
Modifier and Type	Method and Description
`private ImmutableList<ProgramVariable>`	`addGhostParams(ImmutableList<ProgramVariable> paramVars)` Make sure ghost parameters appear in the list of parameter variables.
`private ImmutableList<Term>`	`addGhostParamTerms(ImmutableList<Term> paramVars)` Make sure ghost parameters appear in the list of parameter variables.
`ContractPO`	`createProofObl(InitConfig initConfig)` Returns a proof obligation to the passed initConfig.
`ProofOblInput`	`createProofObl(InitConfig initConfig, Contract contract)` Returns a proof obligation to the passed contract and initConfig.
`ProofOblInput`	`createProofObl(InitConfig initConfig, Contract contract, boolean addSymbolicExecutionLabel)` Returns a proof obligation to the passed contract and initConfig.
`Term`	`getAccessible(ProgramVariable heap)`
`private Term`	`getAnyMod(LocationVariable heap, Term mod, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)`
`Term`	`getAnyMod(Term mod, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)`
`Term`	`getAssignable(LocationVariable heap)`
`java.lang.String`	`getBaseName()`
`Term`	`getDep(LocationVariable heap, boolean atPre, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)` Returns the dependency set of the contract.
`Term`	`getDep(LocationVariable heap, boolean atPre, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)` Returns the dependency set of the contract.
`java.lang.String`	`getDisplayName()` Returns the displayed name.
`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`	`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`	`getGlobalDefs()`
`Term`	`getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)`
`java.lang.String`	`getHTMLText(Services services)` Returns the contract in pretty HTML format.
`KeYJavaType`	`getKJT()` Returns the KeYJavaType representing the class/interface to which the specification element belongs.
`Term`	`getMby()`
`Term`	`getMby(java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)` Returns the measured_by clause of the contract.
`Term`	`getMby(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)` Returns the measured_by clause of the contract.
`Term`	`getMod()`
`Term`	`getMod(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)` Returns the modifies clause of the contract.
`Term`	`getMod(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)` Returns the modifies clause of the contract.
`Modality`	`getModality()` Returns the modality of the contract.
`java.lang.String`	`getName()` Returns the unique internal name of the specification element.
`Contract.OriginalVariables`	`getOrigVars()` Returns the original ProgramVariables to replace them easier.
`ImmutableList<Term>`	`getParams()`
`java.lang.String`	`getPlainText(Services services)` Returns the contract in pretty plain text format.
`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`	`getPre(java.util.List<LocationVariable> heapContext, java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)` Returns the precondition of the contract.
`Term`	`getPre(java.util.List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)` Returns the precondition of the contract.
`Term`	`getPre(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)` Returns the precondition of the contract.
`Term`	`getPre(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services)` Returns the precondition of the contract.
`ProofOblInput`	`getProofObl(Services services)` Lookup the proof obligation belonging to the contract in the specification repository.
`protected java.util.Map<Term,Term>`	`getReplaceMap(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)` Deprecated.
`protected java.util.Map<Term,Term>`	`getReplaceMap(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, Term atPre, Services services)` Deprecated.
`protected java.util.Map<Term,Term>`	`getReplaceMap(java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, Term resultTerm, Term excTerm, java.util.Map<LocationVariable,Term> atPres, Services services)`
`protected java.util.Map<ProgramVariable,ProgramVariable>`	`getReplaceMap(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services)`
`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`	`getRequires(LocationVariable heap)`
`Term`	`getResult()`
`Term`	`getSelf()`
`KeYJavaType`	`getSpecifiedIn()`
`IProgramMethod`	`getTarget()` Returns the contracted function symbol.
`private java.lang.String`	`getText(boolean includeHtmlMarkup, Services services)`
`static java.lang.String`	`getText(FunctionalOperationContract contract, ImmutableList<Term> contractParams, Term resultTerm, Term contractSelf, Term excTerm, LocationVariable baseHeap, Term baseHeapTerm, java.util.List<LocationVariable> heapContext, java.util.Map<LocationVariable,Term> atPres, boolean includeHtmlMarkup, Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols)`
`private static java.lang.String`	getText(IProgramMethod pm, Operator originalResultVar, Operator originalSelfVar, ImmutableList<? extends SVSubstitute> originalParamVars, ProgramVariable originalExcVar, boolean hasMby, Term originalMby, java.util.Map<LocationVariable,Term> originalMods, java.util.Map<LocationVariable,java.lang.Boolean> hasRealModifiesClause, Term globalDefs, java.util.Map<LocationVariable,Term> originalPres, java.util.Map<LocationVariable,Term> originalFreePres, java.util.Map<LocationVariable,Term> originalPosts, java.util.Map<LocationVariable,Term> originalFreePosts, java.util.Map<LocationVariable,Term> originalAxioms, Modality modality, boolean transaction, boolean includeHtmlMarkup, Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols)
`java.lang.String`	`getTypeName()` Returns technical name for the contract type.
`VisibilityModifier`	`getVisibility()` Returns the visibility of the invariant (null for default visibility)
`boolean`	`hasMby()` Tells whether the contract contains a measured_by clause.
`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."
`boolean`	`hasResultVar()`
`boolean`	`hasSelfVar()` Checks if a self variable is originally provided.
`int`	`id()` Returns the id number of the contract.
`boolean`	`isReadOnlyContract(Services services)`
`java.lang.String`	`proofToString(Services services)` Returns a parseable String representation of the contract.
`FunctionalOperationContract`	`setID(int newId)` Returns a contract which is identical this contract except that the id is set to the new id.
`Contract`	`setTarget(KeYJavaType newKJT, IObserverFunction newPM)` Returns a contract which is identical to this contract except that the KeYJavaType and IObserverFunction are set to the new values.
`boolean`	`toBeSaved()` Tells whether, on saving a proof where this contract is available, the contract should be saved too.
`java.lang.String`	`toString()`
`boolean`	`transactionApplicableContract()`

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

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

Field Detail

TB
```
protected final TermBuilder TB
```

services
```
private final TermServices services
```

baseName
```
final java.lang.String baseName
```

name
```
final java.lang.String name
```

kjt
```
final KeYJavaType kjt
```

pm
```
final IProgramMethod pm
```

specifiedIn
```
final KeYJavaType specifiedIn
```

modality
```
final Modality modality
```

originalPres

final java.util.Map<LocationVariable,Term> originalPres

originalFreePres

final java.util.Map<LocationVariable,Term> originalFreePres

originalMby
```
final Term originalMby
```

originalPosts

final java.util.Map<LocationVariable,Term> originalPosts

originalFreePosts

final java.util.Map<LocationVariable,Term> originalFreePosts

originalAxioms

final java.util.Map<LocationVariable,Term> originalAxioms

originalMods

final java.util.Map<LocationVariable,Term> originalMods

originalDeps

final java.util.Map<ProgramVariable,Term> originalDeps

originalSelfVar
```
final ProgramVariable originalSelfVar
```

originalParamVars

final ImmutableList<ProgramVariable> originalParamVars

originalResultVar

final ProgramVariable originalResultVar

originalExcVar
```
final ProgramVariable originalExcVar
```

originalAtPreVars

final java.util.Map<LocationVariable,LocationVariable> originalAtPreVars

globalDefs
```
final Term globalDefs
```

id
```
final int id
```

transaction
```
final boolean transaction
```

toBeSaved
```
final boolean toBeSaved
```

hasRealModifiesClause
```
final java.util.Map<LocationVariable,java.lang.Boolean> hasRealModifiesClause
```
If a method is strictly pure, it has no modifies clause which could be anonymised.

See Also:

#hasModifiesClause()

Constructor Detail

FunctionalOperationContractImpl

FunctionalOperationContractImpl(java.lang.String baseName,
                                java.lang.String name,
                                KeYJavaType kjt,
                                IProgramMethod pm,
                                KeYJavaType specifiedIn,
                                Modality modality,
                                java.util.Map<LocationVariable,Term> pres,
                                java.util.Map<LocationVariable,Term> freePres,
                                Term mby,
                                java.util.Map<LocationVariable,Term> posts,
                                java.util.Map<LocationVariable,Term> freePosts,
                                java.util.Map<LocationVariable,Term> axioms,
                                java.util.Map<LocationVariable,Term> mods,
                                java.util.Map<ProgramVariable,Term> accessibles,
                                java.util.Map<LocationVariable,java.lang.Boolean> hasRealMod,
                                ProgramVariable selfVar,
                                ImmutableList<ProgramVariable> paramVars,
                                ProgramVariable resultVar,
                                ProgramVariable excVar,
                                java.util.Map<LocationVariable,LocationVariable> atPreVars,
                                Term globalDefs,
                                int id,
                                boolean toBeSaved,
                                boolean transaction,
                                TermServices services)

Creates an operation contract. Using this constructor is discouraged: it may change in the future. Please use the factory methods in ContractFactory.

Parameters:: baseName - base name of the contract (does not have to be unique); pm - the IProgramMethod to which the contract belongs; modality - the modality of the contract; mby - the measured_by clause of the contract; selfVar - the variable used for the receiver object; paramVars - the variables used for the operation parameters; resultVar - the variables used for the operation result; excVar - the variable used for the thrown exception; globalDefs - definitions for the whole contract; services - TODO; pre - the precondition of the contract; post - the postcondition of the contract; mod - the modifies clause of the contract; heapAtPreVar - the variable used for the pre-heap

Method Detail

getReplaceMap

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

getReplaceMap

@Deprecated
protected java.util.Map<Term,Term> getReplaceMap(LocationVariable heap,
                                                             Term heapTerm,
                                                             Term selfTerm,
                                                             ImmutableList<Term> paramTerms,
                                                             Services services)

Deprecated.

getReplaceMap

@Deprecated
protected java.util.Map<Term,Term> getReplaceMap(LocationVariable heap,
                                                             Term heapTerm,
                                                             Term selfTerm,
                                                             ImmutableList<Term> paramTerms,
                                                             Term resultTerm,
                                                             Term excTerm,
                                                             Term atPre,
                                                             Services services)

Deprecated.

getReplaceMap

protected java.util.Map<Term,Term> getReplaceMap(java.util.Map<LocationVariable,Term> heapTerms,
                                                 Term selfTerm,
                                                 ImmutableList<Term> paramTerms,
                                                 Term resultTerm,
                                                 Term excTerm,
                                                 java.util.Map<LocationVariable,Term> atPres,
                                                 Services services)

addGhostParams

private ImmutableList<ProgramVariable> addGhostParams(ImmutableList<ProgramVariable> paramVars)

Make sure ghost parameters appear in the list of parameter variables.

addGhostParamTerms
```
private ImmutableList<Term> addGhostParamTerms(ImmutableList<Term> paramVars)
```
Make sure ghost parameters appear in the list of parameter variables.

getName
```
public java.lang.String getName()
```
Description copied from interface: SpecificationElement

Returns the unique internal name of the specification element.

Specified by:

getName in interface SpecificationElement

id
```
public int id()
```
Description copied from interface: Contract

Returns the id number of the contract. If a contract has instances for several methods (inheritance!), all instances have the same id. The id is either non-negative or equal to INVALID_ID.

Specified by:

id in interface Contract

getKJT
```
public KeYJavaType getKJT()
```
Description copied from interface: SpecificationElement

Returns the KeYJavaType representing the class/interface to which the specification element belongs.

Specified by:

getKJT in interface SpecificationElement

getTarget
```
public IProgramMethod getTarget()
```
Description copied from interface: Contract

Returns the contracted function symbol.

Specified by:

getTarget in interface Contract

Specified by:

getTarget in interface OperationContract

hasMby
```
public boolean hasMby()
```
Description copied from interface: Contract

Tells whether the contract contains a measured_by clause.

Specified by:

hasMby in interface Contract

getPre

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

Description copied from interface: Contract

Returns the precondition of the contract.

Specified by:: getPre in interface Contract
Parameters:: heap - heap variable; selfVar - self variable; paramVars - parameter variables; atPreVars - variables at previous heap; services - services object
Returns:: precondition

getPre

public Term getPre(java.util.List<LocationVariable> heapContext,
                   ProgramVariable selfVar,
                   ImmutableList<ProgramVariable> paramVars,
                   java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
                   Services services)

Description copied from interface: Contract

Returns the precondition of the contract.

Specified by:: getPre in interface Contract
Parameters:: heapContext - heap context; selfVar - self variable; paramVars - parameter variables; atPreVars - variables at previous heap; services - services object
Returns:: precondition

getPre

public Term getPre(LocationVariable heap,
                   Term heapTerm,
                   Term selfTerm,
                   ImmutableList<Term> paramTerms,
                   java.util.Map<LocationVariable,Term> atPres,
                   Services services)

Description copied from interface: Contract

Returns the precondition of the contract.

Specified by:: getPre in interface Contract
Parameters:: heap - heap variable; heapTerm - heap term; selfTerm - self term; paramTerms - parameter terms; atPres - terms of variables at previous heap; services - services object
Returns:: the precondition

getPre

public Term getPre(java.util.List<LocationVariable> heapContext,
                   java.util.Map<LocationVariable,Term> heapTerms,
                   Term selfTerm,
                   ImmutableList<Term> paramTerms,
                   java.util.Map<LocationVariable,Term> atPres,
                   Services services)

Description copied from interface: Contract

Returns the precondition of the contract.

Specified by:: getPre in interface Contract
Parameters:: heapContext - heap context; heapTerms - heap terms; selfTerm - term of self variable; paramTerms - terms of parameter variables; atPres - terms of variables at previous heap; services - services object
Returns:: the precondition

getFreePre

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

Specified by:: getFreePre in interface OperationContract

getFreePre

public Term getFreePre(java.util.List<LocationVariable> heapContext,
                       ProgramVariable selfVar,
                       ImmutableList<ProgramVariable> paramVars,
                       java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
                       Services services)

Specified by:: getFreePre in interface OperationContract

getFreePre

public Term getFreePre(LocationVariable heap,
                       Term heapTerm,
                       Term selfTerm,
                       ImmutableList<Term> paramTerms,
                       java.util.Map<LocationVariable,Term> atPres,
                       Services services)

Specified by:: getFreePre in interface OperationContract

getRequires

public Term getRequires(LocationVariable heap)

Specified by:: getRequires in interface Contract

getEnsures
```
public Term getEnsures(LocationVariable heap)
```
Specified by:

getEnsures in interface FunctionalOperationContract

getAssignable
```
public Term getAssignable(LocationVariable heap)
```
Specified by:

getAssignable in interface Contract

getAccessible
```
public Term getAccessible(ProgramVariable heap)
```
Specified by:

getAccessible in interface Contract

getMby
```
public Term getMby(ProgramVariable selfVar,
                   ImmutableList<ProgramVariable> paramVars,
                   Services services)
```
Description copied from interface: Contract

Returns the measured_by clause of the contract.

Specified by:

getMby in interface Contract

Parameters:

selfVar - the self variable

paramVars - the parameter variables

services - services object

Returns:

the measured-by term

getMby
```
public Term getMby(java.util.Map<LocationVariable,Term> heapTerms,
                   Term selfTerm,
                   ImmutableList<Term> paramTerms,
                   java.util.Map<LocationVariable,Term> atPres,
                   Services services)
```
Description copied from interface: Contract

Returns the measured_by clause of the contract.

Specified by:

getMby in interface Contract

Parameters:

heapTerms - terms for the heap context

selfTerm - term of self variable

paramTerms - terms of parameter variables

atPres - terms of variables at previous heap

services - services object

Returns:

the measured-by term

getPlainText
```
public java.lang.String getPlainText(Services services)
```
Description copied from interface: Contract

Returns the contract in pretty plain text format.

Specified by:

getPlainText in interface Contract

Parameters:

services - services instance

Returns:

the plain text representation

getHTMLText
```
public java.lang.String getHTMLText(Services services)
```
Description copied from interface: Contract

Returns the contract in pretty HTML format.

Specified by:

getHTMLText in interface Contract

Parameters:

services - services instance

Returns:

the html representation

getText

private java.lang.String getText(boolean includeHtmlMarkup,
                                 Services services)

getText

public static java.lang.String getText(FunctionalOperationContract contract,
                                       ImmutableList<Term> contractParams,
                                       Term resultTerm,
                                       Term contractSelf,
                                       Term excTerm,
                                       LocationVariable baseHeap,
                                       Term baseHeapTerm,
                                       java.util.List<LocationVariable> heapContext,
                                       java.util.Map<LocationVariable,Term> atPres,
                                       boolean includeHtmlMarkup,
                                       Services services,
                                       boolean usePrettyPrinting,
                                       boolean useUnicodeSymbols)

getText

private static java.lang.String getText(IProgramMethod pm,
                                        Operator originalResultVar,
                                        Operator originalSelfVar,
                                        ImmutableList<? extends SVSubstitute> originalParamVars,
                                        ProgramVariable originalExcVar,
                                        boolean hasMby,
                                        Term originalMby,
                                        java.util.Map<LocationVariable,Term> originalMods,
                                        java.util.Map<LocationVariable,java.lang.Boolean> hasRealModifiesClause,
                                        Term globalDefs,
                                        java.util.Map<LocationVariable,Term> originalPres,
                                        java.util.Map<LocationVariable,Term> originalFreePres,
                                        java.util.Map<LocationVariable,Term> originalPosts,
                                        java.util.Map<LocationVariable,Term> originalFreePosts,
                                        java.util.Map<LocationVariable,Term> originalAxioms,
                                        Modality modality,
                                        boolean transaction,
                                        boolean includeHtmlMarkup,
                                        Services services,
                                        boolean usePrettyPrinting,
                                        boolean useUnicodeSymbols)

toBeSaved
```
public boolean toBeSaved()
```
Description copied from interface: Contract

Tells whether, on saving a proof where this contract is available, the contract should be saved too. (this is currently true for contracts specified directly in DL, but not for JML contracts)

Specified by:

toBeSaved in interface Contract

Returns:

see above

proofToString
```
public java.lang.String proofToString(Services services)
```
Description copied from interface: Contract

Returns a parseable String representation of the contract. Precondition: toBeSaved() must be true.

Specified by:

proofToString in interface Contract

Parameters:

services - the services instance

Returns:

the (parseable) String representation

getModality
```
public Modality getModality()
```
Description copied from interface: FunctionalOperationContract

Returns the modality of the contract.

Specified by:

getModality in interface FunctionalOperationContract

getPost

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

Description copied from interface: FunctionalOperationContract

Returns the postcondition of the contract.

Specified by:: getPost in interface FunctionalOperationContract

getPost

public 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)

Specified by:: getPost in interface FunctionalOperationContract

getPost

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

Description copied from interface: FunctionalOperationContract

Returns the postcondition of the contract.

Specified by:: getPost in interface FunctionalOperationContract

getPost

public 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)

Specified by:: getPost in interface FunctionalOperationContract

getFreePost

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

Specified by:: getFreePost in interface FunctionalOperationContract

getFreePost

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

Specified by:: getFreePost in interface FunctionalOperationContract

getFreePost

public 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)

Specified by:: getFreePost in interface FunctionalOperationContract

getRepresentsAxiom

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

Description copied from interface: FunctionalOperationContract

Returns the model method definition for model method contracts

Specified by:: getRepresentsAxiom in interface FunctionalOperationContract

getRepresentsAxiom

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

Specified by:: getRepresentsAxiom in interface FunctionalOperationContract

isReadOnlyContract
```
public boolean isReadOnlyContract(Services services)
```
Specified by:

isReadOnlyContract in interface FunctionalOperationContract

getAnyMod

public Term getAnyMod(Term mod,
                      ProgramVariable selfVar,
                      ImmutableList<ProgramVariable> paramVars,
                      Services services)

getMod

public Term getMod(LocationVariable heap,
                   ProgramVariable selfVar,
                   ImmutableList<ProgramVariable> paramVars,
                   Services services)

Description copied from interface: OperationContract

Returns the modifies clause of the contract.

Specified by:: getMod in interface OperationContract

getAnyMod

private Term getAnyMod(LocationVariable heap,
                       Term mod,
                       Term heapTerm,
                       Term selfTerm,
                       ImmutableList<Term> paramTerms,
                       Services services)

hasModifiesClause
```
public boolean hasModifiesClause(LocationVariable heap)
```
Description copied from interface: OperationContract

Returns true iff the method (according to the contract) does not modify the heap at all, i.e., iff it is "strictly pure."

Specified by:

hasModifiesClause in interface OperationContract

Returns:

whether this contract is strictly pure.

getMod

public Term getMod(LocationVariable heap,
                   Term heapTerm,
                   Term selfTerm,
                   ImmutableList<Term> paramTerms,
                   Services services)

Description copied from interface: OperationContract

Returns the modifies clause of the contract.

Specified by:: getMod in interface OperationContract

getDep

public Term getDep(LocationVariable heap,
                   boolean atPre,
                   ProgramVariable selfVar,
                   ImmutableList<ProgramVariable> paramVars,
                   java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
                   Services services)

Description copied from interface: Contract

Returns the dependency set of the contract.

Specified by:: getDep in interface Contract
Parameters:: heap - the heap variable; atPre - boolean whether old heap should be used; selfVar - self variable; paramVars - parameter variables; atPreVars - variables at previous heap; services - services object
Returns:: the dependency set

getDep
```
public Term getDep(LocationVariable heap,
                   boolean atPre,
                   Term heapTerm,
                   Term selfTerm,
                   ImmutableList<Term> paramTerms,
                   java.util.Map<LocationVariable,Term> atPres,
                   Services services)
```
Description copied from interface: Contract

Returns the dependency set of the contract.

Specified by:

getDep in interface Contract

Parameters:

heap - the heap variable

atPre - boolean whether old heap should be used

heapTerm - the heap variable term

selfTerm - term of self variable

paramTerms - terms of parameter variables

atPres - terms of variables at previous heap

services - services object

Returns:

the dependency set

getGlobalDefs
```
public Term getGlobalDefs()
```
Specified by:

getGlobalDefs in interface Contract

getGlobalDefs

public Term getGlobalDefs(LocationVariable heap,
                          Term heapTerm,
                          Term selfTerm,
                          ImmutableList<Term> paramTerms,
                          Services services)

Specified by:: getGlobalDefs in interface Contract

toString
```
public java.lang.String toString()
```
Overrides:

toString in class java.lang.Object

createProofObl
```
public final ContractPO createProofObl(InitConfig initConfig)
```
Description copied from interface: Contract

Returns a proof obligation to the passed initConfig.

Specified by:

createProofObl in interface Contract

Parameters:

initConfig - the initial configuration

Returns:

the proof obligation

getProofObl
```
public ProofOblInput getProofObl(Services services)
```
Description copied from interface: Contract

Lookup the proof obligation belonging to the contract in the specification repository.

Specified by:

getProofObl in interface Contract

Parameters:

services - the services instance

Returns:

the proof obligation according to the specification repository

createProofObl
```
public ProofOblInput createProofObl(InitConfig initConfig,
                                    Contract contract)
```
Description copied from interface: Contract

Returns a proof obligation to the passed contract and initConfig.

Specified by:

createProofObl in interface Contract

Parameters:

initConfig - the initial configuration

contract - the contract

Returns:

the proof obligation

createProofObl
```
public ProofOblInput createProofObl(InitConfig initConfig,
                                    Contract contract,
                                    boolean addSymbolicExecutionLabel)
```
Description copied from interface: Contract

Returns a proof obligation to the passed contract and initConfig.

Specified by:

createProofObl in interface Contract

Parameters:

initConfig - the initial configuration

contract - the contract

addSymbolicExecutionLabel - boolean saying whether symbolic execution api is supported

Returns:

the proof obligation

getDisplayName
```
public java.lang.String getDisplayName()
```
Description copied from interface: SpecificationElement

Returns the displayed name.

Specified by:

getDisplayName in interface SpecificationElement

getVisibility
```
public VisibilityModifier getVisibility()
```
Description copied from interface: SpecificationElement

Returns the visibility of the invariant (null for default visibility)

Specified by:

getVisibility in interface SpecificationElement

transactionApplicableContract
```
public boolean transactionApplicableContract()
```
Specified by:

transactionApplicableContract in interface Contract

setID
```
public FunctionalOperationContract setID(int newId)
```
Description copied from interface: Contract

Returns a contract which is identical this contract except that the id is set to the new id.

Specified by:

setID in interface Contract

Parameters:

newId - the new id value

Returns:

an identical contract with the new id

setTarget
```
public Contract setTarget(KeYJavaType newKJT,
                          IObserverFunction newPM)
```
Description copied from interface: Contract

Returns a contract which is identical to this contract except that the KeYJavaType and IObserverFunction are set to the new values.

Specified by:

setTarget in interface Contract

Parameters:

newKJT - the new KeYJavaType

newPM - the new observer function

Returns:

an identical contract with the new KJT and PM (see above)

getTypeName
```
public java.lang.String getTypeName()
```
Description copied from interface: Contract

Returns technical name for the contract type.

Specified by:

getTypeName in interface Contract

Returns:

the technical name

hasSelfVar
```
public boolean hasSelfVar()
```
Description copied from interface: Contract

Checks if a self variable is originally provided.

Specified by:

hasSelfVar in interface Contract

Returns:

true self variable is originally provided, false no self variable available.

getBaseName
```
public java.lang.String getBaseName()
```
Specified by:

getBaseName in interface FunctionalOperationContract

getPre
```
public Term getPre()
```
Specified by:

getPre in interface FunctionalOperationContract

getPost
```
public Term getPost()
```
Specified by:

getPost in interface FunctionalOperationContract

getMod
```
public Term getMod()
```
Specified by:

getMod in interface FunctionalOperationContract

getMby
```
public Term getMby()
```
Specified by:

getMby in interface Contract

Specified by:

getMby in interface FunctionalOperationContract

getSelf
```
public Term getSelf()
```
Specified by:

getSelf in interface FunctionalOperationContract

hasResultVar
```
public boolean hasResultVar()
```
Specified by:

hasResultVar in interface FunctionalOperationContract

getParams
```
public ImmutableList<Term> getParams()
```
Specified by:

getParams in interface FunctionalOperationContract

getResult
```
public Term getResult()
```
Specified by:

getResult in interface FunctionalOperationContract

getExc
```
public Term getExc()
```
Specified by:

getExc in interface FunctionalOperationContract

getSpecifiedIn
```
public KeYJavaType getSpecifiedIn()
```
Specified by:

getSpecifiedIn in interface FunctionalOperationContract

getOrigVars
```
public Contract.OriginalVariables getOrigVars()
```
Description copied from interface: Contract

Returns the original ProgramVariables to replace them easier. The second list consists of the parameters.

Specified by:

getOrigVars in interface Contract

Class FunctionalOperationContractImpl

Nested Class Summary

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

Field Summary

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

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

TB

services

baseName

name

kjt

pm

specifiedIn

modality

originalPres

originalFreePres

originalMby

originalPosts

originalFreePosts

originalAxioms

originalMods

originalDeps

originalSelfVar

originalParamVars

originalResultVar

originalExcVar

originalAtPreVars

globalDefs

id

transaction

toBeSaved

hasRealModifiesClause

Constructor Detail

FunctionalOperationContractImpl

Method Detail

getReplaceMap

getReplaceMap

getReplaceMap

getReplaceMap

addGhostParams

addGhostParamTerms

getName

id

getKJT

getTarget

hasMby

getPre

getPre

getPre

getPre

getFreePre

getFreePre

getFreePre

getRequires

getEnsures

getAssignable

getAccessible

getMby

getMby

getPlainText

getHTMLText

getText

getText

getText

toBeSaved

proofToString

getModality

getPost

getPost

getPost

getPost

getFreePost

getFreePost

getFreePost

getRepresentsAxiom

getRepresentsAxiom