de.uka.ilkd.key.speclang

Class InformationFlowContractImpl

java.lang.Object

de.uka.ilkd.key.speclang.InformationFlowContractImpl

All Implemented Interfaces:

Contract, InformationFlowContract, SpecificationElement

public final class InformationFlowContractImpl
extends java.lang.Object
implements InformationFlowContract

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
private java.lang.String	baseName
private KeYJavaType	forClass
(package private) boolean	hasRealModifiesClause If a method is strictly pure, it has no modifies clause which could anonymised.
private int	id
private Modality	modality
private java.lang.String	name
private Term	origAtPre
private Term	origDep
private Term	origExc
private ImmutableList<InfFlowSpec>	origInfFlowSpecs
private Term	origMby
private Term	origMod
private ImmutableList<Term>	origParams
private Term	origPre
private Term	origResult
private Term	origSelf
private IProgramMethod	pm
private KeYJavaType	specifiedIn
private boolean	toBeSaved

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

INVALID_ID

Constructor Summary

Constructors

Modifier	Constructor and Description
	InformationFlowContractImpl(java.lang.String baseName, KeYJavaType forClass, IProgramMethod pm, KeYJavaType specifiedIn, Modality modality, Term pre, Term mby, Term mod, boolean hasRealMod, Term self, ImmutableList<Term> params, Term result, Term exc, Term heapAtPre, Term dep, ImmutableList<InfFlowSpec> infFlowSpecs, boolean toBeSaved)
protected	InformationFlowContractImpl(java.lang.String baseName, java.lang.String name, KeYJavaType forClass, IProgramMethod pm, KeYJavaType specifiedIn, Modality modality, Term pre, Term mby, Term mod, boolean hasRealMod, Term self, ImmutableList<Term> params, Term result, Term exc, Term heapAtPre, Term dep, ImmutableList<InfFlowSpec> infFlowSpecs, boolean toBeSaved, 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.
boolean	equals(Contract c)
Term	getAccessible(ProgramVariable heap)
Term	getAssignable(LocationVariable heap)
Term	getAtPre()
java.lang.String	getBaseName()
Term	getDep() Returns the dependency set of the contract.
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	getExc() Get the exception-variable which is used in this contract.
Term	getGlobalDefs()
Term	getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
java.lang.String	getHTMLBody(Services services)
private java.lang.String	getHTMLFor(ImmutableList<InfFlowSpec> originalInfFlowSpecs, java.lang.String htmlName, Services services)
private java.lang.String	getHTMLFor(java.lang.Iterable<Term> originalTerms, Services services)
protected java.lang.String	getHTMLFor(Term originalTerm, java.lang.String htmlName, Services services)
private java.lang.String	getHTMLSignature()
private java.lang.StringBuffer	getHTMLSignatureBody()
java.lang.String	getHTMLText(Services services) Returns the contract in pretty HTML format.
ImmutableList<InfFlowSpec>	getInfFlowSpecs() Returns the set of views.
KeYJavaType	getKJT() Returns the KeYJavaType representing the class/interface to which the specification element belongs.
Term	getMby() Returns the original measured_by clause of the contract.
Term	getMby(java.util.Map<LocationVariable,Term> heapTerms, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services) Deprecated.
Term	getMby(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services) Deprecated.
Term	getMod() Returns the original 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() Get the parameter-variables which is used in this contract.
java.lang.String	getPlainText(Services services) Returns the contract in pretty plain text format.
java.lang.String	getPODisplayName() For generating contract name of SymbolicExecutionPO
Term	getPre() Returns the original precondition of the contract.
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) Deprecated.
Term	getPre(java.util.List<LocationVariable> heapContext, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services) Deprecated.
Term	getPre(LocationVariable heap, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Services services) Deprecated.
Term	getPre(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, java.util.Map<LocationVariable,Term> atPres, Services services) Deprecated.
ProofOblInput	getProofObl(Services services) Lookup the proof obligation belonging to the contract in the specification repository.
Term	getRequires(LocationVariable heap)
Term	getResult() Get the result-variable which is used in this contract.
Term	getSelf() Get the self-variable which is used in this contract.
KeYJavaType	getSpecifiedIn()
IProgramMethod	getTarget() Returns the contracted function symbol.
java.lang.String	getTypeName() Returns technical name for the contract type.
VisibilityModifier	getVisibility() Returns the visibility of the invariant (null for default visibility)
boolean	hasInfFlowSpec()
boolean	hasMby() Tells whether the contract contains a measured_by clause.
boolean	hasModifiesClause() Returns true iff the method (according to the contract) does not modify the heap at all, i.e., iff it is "strictly pure."
boolean	hasSelfVar() Checks if a self variable is originally provided.
int	id() Returns the id number of the contract.
boolean	isReadOnlyContract()
java.lang.String	proofToString(Services services) Returns a parseable String representation of the contract.
InformationFlowContract	setID(int newId) Return a new contract which equals this contract except that the id is set to the new id.
InformationFlowContract	setModality(Modality modality)
InformationFlowContract	setModifies(Term modifies)
InformationFlowContract	setName(java.lang.String name)
InformationFlowContract	setTarget(KeYJavaType newKJT, IObserverFunction newPM) Return a new contract which equals this contract except that the the KeYJavaType and ObserverFunction 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

id

private final int id

forClass

private final KeYJavaType forClass

pm

private final IProgramMethod pm

specifiedIn

private final KeYJavaType specifiedIn

baseName

private final java.lang.String baseName

name

private final java.lang.String name

origPre

private final Term origPre

origMby

private final Term origMby

origMod

private final Term origMod

modality

private final Modality modality

origSelf

private final Term origSelf

origParams

private final ImmutableList<Term> origParams

origResult

private final Term origResult

origExc

private final Term origExc

origAtPre

private final Term origAtPre

toBeSaved

private final boolean toBeSaved

origDep

private final Term origDep

origInfFlowSpecs

private final ImmutableList<InfFlowSpec> origInfFlowSpecs

hasRealModifiesClause

final boolean hasRealModifiesClause

If a method is strictly pure, it has no modifies clause which could anonymised.

See Also:

hasModifiesClause()

Constructor Detail

InformationFlowContractImpl

protected InformationFlowContractImpl(java.lang.String baseName,
                                      java.lang.String name,
                                      KeYJavaType forClass,
                                      IProgramMethod pm,
                                      KeYJavaType specifiedIn,
                                      Modality modality,
                                      Term pre,
                                      Term mby,
                                      Term mod,
                                      boolean hasRealMod,
                                      Term self,
                                      ImmutableList<Term> params,
                                      Term result,
                                      Term exc,
                                      Term heapAtPre,
                                      Term dep,
                                      ImmutableList<InfFlowSpec> infFlowSpecs,
                                      boolean toBeSaved,
                                      int id)

InformationFlowContractImpl

public InformationFlowContractImpl(java.lang.String baseName,
                                   KeYJavaType forClass,
                                   IProgramMethod pm,
                                   KeYJavaType specifiedIn,
                                   Modality modality,
                                   Term pre,
                                   Term mby,
                                   Term mod,
                                   boolean hasRealMod,
                                   Term self,
                                   ImmutableList<Term> params,
                                   Term result,
                                   Term exc,
                                   Term heapAtPre,
                                   Term dep,
                                   ImmutableList<InfFlowSpec> infFlowSpecs,
                                   boolean toBeSaved)

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

Description copied from interface: Contract

Returns the contracted function symbol.

Specified by:

getTarget in interface Contract

Specified by:

getTarget in interface InformationFlowContract

hasMby

public boolean hasMby()

Description copied from interface: Contract

Tells whether the contract contains a measured_by clause.

Specified by:

hasMby in interface Contract

getBaseName

public java.lang.String getBaseName()

Specified by:

getBaseName in interface InformationFlowContract

getPre

public Term getPre()

Description copied from interface: InformationFlowContract

Returns the original precondition of the contract.

Specified by:

getPre in interface InformationFlowContract

getMod

public Term getMod()

Description copied from interface: InformationFlowContract

Returns the original modifies clause of the contract.

Specified by:

getMod in interface InformationFlowContract

getMby

public Term getMby()

Description copied from interface: InformationFlowContract

Returns the original measured_by clause of the contract.

Specified by:

getMby in interface Contract

Specified by:

getMby in interface InformationFlowContract

getModality

public Modality getModality()

Description copied from interface: InformationFlowContract

Returns the modality of the contract.

Specified by:

getModality in interface InformationFlowContract

getSelf

public Term getSelf()

Description copied from interface: InformationFlowContract

Get the self-variable which is used in this contract.

Specified by:

getSelf in interface InformationFlowContract

Returns:

originally used self-variable

getParams

public ImmutableList<Term> getParams()

Description copied from interface: InformationFlowContract

Get the parameter-variables which is used in this contract.

Specified by:

getParams in interface InformationFlowContract

Returns:

originally used parameter-variables

getResult

public Term getResult()

Description copied from interface: InformationFlowContract

Get the result-variable which is used in this contract.

Specified by:

getResult in interface InformationFlowContract

Returns:

used result-variable

getExc

public Term getExc()

Description copied from interface: InformationFlowContract

Get the exception-variable which is used in this contract.

Specified by:

getExc in interface InformationFlowContract

Returns:

used exception-variable

getAtPre

public Term getAtPre()

Specified by:

getAtPre in interface InformationFlowContract

isReadOnlyContract

public boolean isReadOnlyContract()

Specified by:

isReadOnlyContract in interface InformationFlowContract

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

hasModifiesClause

public boolean hasModifiesClause()

Description copied from interface: InformationFlowContract

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 InformationFlowContract

Returns:

whether this contract is strictly pure.

hasInfFlowSpec

public boolean hasInfFlowSpec()

Specified by:

hasInfFlowSpec in interface InformationFlowContract

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

getHTMLBody

public java.lang.String getHTMLBody(Services services)

getHTMLSignature

private java.lang.String getHTMLSignature()

getHTMLSignatureBody

private java.lang.StringBuffer getHTMLSignatureBody()

getHTMLFor

protected java.lang.String getHTMLFor(Term originalTerm,
                                      java.lang.String htmlName,
                                      Services services)

getHTMLFor

private java.lang.String getHTMLFor(java.lang.Iterable<Term> originalTerms,
                                    Services services)

getHTMLFor

private java.lang.String getHTMLFor(ImmutableList<InfFlowSpec> originalInfFlowSpecs,
                                    java.lang.String htmlName,
                                    Services services)

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

getDisplayName

public java.lang.String getDisplayName()

Description copied from interface: SpecificationElement

Returns the displayed name.

Specified by:

getDisplayName in interface SpecificationElement

getPODisplayName

public java.lang.String getPODisplayName()

Description copied from interface: InformationFlowContract

For generating contract name of SymbolicExecutionPO

Specified by:

getPODisplayName in interface InformationFlowContract

Returns:

String "Method Contract"

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

getSpecifiedIn

public KeYJavaType getSpecifiedIn()

Specified by:

getSpecifiedIn in interface InformationFlowContract

setID

public InformationFlowContract setID(int newId)

Description copied from interface: InformationFlowContract

Return a new contract which equals this contract except that the id is set to the new id.

Specified by:

setID in interface Contract

Specified by:

setID in interface InformationFlowContract

Parameters:

newId - the new id value

Returns:

an identical contract with the new id

setTarget

public InformationFlowContract setTarget(KeYJavaType newKJT,
                                         IObserverFunction newPM)

Description copied from interface: InformationFlowContract

Return a new contract which equals this contract except that the the KeYJavaType and ObserverFunction are set to the new values.

Specified by:

setTarget in interface Contract

Specified by:

setTarget in interface InformationFlowContract

Parameters:

newKJT - the new KeYJavaType

newPM - the new observer function

Returns:

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

setName

public InformationFlowContract setName(java.lang.String name)

Specified by:

setName in interface InformationFlowContract

setModality

public InformationFlowContract setModality(Modality modality)

Specified by:

setModality in interface InformationFlowContract

setModifies

public InformationFlowContract setModifies(Term modifies)

Specified by:

setModifies in interface InformationFlowContract

getDep

public Term getDep()

Description copied from interface: InformationFlowContract

Returns the dependency set of the contract.

Specified by:

getDep in interface InformationFlowContract

getInfFlowSpecs

public ImmutableList<InfFlowSpec> getInfFlowSpecs()

Description copied from interface: InformationFlowContract

Returns the set of views.

Specified by:

getInfFlowSpecs in interface InformationFlowContract

equals

public boolean equals(Contract c)

Specified by:

equals in interface InformationFlowContract

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

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

getGlobalDefs

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

Specified by:

getGlobalDefs in interface Contract

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.

getPre

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

Deprecated.

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

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

Deprecated.

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

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

Deprecated.

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

@Deprecated
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)

Deprecated.

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

getMby

@Deprecated
public Term getMby(ProgramVariable selfVar,
                               ImmutableList<ProgramVariable> paramVars,
                               Services services)

Deprecated.

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

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

Deprecated.

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

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

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

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

getGlobalDefs

public Term getGlobalDefs()

Specified by:

getGlobalDefs in interface Contract