public class FunctionalLoopContract extends FunctionalAuxiliaryContract<LoopContract>
FunctionalLoopContractPO
.
If a block is encountered during a proof, LoopContract
is used instead.Contract.OriginalVariables
INVALID_ID
Constructor and Description |
---|
FunctionalLoopContract(LoopContract contract) |
FunctionalLoopContract(LoopContract 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.
|
void |
replaceEnhancedForVariables(Services services)
Replaces
\index and \values with the proper variables in all terms of this
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.
|
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
FunctionalLoopContract(LoopContract contract)
contract
- a loop contract.FunctionalLoopContract(LoopContract contract, int id)
contract
- a loop 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<LoopContract>
initConfig
- the initial configurationcontract
- the contractpublic ProofOblInput createProofObl(InitConfig initConfig, Contract contract, boolean supportSymbolicExecutionAPI)
Contract
createProofObl
in interface Contract
createProofObl
in class FunctionalAuxiliaryContract<LoopContract>
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 functionpublic void replaceEnhancedForVariables(Services services)
\index
and \values
with the proper variables in all terms of this
contract.services
- services.LoopContract.replaceEnhancedForVariables(de.uka.ilkd.key.java.StatementBlock, Services)