de.uka.ilkd.key.speclang

Class FunctionalBlockContract

java.lang.Object

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

de.uka.ilkd.key.speclang.FunctionalBlockContract

All Implemented Interfaces:

Contract, SpecificationElement

public class FunctionalBlockContract
extends FunctionalAuxiliaryContract<BlockContract>

This class is only used to generate a proof obligation for a block (see FunctionalBlockContractPO. If a block is encountered during a proof, BlockContract is used instead.

Author:

lanzinger

Nested Class Summary

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

Contract.OriginalVariables

Field Summary

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

INVALID_ID

Constructor Summary

Constructors

Constructor and Description
FunctionalBlockContract(BlockContract contract)
FunctionalBlockContract(BlockContract contract, 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 supportSymbolicExecutionAPI) Returns a proof obligation to the passed contract and initConfig.
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.

Methods inherited from class de.uka.ilkd.key.speclang.FunctionalAuxiliaryContract

getAccessible, getAssignable, getAuxiliaryContract, getBlock, getDep, getDep, getDisplayName, getGlobalDefs, getGlobalDefs, getHTMLText, getKJT, getMby, getMby, getMby, getMethod, getModality, getName, getOrigVars, getPlaceholderVariables, getPlainText, getPre, getPre, getPre, getPre, getProofObl, getRequires, getTarget, getTypeName, getVisibility, hasMby, hasModifiesClause, hasSelfVar, id, isAuxiliary, proofToString, setAuxiliaryContract, toBeSaved, transactionApplicableContract

Methods inherited from class java.lang.Object

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

Constructor Detail

FunctionalBlockContract

FunctionalBlockContract(BlockContract contract)

Parameters:

contract - a block contract.

FunctionalBlockContract

FunctionalBlockContract(BlockContract contract,
                        int id)

Parameters:

contract - a block contract.

id - an ID.

Method Detail

createProofObl

public ContractPO createProofObl(InitConfig initConfig)

Description copied from interface: Contract

Returns a proof obligation to the passed initConfig.

Parameters:

initConfig - the initial configuration

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

Overrides:

createProofObl in class FunctionalAuxiliaryContract<BlockContract>

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

Overrides:

createProofObl in class FunctionalAuxiliaryContract<BlockContract>

Parameters:

initConfig - the initial configuration

contract - the contract

supportSymbolicExecutionAPI - boolean saying whether symbolic execution api is supported

Returns:

the proof obligation

setID

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

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.

Parameters:

newKJT - the new KeYJavaType

newPM - the new observer function

Returns:

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