de.uka.ilkd.key.speclang

Class FunctionalAuxiliaryContract<T extends AuxiliaryContract>

java.lang.Object

de.uka.ilkd.key.speclang.FunctionalAuxiliaryContract<T>

Type Parameters:

T - the type of AuxiliaryContract for which this class generated POs.

All Implemented Interfaces:

Contract, SpecificationElement

Direct Known Subclasses:

FunctionalBlockContract, FunctionalLoopContract

public abstract class FunctionalAuxiliaryContract<T extends AuxiliaryContract>
extends java.lang.Object
implements Contract

This class is only used to generate a proof obligation for an AuxiliaryContract.

Author:

lanzinger

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 T	contract
private java.lang.String	displayName This contract's display name.
private int	id This contract's ID.
private java.lang.String	name This contract's name.
private java.lang.String	typeName This contract's type name.

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

INVALID_ID

Constructor Summary

Constructors

Constructor and Description
FunctionalAuxiliaryContract(T contract)
FunctionalAuxiliaryContract(T contract, int id)

Method Summary

Modifier and Type	Method and Description
ProofOblInput	createProofObl(InitConfig initConfig, Contract contract) Returns a proof obligation to the passed contract and initConfig.
ProofOblInput	createProofObl(InitConfig initConfig, Contract contract, boolean supportSymbolicExecutionAPI) Returns a proof obligation to the passed contract and initConfig.
private java.lang.String	generateName(java.lang.String baseName, java.util.function.UnaryOperator<java.lang.String> generator)
Term	getAccessible(ProgramVariable heap)
Term	getAssignable(LocationVariable heap)
T	getAuxiliaryContract()
StatementBlock	getBlock()
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.
IProgramMethod	getMethod()
Modality	getModality()
java.lang.String	getName() Returns the unique internal name of the specification element.
Contract.OriginalVariables	getOrigVars() Returns the original ProgramVariables to replace them easier.
AuxiliaryContract.Variables	getPlaceholderVariables() Returns the set of placeholder variables created during this contract's instantiation.
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)
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	hasMby() Tells whether the contract contains a measured_by clause.
boolean	hasModifiesClause(LocationVariable heap) Returns true iff the method (according to the contract) does not modify the heap at all, i.e., iff it is "strictly pure."
boolean	hasSelfVar() Checks if a self variable is originally provided.
int	id() Returns the id number of the contract.
boolean	isAuxiliary()
java.lang.String	proofToString(Services services) Returns a parseable String representation of the contract.
protected void	setAuxiliaryContract(T contract)
boolean	toBeSaved() Tells whether, on saving a proof where this contract is available, the contract should be saved too.
boolean	transactionApplicableContract()

Methods inherited from class java.lang.Object

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

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

createProofObl, setID, setTarget

Field Detail

contract

private T extends AuxiliaryContract contract

See Also:

getAuxiliaryContract()

id

private final int id

This contract's ID.

name

private final java.lang.String name

This contract's name.

displayName

private final java.lang.String displayName

This contract's display name.

typeName

private final java.lang.String typeName

This contract's type name.

Constructor Detail

FunctionalAuxiliaryContract

FunctionalAuxiliaryContract(T contract)

Parameters:

contract - a block contract.

FunctionalAuxiliaryContract

FunctionalAuxiliaryContract(T contract,
                            int id)

Parameters:

contract - a block contract.

id - an ID.

Method Detail

generateName

private java.lang.String generateName(java.lang.String baseName,
                                      java.util.function.UnaryOperator<java.lang.String> generator)

Parameters:

baseName - a base name.

generator - a name generator.

Returns:

the generated name.

isAuxiliary

public boolean isAuxiliary()

Specified by:

isAuxiliary in interface Contract

Returns:

true if any only if this contract does not necessarily need to be proven in its own proof obligation. E.g., this is true for FunctionalBlockContracts and FunctionalLoopContracts.

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

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

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

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

getTarget

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

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

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

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

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

getGlobalDefs

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

Specified by:

getGlobalDefs in interface Contract

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

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

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

transactionApplicableContract

public boolean transactionApplicableContract()

Specified by:

transactionApplicableContract in interface Contract

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

getProofObl

public ProofOblInput getProofObl(Services services)

Description copied from interface: Contract

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

Specified by:

getProofObl in interface Contract

Parameters:

services - the services instance

Returns:

the proof obligation according to the specification repository

createProofObl

public ProofOblInput createProofObl(InitConfig initConfig,
                                    Contract contract)

Description copied from interface: Contract

Returns a proof obligation to the passed contract and initConfig.

Specified by:

createProofObl in interface Contract

Parameters:

initConfig - the initial configuration

contract - the contract

Returns:

the proof obligation

createProofObl

public ProofOblInput createProofObl(InitConfig initConfig,
                                    Contract contract,
                                    boolean supportSymbolicExecutionAPI)

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

supportSymbolicExecutionAPI - boolean saying whether symbolic execution api is supported

Returns:

the proof obligation

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.

hasModifiesClause

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

true iff this contract is strictly pure.

See Also:

AuxiliaryContract.hasModifiesClause(LocationVariable)

setAuxiliaryContract

protected void setAuxiliaryContract(T contract)

getAuxiliaryContract

public T getAuxiliaryContract()

Returns:

the corresponding AuxiliaryContract.

getBlock

public StatementBlock getBlock()

Returns:

the block this contract belongs to.

See Also:

AuxiliaryContract.getBlock()

getMethod

public IProgramMethod getMethod()

Returns:

the method containing getBlock()

See Also:

AuxiliaryContract.getMethod()

getPlaceholderVariables

public 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, AuxiliaryContract.getPlaceholderVariables()

getModality

public Modality getModality()

Returns:

this contract's modality.

See Also:

AuxiliaryContract.getModality()