AuxiliaryContract (KeY API Documentation)

All Superinterfaces:

SpecificationElement

All Known Subinterfaces:

BlockContract, LoopContract

All Known Implementing Classes:

AbstractAuxiliaryContractImpl, BlockContractImpl, LoopContractImpl
```
public interface AuxiliaryContract
extends SpecificationElement
```
Super-interface for BlockContract and LoopContract.

Author:

wacker, lanzinger

Nested Class Summary

Nested Classes
Modifier and Type	Interface and Description
`static class`	`AuxiliaryContract.Terms`
`static class`	`AuxiliaryContract.Variables` This class contains all new variables that are introduced during a `AuxiliaryContract`'s instantiation.
`static class`	`AuxiliaryContract.VariablesCreator`

Method Summary

All Methods Instance Methods Abstract Methods
Modifier and Type	Method and Description
`Term`	`getAssignable(LocationVariable heap)`
`java.lang.String`	`getBaseName()`
`StatementBlock`	`getBlock()`
`Term`	`getEnsures(LocationVariable heap)`
`ImmutableSet<FunctionalAuxiliaryContract<?>>`	`getFunctionalContracts()`
`java.lang.String`	`getHtmlText(Services services)`
`ImmutableList<InfFlowSpec>`	`getInfFlowSpecs()`
`Term`	`getInstantiationSelfTerm()`
`Term`	`getInstantiationSelfTerm(TermServices services)`
`java.util.List<Label>`	`getLabels()`
`Term`	`getMby()`
`Term`	`getMby(AuxiliaryContract.Variables variables, Services services)`
`Term`	`getMby(java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, java.util.Map<LocationVariable,Term> atPres, Services services)`
`Term`	`getMby(ProgramVariable selfVar, Services services)`
`IProgramMethod`	`getMethod()`
`Term`	`getMod(Services services)`
`Modality`	`getModality()`
`Term`	`getModifiesClause(LocationVariable heap, AuxiliaryContract.Variables variables, Services services)`
`Term`	`getModifiesClause(LocationVariable heap, ProgramVariable self, Services services)`
`Term`	`getModifiesClause(LocationVariable heap, Services services)`
`Term`	`getModifiesClause(LocationVariable heapVariable, Term heap, Term self, Services services)`
`Contract.OriginalVariables`	`getOrigVars()`
`AuxiliaryContract.Variables`	`getPlaceholderVariables()` Returns the set of placeholder variables created during this contract's instantiation.
`java.lang.String`	`getPlainText(Services services)`
`java.lang.String`	`getPlainText(Services services, AuxiliaryContract.Terms terms)`
`Term`	`getPost(Services services)`
`Term`	`getPostcondition(LocationVariable heap, AuxiliaryContract.Variables variables, Services services)`
`Term`	`getPostcondition(LocationVariable heap, Services services)`
`Term`	`getPostcondition(LocationVariable heapVariable, Term heap, AuxiliaryContract.Terms terms, Services services)`
`Term`	`getPre(Services services)`
`Term`	`getPrecondition(LocationVariable heap, AuxiliaryContract.Variables variables, Services services)`
`Term`	`getPrecondition(LocationVariable heap, ProgramVariable self, java.util.Map<LocationVariable,LocationVariable> atPres, Services services)`
`Term`	`getPrecondition(LocationVariable heap, Services services)`
`Term`	`getPrecondition(LocationVariable heapVariable, Term heap, AuxiliaryContract.Terms terms, Services services)`
`Term`	`getPrecondition(LocationVariable heapVariable, Term heap, Term self, java.util.Map<LocationVariable,Term> atPres, Services services)`
`Term`	`getRequires(LocationVariable heap)`
`IProgramMethod`	`getTarget()`
`java.lang.String`	`getUniqueName()`
`AuxiliaryContract.Variables`	`getVariables()`
`AuxiliaryContract.Terms`	`getVariablesAsTerms(Services services)`
`boolean`	`hasInfFlowSpecs()`
`boolean`	`hasMby()`
`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`	`isReadOnly(Services services)`
`boolean`	`isTransactionApplicable()`
`AuxiliaryContract`	`setBlock(StatementBlock newBlock)`
`void`	`setFunctionalContract(FunctionalAuxiliaryContract<?> contract)`
`void`	`setInstantiationSelf(Term selfInstantiation)`
`AuxiliaryContract`	`setTarget(KeYJavaType newKJT, IObserverFunction newPM)`
`void`	`visit(Visitor visitor)` Accepts a visitor.

Methods inherited from interface de.uka.ilkd.key.speclang.SpecificationElement
getDisplayName, getKJT, getName, getVisibility

- Method Detail
  - getFunctionalContracts
```
ImmutableSet<FunctionalAuxiliaryContract<?>> getFunctionalContracts()
```
    Returns:
    
    all FunctionalAuxiliaryContracts with a valid id that correspond to this BlockSpecificationElement. Unless this contract is a combination of other contracts, the resulting set will only contain one element.
  - setFunctionalContract
```
void setFunctionalContract(FunctionalAuxiliaryContract<?> contract)
```
    Parameters:
    
    contract - the new functional contract.
    
    See Also:
    
    getFunctionalContracts()
  - getBlock
```
StatementBlock getBlock()
```
    Returns:
    
    the block this contract belongs to.
  - getLabels
```
java.util.List<Label> getLabels()
```
    Returns:
    
    all labels belonging to getBlock()
  - getMethod
```
IProgramMethod getMethod()
```
    Returns:
    
    the method containing getBlock()
  - getModality
```
Modality getModality()
```
    Returns:
    
    this contract's modality.
  - getPlaceholderVariables
```
AuxiliaryContract.Variables getPlaceholderVariables()
```
    Returns the set of placeholder variables created during this contract's instantiation. These are replaced by the real variables with the same names when the contract is applied.
    
    Returns:
    
    the placeholder variables used created during this contracts instantiation.
    
    See Also:
    
    AuxiliaryContractBuilders.VariablesCreatorAndRegistrar
  - isTransactionApplicable
```
boolean isTransactionApplicable()
```
    Returns:
    
    true if and only if this contract is applicable for transactions.
  - isReadOnly
```
boolean isReadOnly(Services services)
```
    Parameters:
    
    services - services.
    
    Returns:
    
    true if and only if this contract is read-only.
  - getBaseName
```
java.lang.String getBaseName()
```
    Returns:
    
    this contract's base name.
  - getUniqueName
```
java.lang.String getUniqueName()
```
    Returns:
    
    this contract's unique name.
  - hasModifiesClause
```
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."
    
    Parameters:
    
    heap - the heap to use.
    
    Returns:
    
    whether this contract is strictly pure.
  - getInstantiationSelfTerm
```
Term getInstantiationSelfTerm()
```
    Returns:
    
    the self variable as a term.
  - getPrecondition
```
Term getPrecondition(LocationVariable heap,
                     Services services)
```
    Parameters:
    
    heap - the heap to use.
    
    services - services.
    
    Returns:
    
    this contract's precondition on the specified heap.
  - getPrecondition
```
Term getPrecondition(LocationVariable heap,
                     AuxiliaryContract.Variables variables,
                     Services services)
```
    Parameters:
    
    heap - the heap to use.
    
    variables - the variables to use instead of getPlaceholderVariables().
    
    services - services.
    
    Returns:
    
    this contract's precondition on the specified heap with all free program variables replaced by those in variables.
  - getPrecondition
```
Term getPrecondition(LocationVariable heap,
                     ProgramVariable self,
                     java.util.Map<LocationVariable,LocationVariable> atPres,
                     Services services)
```
    Parameters:
    
    heap - the heap to use.
    
    self - the self variable to use instead of getPlaceholderVariables().
    
    atPres - a map from every variable var to \old(var) to use instead of getPlaceholderVariables().
    
    services - services.
    
    Returns:
    
    this contract's precondition on the specified heap.
  - getPrecondition
```
Term getPrecondition(LocationVariable heapVariable,
                     Term heap,
                     Term self,
                     java.util.Map<LocationVariable,Term> atPres,
                     Services services)
```
    Parameters:
    
    heapVariable - the heap to use.
    
    heap - the heap to use.
    
    self - the self variable to use to use instead of getPlaceholderVariables().
    
    atPres - a map from every variable var to \old(var) to use instead of getPlaceholderVariables().
    
    services - services.
    
    Returns:
    
    this contract's precondition on the specified heap.
  - getPrecondition
```
Term getPrecondition(LocationVariable heapVariable,
                     Term heap,
                     AuxiliaryContract.Terms terms,
                     Services services)
```
    Parameters:
    
    heapVariable - the heap to use.
    
    heap - the heap to use.
    
    terms - the terms to use instead of getPlaceholderVariables().
    
    services - services.
    
    Returns:
    
    this contract's precondition on the specified heap.
  - getPostcondition
```
Term getPostcondition(LocationVariable heap,
                      AuxiliaryContract.Variables variables,
                      Services services)
```
    Parameters:
    
    heap - the heap to use.
    
    variables - the variables to use instead of getPlaceholderVariables().
    
    services - services.
    
    Returns:
    
    this contract's postcondition on the specified heap.
  - getPostcondition
```
Term getPostcondition(LocationVariable heapVariable,
                      Term heap,
                      AuxiliaryContract.Terms terms,
                      Services services)
```
    Parameters:
    
    heapVariable - the heap to use.
    
    heap - the heap to use.
    
    terms - the terms to use instead of getPlaceholderVariables().
    
    services - services.
    
    Returns:
    
    this contract's precondition on the specified heap.
  - getPostcondition
```
Term getPostcondition(LocationVariable heap,
                      Services services)
```
    Parameters:
    
    heap - the heap to use.
    
    services - services.
    
    Returns:
    
    this contract's precondition on the specified heap.
  - getModifiesClause
```
Term getModifiesClause(LocationVariable heap,
                       ProgramVariable self,
                       Services services)
```
    Parameters:
    
    heap - the heap to use.
    
    self - the self variable to use instead of getPlaceholderVariables().
    
    services - services.
    
    Returns:
    
    this contract's modifies clause on the specified heap.
  - getModifiesClause
```
Term getModifiesClause(LocationVariable heapVariable,
                       Term heap,
                       Term self,
                       Services services)
```
    Parameters:
    
    heapVariable - the heap to use.
    
    heap - the heap to use.
    
    self - the self variable to use instead of getPlaceholderVariables().
    
    services - services.
    
    Returns:
    
    this contract's modifies clause on the specified heap.
  - getModifiesClause
```
Term getModifiesClause(LocationVariable heap,
                       AuxiliaryContract.Variables variables,
                       Services services)
```
    Parameters:
    
    heap - the heap to use.
    
    variables - the variables to use instead of getPlaceholderVariables().
    
    services - services.
    
    Returns:
    
    this contract's modifies clause on the specified heap.
  - getModifiesClause
```
Term getModifiesClause(LocationVariable heap,
                       Services services)
```
    Parameters:
    
    heap - the heap to use.
    
    services - services.
    
    Returns:
    
    this contract's modifies clause on the specified heap.
  - getRequires
```
Term getRequires(LocationVariable heap)
```
    Parameters:
    
    heap - the heap to use.
    
    Returns:
    
    this contract's precondition on the specified heap.
  - getEnsures
```
Term getEnsures(LocationVariable heap)
```
    Parameters:
    
    heap - the heap to use.
    
    Returns:
    
    this contract's postcondition on the specified heap.
  - getAssignable
```
Term getAssignable(LocationVariable heap)
```
    Parameters:
    
    heap - the heap to use.
    
    Returns:
    
    this contract's assignable term on the specified heap.
  - visit
```
void visit(Visitor visitor)
```
    Accepts a visitor.
    
    Parameters:
    
    visitor - the visitor to accept.
  - getHtmlText
```
java.lang.String getHtmlText(Services services)
```
    Parameters:
    
    services - services.
    
    Returns:
    
    a HTML representation of this contract.
  - getPlainText
```
java.lang.String getPlainText(Services services)
```
    Parameters:
    
    services - services.
    
    Returns:
    
    a plain text representation of this contract.
  - getPlainText
```
java.lang.String getPlainText(Services services,
                              AuxiliaryContract.Terms terms)
```
    Parameters:
    
    services - services.
    
    terms - the terms to use instead of getPlaceholderVariables().
    
    Returns:
    
    a plain text representation of this contract.
  - getTarget
```
IProgramMethod getTarget()
```
    Returns:
    
    the method in which the block is located.
  - hasMby
```
boolean hasMby()
```
    Returns:
    
    true if and only if this contract has a measured-by clause.
    
    See Also:
    
    getMby()
  - getMby
```
Term getMby()
```
    Returns:
    
    this contract's measured-by clause if it has one, null otherwise.
  - getMby
```
Term getMby(AuxiliaryContract.Variables variables,
            Services services)
```
    Parameters:
    
    variables - variables to use instead of getPlaceholderVariables().
    
    services - services.
    
    Returns:
    
    this contract's measured-by clause if it has one, null otherwise.
  - getMby
```
Term getMby(ProgramVariable selfVar,
            Services services)
```
    Parameters:
    
    selfVar - the self variable to use instead of getPlaceholderVariables().
    
    services - services.
    
    Returns:
    
    this contract's measured-by clause if it has one, null otherwise.
  - getMby
```
Term getMby(java.util.Map<LocationVariable,Term> heapTerms,
            Term selfTerm,
            java.util.Map<LocationVariable,Term> atPres,
            Services services)
```
    Parameters:
    
    heapTerms - the heaps to use.
    
    selfTerm - the self variable to use instead of getPlaceholderVariables().
    
    atPres - a map from every variable var to \old(var) to use instead of getPlaceholderVariables().
    
    services - services.
    
    Returns:
    
    this contract's measured-by clause if it has one, null otherwise.
  - hasInfFlowSpecs
```
boolean hasInfFlowSpecs()
```
    Returns:
    
    true if and only if this contract has information flow specs.
    
    See Also:
    
    getInfFlowSpecs()
  - setInstantiationSelf
```
void setInstantiationSelf(Term selfInstantiation)
```
    Parameters:
    
    selfInstantiation - the new instantiation self term.
    
    See Also:
    
    getInstantiationSelfTerm()
  - getInstantiationSelfTerm
```
Term getInstantiationSelfTerm(TermServices services)
```
    Parameters:
    
    services - services.
    
    Returns:
    
    the term internally used for self or a newly instantiated one. Use with care - it is likely that this is *not* the right "self" for you.
  - getPre
```
Term getPre(Services services)
```
    Parameters:
    
    services - services.
    
    Returns:
    
    the original precondition of the contract.
  - getPost
```
Term getPost(Services services)
```
    Parameters:
    
    services - services.
    
    Returns:
    
    the original postcondition of the contract.
  - getMod
```
Term getMod(Services services)
```
    Parameters:
    
    services - services.
    
    Returns:
    
    the original modifies clause of the contract.
  - getInfFlowSpecs
```
ImmutableList<InfFlowSpec> getInfFlowSpecs()
```
    Returns:
    
    the original information flow specification clause of the contract.
  - getVariables
```
AuxiliaryContract.Variables getVariables()
```
    Returns:
    
    the original used variables like self, result etc..
  - setTarget
```
AuxiliaryContract setTarget(KeYJavaType newKJT,
                            IObserverFunction newPM)
```
    Parameters:
    
    newKJT - the type containing the new target method.
    
    newPM - the new target method.
    
    Returns:
    
    a contract equal to this one except that it belongs to a different target.
  - setBlock
```
AuxiliaryContract setBlock(StatementBlock newBlock)
```
    Parameters:
    
    newBlock - the new block.
    
    Returns:
    
    a contract equal to this one except that it belongs to a different block.
  - getVariablesAsTerms
```
AuxiliaryContract.Terms getVariablesAsTerms(Services services)
```
    Parameters:
    
    services - services.
    
    Returns:
    
    the original used variables like self, result etc. as terms.
  - getOrigVars
```
Contract.OriginalVariables getOrigVars()
```
    Returns:
    
    the contract's variabels converted to OriginalVariables.
    
    See Also:
    
    getVariables()

Interface AuxiliaryContract

Nested Class Summary

Method Summary

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

Method Detail

getFunctionalContracts

setFunctionalContract

getBlock

getLabels

getMethod

getModality

getPlaceholderVariables

isTransactionApplicable

isReadOnly

getBaseName

getUniqueName

hasModifiesClause

getInstantiationSelfTerm

getPrecondition

getPrecondition

getPrecondition

getPrecondition

getPrecondition

getPostcondition

getPostcondition

getPostcondition

getModifiesClause

getModifiesClause

getModifiesClause

getModifiesClause

getRequires

getEnsures

getAssignable

visit

getHtmlText

getPlainText

getPlainText

getTarget

hasMby

getMby

getMby

getMby

getMby

hasInfFlowSpecs

setInstantiationSelf

getInstantiationSelfTerm

getPre

getPost

getMod

getInfFlowSpecs

getVariables

setTarget

setBlock

getVariablesAsTerms

getOrigVars