public class FunctionalBlockContract extends FunctionalAuxiliaryContract<BlockContract>
FunctionalBlockContractPO
.
If a block is encountered during a proof, BlockContract
is used instead.Contract.OriginalVariables
INVALID_ID
Constructor and Description |
---|
FunctionalBlockContract(BlockContract contract) |
FunctionalBlockContract(BlockContract contract,
int id) |
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.
|
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
FunctionalBlockContract(BlockContract contract)
contract
- a block contract.FunctionalBlockContract(BlockContract contract, int id)
contract
- a block contract.id
- an ID.public ContractPO createProofObl(InitConfig initConfig)
Contract
initConfig
- the initial configurationpublic ProofOblInput createProofObl(InitConfig initConfig, Contract contract)
Contract
createProofObl
in interface Contract
createProofObl
in class FunctionalAuxiliaryContract<BlockContract>
initConfig
- the initial configurationcontract
- the contractpublic ProofOblInput createProofObl(InitConfig initConfig, Contract contract, boolean supportSymbolicExecutionAPI)
Contract
createProofObl
in interface Contract
createProofObl
in class FunctionalAuxiliaryContract<BlockContract>
initConfig
- the initial configurationcontract
- the contractsupportSymbolicExecutionAPI
- boolean saying whether symbolic execution api is supportedpublic Contract setID(int newId)
Contract
newId
- the new id valuepublic Contract setTarget(KeYJavaType newKJT, IObserverFunction newPM)
Contract
newKJT
- the new KeYJavaTypenewPM
- the new observer function