de.uka.ilkd.key.speclang

Class AbstractAuxiliaryContractImpl

java.lang.Object

de.uka.ilkd.key.speclang.AbstractAuxiliaryContractImpl

All Implemented Interfaces:

AuxiliaryContract, SpecificationElement

Direct Known Subclasses:

BlockContractImpl, LoopContractImpl

public abstract class AbstractAuxiliaryContractImpl
extends java.lang.Object
implements AuxiliaryContract

Abstract base class for all default implementations of the sub-interfaces of AuxiliaryContract.

Author:

wacker, lanzinger

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected static class	AbstractAuxiliaryContractImpl.Combinator<T extends AuxiliaryContract> This class is used to to combine multiple contracts for the same block and apply them simultaneously.
protected static class	AbstractAuxiliaryContractImpl.Creator<T extends AuxiliaryContract> This class contains a builder method for AbstractAuxiliaryContractImpls (AbstractAuxiliaryContractImpl.Creator.create()).
private static class	AbstractAuxiliaryContractImpl.ReplacementMap<S extends Sorted> A map from some type to the same type.
private static class	AbstractAuxiliaryContractImpl.TermReplacementMap A replacement map for terms.
private static class	AbstractAuxiliaryContractImpl.VariableReplacementMap A replacement map for variables.

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

AuxiliaryContract.Terms, AuxiliaryContract.Variables, AuxiliaryContract.VariablesCreator

Field Summary

Fields

Modifier and Type	Field and Description
protected java.lang.String	baseName
protected StatementBlock	block
private ImmutableSet<FunctionalAuxiliaryContract<?>>	functionalContracts
protected java.util.Map<LocationVariable,java.lang.Boolean>	hasMod
protected ImmutableList<InfFlowSpec>	infFlowSpecs
protected Term	instantiationSelf
protected java.util.List<Label>	labels
protected Term	measuredBy
protected IProgramMethod	method
protected Modality	modality
protected java.util.Map<LocationVariable,Term>	modifiesClauses
protected java.util.Map<LocationVariable,Term>	postconditions
protected java.util.Map<LocationVariable,Term>	preconditions
protected boolean	transactionApplicable
protected AuxiliaryContract.Variables	variables

Constructor Summary

Constructors

Constructor and Description

AbstractAuxiliaryContractImpl(java.lang.String baseName, StatementBlock block, java.util.List<Label> labels, IProgramMethod method, Modality modality, java.util.Map<LocationVariable,Term> preconditions, Term measuredBy, java.util.Map<LocationVariable,Term> postconditions, java.util.Map<LocationVariable,Term> modifiesClauses, ImmutableList<InfFlowSpec> infFlowSpecs, AuxiliaryContract.Variables variables, boolean transactionApplicable, java.util.Map<LocationVariable,java.lang.Boolean> hasMod, ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts)

Method Summary

Modifier and Type	Method and Description
protected java.util.Map<ProgramVariable,ProgramVariable>	createReplacementMap(AuxiliaryContract.Variables newVariables, Services services)
protected java.util.Map<Term,Term>	createReplacementMap(Term newHeap, AuxiliaryContract.Terms newTerms, Services services)
boolean	equals(java.lang.Object obj)
Term	getAssignable(LocationVariable heap)
java.lang.String	getBaseName()
StatementBlock	getBlock()
Term	getEnsures(LocationVariable heap)
ImmutableSet<FunctionalAuxiliaryContract<?>>	getFunctionalContracts()
private java.lang.String	getHtmlMods(LocationVariable baseHeap, HeapLDT heapLDT, Services services)
private java.lang.String	getHtmlPosts(LocationVariable baseHeap, HeapLDT heapLDT, Services services)
private java.lang.String	getHtmlPres(LocationVariable baseHeap, HeapLDT heapLDT, Services services)
java.lang.String	getHtmlText(Services services)
ImmutableList<InfFlowSpec>	getInfFlowSpecs()
Term	getInstantiationSelfTerm()
Term	getInstantiationSelfTerm(TermServices services)
KeYJavaType	getKJT() Returns the KeYJavaType representing the class/interface to which the specification element belongs.
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.
private java.lang.String	getPlainMods(Term self, LocationVariable baseHeap, HeapLDT heapLDT, Services services)
private java.lang.String	getPlainPosts(AuxiliaryContract.Terms terms, LocationVariable baseHeap, HeapLDT heapLDT, Services services)
private java.lang.String	getPlainPres(AuxiliaryContract.Terms terms, LocationVariable baseHeap, HeapLDT heapLDT, Services services)
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()
Term	getTerm(Term term, AuxiliaryContract.Variables variables, Services services) Replaces variables in a map of terms
Term	getTerm(Term term, Term heap, AuxiliaryContract.Terms terms, Services services) Replaces variables in a map of terms
AuxiliaryContract.Variables	getVariables()
AuxiliaryContract.Terms	getVariablesAsTerms(Services services)
VisibilityModifier	getVisibility() Returns the visibility of the invariant (null for default visibility)
int	hashCode()
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()
void	setFunctionalContract(FunctionalAuxiliaryContract<?> contract)
void	setInstantiationSelf(Term selfInstantiation)

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait

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

getUniqueName, setBlock, setTarget, visit

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

getDisplayName, getName

Field Detail

block

protected final StatementBlock block

See Also:

getBlock()

labels

protected final java.util.List<Label> labels

See Also:

getLabels()

method

protected final IProgramMethod method

See Also:

getMethod()

modality

protected final Modality modality

See Also:

getModality()

instantiationSelf

protected Term instantiationSelf

See Also:

getInstantiationSelfTerm()

preconditions

protected final java.util.Map<LocationVariable,Term> preconditions

See Also:

getPrecondition(LocationVariable, Services)

measuredBy

protected final Term measuredBy

See Also:

getMby()

postconditions

protected final java.util.Map<LocationVariable,Term> postconditions

See Also:

getPostcondition(LocationVariable, Services)

modifiesClauses

protected final java.util.Map<LocationVariable,Term> modifiesClauses

See Also:

getModifiesClause(LocationVariable, Services)

infFlowSpecs

protected ImmutableList<InfFlowSpec> infFlowSpecs

See Also:

getInfFlowSpecs()

variables

protected final AuxiliaryContract.Variables variables

See Also:

getVariables()

transactionApplicable

protected final boolean transactionApplicable

See Also:

isTransactionApplicable()

hasMod

protected final java.util.Map<LocationVariable,java.lang.Boolean> hasMod

See Also:

hasModifiesClause(LocationVariable)

baseName

protected final java.lang.String baseName

See Also:

getBaseName()

functionalContracts

private ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts

See Also:

AuxiliaryContract.getFunctionalContracts()

Constructor Detail

AbstractAuxiliaryContractImpl

public AbstractAuxiliaryContractImpl(java.lang.String baseName,
                                     StatementBlock block,
                                     java.util.List<Label> labels,
                                     IProgramMethod method,
                                     Modality modality,
                                     java.util.Map<LocationVariable,Term> preconditions,
                                     Term measuredBy,
                                     java.util.Map<LocationVariable,Term> postconditions,
                                     java.util.Map<LocationVariable,Term> modifiesClauses,
                                     ImmutableList<InfFlowSpec> infFlowSpecs,
                                     AuxiliaryContract.Variables variables,
                                     boolean transactionApplicable,
                                     java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
                                     ImmutableSet<FunctionalAuxiliaryContract<?>> functionalContracts)

Parameters:

baseName - the base name.

block - the block this contract belongs to.

labels - all labels belonging to the block.

method - the method containing the block.

modality - this contract's modality.

preconditions - this contract's preconditions on every heap.

measuredBy - this contract's measured-by term.

postconditions - this contract's postconditions on every heap.

modifiesClauses - this contract's modifies clauses on every heap.

infFlowSpecs - this contract's information flow specifications.

variables - this contract's variables.

transactionApplicable - whether or not this contract is applicable for transactions.

hasMod - a map specifying on which heaps this contract has a modified clause.

functionalContracts - the functional contracts corresponding to this contract.

Method Detail

getBaseName

public java.lang.String getBaseName()

Specified by:

getBaseName in interface AuxiliaryContract

Returns:

this contract's base name.

getBlock

public StatementBlock getBlock()

Specified by:

getBlock in interface AuxiliaryContract

Returns:

the block this contract belongs to.

getLabels

public java.util.List<Label> getLabels()

Specified by:

getLabels in interface AuxiliaryContract

Returns:

all labels belonging to AuxiliaryContract.getBlock()

getMethod

public IProgramMethod getMethod()

Specified by:

getMethod in interface AuxiliaryContract

Returns:

the method containing AuxiliaryContract.getBlock()

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

getModality

public Modality getModality()

Specified by:

getModality in interface AuxiliaryContract

Returns:

this contract's modality.

getPlaceholderVariables

public AuxiliaryContract.Variables getPlaceholderVariables()

Description copied from interface: AuxiliaryContract

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.

Specified by:

getPlaceholderVariables in interface AuxiliaryContract

Returns:

the placeholder variables used created during this contracts instantiation.

See Also:

AuxiliaryContractBuilders.VariablesCreatorAndRegistrar

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

isTransactionApplicable

public boolean isTransactionApplicable()

Specified by:

isTransactionApplicable in interface AuxiliaryContract

Returns:

true if and only if this contract is applicable for transactions.

isReadOnly

public boolean isReadOnly(Services services)

Specified by:

isReadOnly in interface AuxiliaryContract

Parameters:

services - services.

Returns:

true if and only if this contract is read-only.

hasModifiesClause

public boolean hasModifiesClause(LocationVariable heap)

Description copied from interface: AuxiliaryContract

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 AuxiliaryContract

Parameters:

heap - the heap to use.

Returns:

whether this contract is strictly pure.

getVariables

public AuxiliaryContract.Variables getVariables()

Specified by:

getVariables in interface AuxiliaryContract

Returns:

the original used variables like self, result etc..

getVariablesAsTerms

public AuxiliaryContract.Terms getVariablesAsTerms(Services services)

Specified by:

getVariablesAsTerms in interface AuxiliaryContract

Parameters:

services - services.

Returns:

the original used variables like self, result etc. as terms.

getTerm

public Term getTerm(Term term,
                    AuxiliaryContract.Variables variables,
                    Services services)

Replaces variables in a map of terms

Parameters:

term - a term.

variables - replacements for getVariables()

services - services.

Returns:

the term with every occurrence of a variable from getVariables() replaced.

getTerm

public Term getTerm(Term term,
                    Term heap,
                    AuxiliaryContract.Terms terms,
                    Services services)

Replaces variables in a map of terms

Parameters:

term - a term.

heap - the replacement heap

terms - replacements for getVariables()

services - services.

Returns:

the term with every occurrence of a variable from getVariables() replaced.

getMby

public Term getMby()

Specified by:

getMby in interface AuxiliaryContract

Returns:

this contract's measured-by clause if it has one, null otherwise.

getMby

public Term getMby(AuxiliaryContract.Variables variables,
                   Services services)

Specified by:

getMby in interface AuxiliaryContract

Parameters:

variables - variables to use instead of AuxiliaryContract.getPlaceholderVariables().

services - services.

Returns:

this contract's measured-by clause if it has one, null otherwise.

getMby

public Term getMby(ProgramVariable selfVar,
                   Services services)

Specified by:

getMby in interface AuxiliaryContract

Parameters:

selfVar - the self variable to use instead of AuxiliaryContract.getPlaceholderVariables().

services - services.

Returns:

this contract's measured-by clause if it has one, null otherwise.

getMby

public Term getMby(java.util.Map<LocationVariable,Term> heapTerms,
                   Term selfTerm,
                   java.util.Map<LocationVariable,Term> atPres,
                   Services services)

Specified by:

getMby in interface AuxiliaryContract

Parameters:

heapTerms - the heaps to use.

selfTerm - the self variable to use instead of AuxiliaryContract.getPlaceholderVariables().

atPres - a map from every variable var to \old(var) to use instead of AuxiliaryContract.getPlaceholderVariables().

services - services.

Returns:

this contract's measured-by clause if it has one, null otherwise.

getPrecondition

public Term getPrecondition(LocationVariable heap,
                            ProgramVariable self,
                            java.util.Map<LocationVariable,LocationVariable> atPres,
                            Services services)

Specified by:

getPrecondition in interface AuxiliaryContract

Parameters:

heap - the heap to use.

self - the self variable to use instead of AuxiliaryContract.getPlaceholderVariables().

atPres - a map from every variable var to \old(var) to use instead of AuxiliaryContract.getPlaceholderVariables().

services - services.

Returns:

this contract's precondition on the specified heap.

getPrecondition

public Term getPrecondition(LocationVariable heapVariable,
                            Term heap,
                            Term self,
                            java.util.Map<LocationVariable,Term> atPres,
                            Services services)

Specified by:

getPrecondition in interface AuxiliaryContract

Parameters:

heapVariable - the heap to use.

heap - the heap to use.

self - the self variable to use to use instead of AuxiliaryContract.getPlaceholderVariables().

atPres - a map from every variable var to \old(var) to use instead of AuxiliaryContract.getPlaceholderVariables().

services - services.

Returns:

this contract's precondition on the specified heap.

getPrecondition

public Term getPrecondition(LocationVariable heap,
                            Services services)

Specified by:

getPrecondition in interface AuxiliaryContract

Parameters:

heap - the heap to use.

services - services.

Returns:

this contract's precondition on the specified heap.

getPrecondition

public Term getPrecondition(LocationVariable heap,
                            AuxiliaryContract.Variables variables,
                            Services services)

Specified by:

getPrecondition in interface AuxiliaryContract

Parameters:

heap - the heap to use.

variables - the variables to use instead of AuxiliaryContract.getPlaceholderVariables().

services - services.

Returns:

this contract's precondition on the specified heap with all free program variables replaced by those in variables.

getPrecondition

public Term getPrecondition(LocationVariable heapVariable,
                            Term heap,
                            AuxiliaryContract.Terms terms,
                            Services services)

Specified by:

getPrecondition in interface AuxiliaryContract

Parameters:

heapVariable - the heap to use.

heap - the heap to use.

terms - the terms to use instead of AuxiliaryContract.getPlaceholderVariables().

services - services.

Returns:

this contract's precondition on the specified heap.

getPostcondition

public Term getPostcondition(LocationVariable heap,
                             AuxiliaryContract.Variables variables,
                             Services services)

Specified by:

getPostcondition in interface AuxiliaryContract

Parameters:

heap - the heap to use.

variables - the variables to use instead of AuxiliaryContract.getPlaceholderVariables().

services - services.

Returns:

this contract's postcondition on the specified heap.

getPostcondition

public Term getPostcondition(LocationVariable heapVariable,
                             Term heap,
                             AuxiliaryContract.Terms terms,
                             Services services)

Specified by:

getPostcondition in interface AuxiliaryContract

Parameters:

heapVariable - the heap to use.

heap - the heap to use.

terms - the terms to use instead of AuxiliaryContract.getPlaceholderVariables().

services - services.

Returns:

this contract's precondition on the specified heap.

getPostcondition

public Term getPostcondition(LocationVariable heap,
                             Services services)

Specified by:

getPostcondition in interface AuxiliaryContract

Parameters:

heap - the heap to use.

services - services.

Returns:

this contract's precondition on the specified heap.

getModifiesClause

public Term getModifiesClause(LocationVariable heap,
                              ProgramVariable self,
                              Services services)

Specified by:

getModifiesClause in interface AuxiliaryContract

Parameters:

heap - the heap to use.

self - the self variable to use instead of AuxiliaryContract.getPlaceholderVariables().

services - services.

Returns:

this contract's modifies clause on the specified heap.

getModifiesClause

public Term getModifiesClause(LocationVariable heapVariable,
                              Term heap,
                              Term self,
                              Services services)

Specified by:

getModifiesClause in interface AuxiliaryContract

Parameters:

heapVariable - the heap to use.

heap - the heap to use.

self - the self variable to use instead of AuxiliaryContract.getPlaceholderVariables().

services - services.

Returns:

this contract's modifies clause on the specified heap.

getModifiesClause

public Term getModifiesClause(LocationVariable heap,
                              AuxiliaryContract.Variables variables,
                              Services services)

Specified by:

getModifiesClause in interface AuxiliaryContract

Parameters:

heap - the heap to use.

variables - the variables to use instead of AuxiliaryContract.getPlaceholderVariables().

services - services.

Returns:

this contract's modifies clause on the specified heap.

getModifiesClause

public Term getModifiesClause(LocationVariable heap,
                              Services services)

Specified by:

getModifiesClause in interface AuxiliaryContract

Parameters:

heap - the heap to use.

services - services.

Returns:

this contract's modifies clause on the specified heap.

getPre

public Term getPre(Services services)

Specified by:

getPre in interface AuxiliaryContract

Parameters:

services - services.

Returns:

the original precondition of the contract.

getRequires

public Term getRequires(LocationVariable heap)

Specified by:

getRequires in interface AuxiliaryContract

Parameters:

heap - the heap to use.

Returns:

this contract's precondition on the specified heap.

getPost

public Term getPost(Services services)

Specified by:

getPost in interface AuxiliaryContract

Parameters:

services - services.

Returns:

the original postcondition of the contract.

getEnsures

public Term getEnsures(LocationVariable heap)

Specified by:

getEnsures in interface AuxiliaryContract

Parameters:

heap - the heap to use.

Returns:

this contract's postcondition on the specified heap.

getMod

public Term getMod(Services services)

Specified by:

getMod in interface AuxiliaryContract

Parameters:

services - services.

Returns:

the original modifies clause of the contract.

getInfFlowSpecs

public ImmutableList<InfFlowSpec> getInfFlowSpecs()

Specified by:

getInfFlowSpecs in interface AuxiliaryContract

Returns:

the original information flow specification clause of the contract.

hasMby

public boolean hasMby()

Specified by:

hasMby in interface AuxiliaryContract

Returns:

true if and only if this contract has a measured-by clause.

See Also:

AuxiliaryContract.getMby()

hasInfFlowSpecs

public boolean hasInfFlowSpecs()

Specified by:

hasInfFlowSpecs in interface AuxiliaryContract

Returns:

true if and only if this contract has information flow specs.

See Also:

AuxiliaryContract.getInfFlowSpecs()

setInstantiationSelf

public void setInstantiationSelf(Term selfInstantiation)

Specified by:

setInstantiationSelf in interface AuxiliaryContract

Parameters:

selfInstantiation - the new instantiation self term.

See Also:

AuxiliaryContract.getInstantiationSelfTerm()

getInstantiationSelfTerm

public Term getInstantiationSelfTerm()

Specified by:

getInstantiationSelfTerm in interface AuxiliaryContract

Returns:

the self variable as a term.

getInstantiationSelfTerm

public Term getInstantiationSelfTerm(TermServices services)

Specified by:

getInstantiationSelfTerm in interface AuxiliaryContract

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.

getTarget

public IProgramMethod getTarget()

Specified by:

getTarget in interface AuxiliaryContract

Returns:

the method in which the block is located.

getAssignable

public Term getAssignable(LocationVariable heap)

Specified by:

getAssignable in interface AuxiliaryContract

Parameters:

heap - the heap to use.

Returns:

this contract's assignable term on the specified heap.

getHtmlText

public java.lang.String getHtmlText(Services services)

Specified by:

getHtmlText in interface AuxiliaryContract

Parameters:

services - services.

Returns:

a HTML representation of this contract.

getPlainText

public java.lang.String getPlainText(Services services)

Specified by:

getPlainText in interface AuxiliaryContract

Parameters:

services - services.

Returns:

a plain text representation of this contract.

getPlainText

public java.lang.String getPlainText(Services services,
                                     AuxiliaryContract.Terms terms)

Specified by:

getPlainText in interface AuxiliaryContract

Parameters:

services - services.

terms - the terms to use instead of AuxiliaryContract.getPlaceholderVariables().

Returns:

a plain text representation of this contract.

getOrigVars

public Contract.OriginalVariables getOrigVars()

Specified by:

getOrigVars in interface AuxiliaryContract

Returns:

the contract's variabels converted to OriginalVariables.

See Also:

AuxiliaryContract.getVariables()

equals

public boolean equals(java.lang.Object obj)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

getFunctionalContracts

public ImmutableSet<FunctionalAuxiliaryContract<?>> getFunctionalContracts()

Specified by:

getFunctionalContracts in interface AuxiliaryContract

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

public void setFunctionalContract(FunctionalAuxiliaryContract<?> contract)

Specified by:

setFunctionalContract in interface AuxiliaryContract

Parameters:

contract - the new functional contract.

See Also:

AuxiliaryContract.getFunctionalContracts()

createReplacementMap

protected java.util.Map<ProgramVariable,ProgramVariable> createReplacementMap(AuxiliaryContract.Variables newVariables,
                                                                              Services services)

Parameters:

newVariables - new variables.

services - services.

Returns:

a map from every variable in getVariables() to its counterpart in newVariables.

createReplacementMap

protected java.util.Map<Term,Term> createReplacementMap(Term newHeap,
                                                        AuxiliaryContract.Terms newTerms,
                                                        Services services)

Parameters:

newHeap - new base heap.

newTerms - new terms.

services - services.

Returns:

a map from every term in getVariables().termify() to its counterpart in newTerms, and from the base heap to heap.

getHtmlMods

private java.lang.String getHtmlMods(LocationVariable baseHeap,
                                     HeapLDT heapLDT,
                                     Services services)

Parameters:

baseHeap - base heap.

heapLDT - heap LDT.

services - services.

Returns:

a HTML representation of this contract's modifies clauses.

getHtmlPres

private java.lang.String getHtmlPres(LocationVariable baseHeap,
                                     HeapLDT heapLDT,
                                     Services services)

Parameters:

baseHeap - base heap.

heapLDT - heap LDT.

services - services.

Returns:

a HTML representation of this contract's preconditions.

getHtmlPosts

private java.lang.String getHtmlPosts(LocationVariable baseHeap,
                                      HeapLDT heapLDT,
                                      Services services)

Parameters:

baseHeap - base heap.

heapLDT - heap LDT.

services - services.

Returns:

a HTML representation of this contract's postconditions.

getPlainMods

private java.lang.String getPlainMods(Term self,
                                      LocationVariable baseHeap,
                                      HeapLDT heapLDT,
                                      Services services)

Parameters:

self - the self term

baseHeap - base heap.

heapLDT - heap LDT.

services - services.

Returns:

a plain text representation of this contract's modifies clauses.

getPlainPres

private java.lang.String getPlainPres(AuxiliaryContract.Terms terms,
                                      LocationVariable baseHeap,
                                      HeapLDT heapLDT,
                                      Services services)

Parameters:

terms - the terms to use.

baseHeap - base heap.

heapLDT - heap LDT.

services - services.

Returns:

a plain text representation of this contract's preconditions.

getPlainPosts

private java.lang.String getPlainPosts(AuxiliaryContract.Terms terms,
                                       LocationVariable baseHeap,
                                       HeapLDT heapLDT,
                                       Services services)

Parameters:

terms - the terms to use.

baseHeap - base heap.

heapLDT - heap LDT.

services - services.

Returns:

a plain text representation of this contract's postconditions.