de.uka.ilkd.key.speclang

Class DependencyContractImpl

java.lang.Object

de.uka.ilkd.key.speclang.DependencyContractImpl

All Implemented Interfaces:

Contract, DependencyContract, SpecificationElement

public final class DependencyContractImpl
extends java.lang.Object
implements DependencyContract

Standard implementation of the DependencyContract 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) int	id
(package private) KeYJavaType	kjt
(package private) java.lang.String	name
(package private) java.util.Map<LocationVariable,? extends ProgramVariable>	originalAtPreVars
(package private) java.util.Map<ProgramVariable,Term>	originalDeps
(package private) Term	originalMby
(package private) ImmutableList<ProgramVariable>	originalParamVars
(package private) java.util.Map<LocationVariable,Term>	originalPres
(package private) ProgramVariable	originalSelfVar
(package private) KeYJavaType	specifiedIn
(package private) IObserverFunction	target

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

INVALID_ID

Constructor Summary

Constructors

Constructor and Description
DependencyContractImpl(java.lang.String baseName, KeYJavaType kjt, IObserverFunction target, KeYJavaType specifiedIn, java.util.Map<LocationVariable,Term> pres, Term mby, java.util.Map<ProgramVariable,Term> deps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars) Deprecated.
DependencyContractImpl(java.lang.String baseName, java.lang.String name, KeYJavaType kjt, IObserverFunction target, KeYJavaType specifiedIn, java.util.Map<LocationVariable,Term> pres, Term mby, java.util.Map<ProgramVariable,Term> deps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Term globalDefs, int id)

Method Summary

Modifier and Type	Method and Description
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)
Term	getAssignable(LocationVariable heap)
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	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.
java.lang.String	getName() Returns the unique internal name of the specification element.
Contract.OriginalVariables	getOrigVars() Returns the original ProgramVariables to replace them easier.
java.lang.String	getPlainText(Services services) Returns the contract in pretty plain text format.
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.
Term	getRequires(LocationVariable heap)
IObserverFunction	getTarget() Returns the contracted function symbol.
private java.lang.String	getText(boolean includeHtmlMarkup, Services services)
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	hasSelfVar() Checks if a self variable is originally provided.
int	id() Returns the id number of the contract.
java.lang.String	proofToString(Services services) Returns a parseable String representation of the contract.
DependencyContract	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

baseName

final java.lang.String baseName

name

final java.lang.String name

kjt

final KeYJavaType kjt

target

final IObserverFunction target

specifiedIn

final KeYJavaType specifiedIn

originalPres

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

originalMby

final Term originalMby

originalDeps

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

originalSelfVar

final ProgramVariable originalSelfVar

originalParamVars

final ImmutableList<ProgramVariable> originalParamVars

originalAtPreVars

final java.util.Map<LocationVariable,? extends ProgramVariable> originalAtPreVars

globalDefs

final Term globalDefs

id

final int id

Constructor Detail

DependencyContractImpl

DependencyContractImpl(java.lang.String baseName,
                       java.lang.String name,
                       KeYJavaType kjt,
                       IObserverFunction target,
                       KeYJavaType specifiedIn,
                       java.util.Map<LocationVariable,Term> pres,
                       Term mby,
                       java.util.Map<ProgramVariable,Term> deps,
                       ProgramVariable selfVar,
                       ImmutableList<ProgramVariable> paramVars,
                       java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
                       Term globalDefs,
                       int id)

DependencyContractImpl

@Deprecated
DependencyContractImpl(java.lang.String baseName,
                                   KeYJavaType kjt,
                                   IObserverFunction target,
                                   KeYJavaType specifiedIn,
                                   java.util.Map<LocationVariable,Term> pres,
                                   Term mby,
                                   java.util.Map<ProgramVariable,Term> deps,
                                   ProgramVariable selfVar,
                                   ImmutableList<ProgramVariable> paramVars,
                                   java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars)

Deprecated.

Method Detail

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 IObserverFunction getTarget()

Description copied from interface: Contract

Returns the contracted function symbol.

Specified by:

getTarget in interface Contract

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

getRequires

public Term getRequires(LocationVariable heap)

Specified by:

getRequires in interface Contract

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

Specified by:

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

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

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

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

createProofObl

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

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

setID

public DependencyContract 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.

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