de.uka.ilkd.key.speclang

Interface Contract

All Superinterfaces:

SpecificationElement

All Known Subinterfaces:

DependencyContract, FunctionalOperationContract, InformationFlowContract, OperationContract

All Known Implementing Classes:

BlockWellDefinedness, ClassWellDefinedness, DependencyContractImpl, FunctionalAuxiliaryContract, FunctionalBlockContract, FunctionalLoopContract, FunctionalOperationContractImpl, InformationFlowContractImpl, LoopWellDefinedness, MethodWellDefinedness, StatementWellDefinedness, WellDefinednessCheck

public interface Contract
extends SpecificationElement

A contractual agreement about an ObserverFunction.

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static class	Contract.OriginalVariables Class for storing the original variables without always distinguishing several different cases depending on which variables are present/needed in order to provide a general interface.

Field Summary

Fields

Modifier and Type	Field and Description
static int	INVALID_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 supportSymbolicExecutionAPI) 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.
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.
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.
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.
java.lang.String	getTypeName() Returns technical name for the contract type.
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.
default boolean	isAuxiliary()
java.lang.String	proofToString(Services services) Returns a parseable String representation of the contract.
Contract	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.
boolean	transactionApplicableContract()

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

getDisplayName, getKJT, getName, getVisibility

Field Detail

INVALID_ID

static final int INVALID_ID

See Also:

Constant Field Values

Method Detail

isAuxiliary

default boolean isAuxiliary()

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.

id

int id()

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.

getTarget

IObserverFunction getTarget()

Returns the contracted function symbol.

hasMby

boolean hasMby()

Tells whether the contract contains a measured_by clause.

getOrigVars

Contract.OriginalVariables getOrigVars()

Returns the original ProgramVariables to replace them easier. The second list consists of the parameters.

getPre

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

Returns the precondition of the contract.

Parameters:

heap - heap variable

selfVar - self variable

paramVars - parameter variables

atPreVars - variables at previous heap

services - services object

Returns:

precondition

getPre

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.

Parameters:

heapContext - heap context

selfVar - self variable

paramVars - parameter variables

atPreVars - variables at previous heap

services - services object

Returns:

precondition

getPre

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.

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

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.

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

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.

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

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.

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

Term getRequires(LocationVariable heap)

getAssignable

Term getAssignable(LocationVariable heap)

getAccessible

Term getAccessible(ProgramVariable heap)

getGlobalDefs

Term getGlobalDefs()

getGlobalDefs

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

getMby

Term getMby()

getMby

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

Returns the measured_by clause of the contract.

Parameters:

selfVar - the self variable

paramVars - the parameter variables

services - services object

Returns:

the measured-by 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.

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

getHTMLText

java.lang.String getHTMLText(Services services)

Returns the contract in pretty HTML format.

Parameters:

services - services instance

Returns:

the html representation

getPlainText

java.lang.String getPlainText(Services services)

Returns the contract in pretty plain text format.

Parameters:

services - services instance

Returns:

the plain text representation

toBeSaved

boolean toBeSaved()

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)

Returns:

see above

transactionApplicableContract

boolean transactionApplicableContract()

proofToString

java.lang.String proofToString(Services services)

Returns a parseable String representation of the contract. Precondition: toBeSaved() must be true.

Parameters:

services - the services instance

Returns:

the (parseable) String representation

createProofObl

ContractPO createProofObl(InitConfig initConfig)

Returns a proof obligation to the passed initConfig.

Parameters:

initConfig - the initial configuration

Returns:

the proof obligation

getProofObl

ProofOblInput getProofObl(Services services)

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

Parameters:

services - the services instance

Returns:

the proof obligation according to the specification repository

createProofObl

ProofOblInput createProofObl(InitConfig initConfig,
                             Contract contract)

Returns a proof obligation to the passed contract and initConfig.

Parameters:

initConfig - the initial configuration

contract - the contract

Returns:

the proof obligation

createProofObl

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

Returns a proof obligation to the passed contract and initConfig.

Parameters:

initConfig - the initial configuration

contract - the contract

supportSymbolicExecutionAPI - boolean saying whether symbolic execution api is supported

Returns:

the proof obligation

setID

Contract setID(int newId)

Returns a contract which is identical this contract except that the id is set to the new id.

Parameters:

newId - the new id value

Returns:

an identical contract with the new id

setTarget

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.

Parameters:

newKJT - the new KeYJavaType

newPM - the new observer function

Returns:

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

getTypeName

java.lang.String getTypeName()

Returns technical name for the contract type.

Returns:

the technical name

hasSelfVar

boolean hasSelfVar()

Checks if a self variable is originally provided.

Returns:

true self variable is originally provided, false no self variable available.