Package | Description |
---|---|
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.mgt |
This package contains classes for proof environments and proof management.
|
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
Modifier and Type | Class and Description |
---|---|
class |
InfFlowContractPO |
class |
SymbolicExecutionPO |
Modifier and Type | Class and Description |
---|---|
class |
DependencyContractPO
The proof obligation for dependency contracts.
|
class |
FunctionalBlockContractPO
A proof obligation for a
FunctionalBlockContract . |
class |
FunctionalLoopContractPO
A proof obligation for a
FunctionalLoopContract . |
class |
FunctionalOperationContractPO
The proof obligation for operation contracts.
|
class |
WellDefinednessPO
The proof obligation for well-definedness checks.
|
Modifier and Type | Method and Description |
---|---|
ContractPO |
SpecificationRepository.getContractPOForProof(Proof proof)
Returns the PO that the passed proof is about, or null.
|
ContractPO |
SpecificationRepository.getPO(Contract c)
Returns the PO that the passed contract is about, or null.
|
ContractPO |
SpecificationRepository.getPOForProof(Proof proof) |
Modifier and Type | Method and Description |
---|---|
ContractPO |
FunctionalOperationContractImpl.createProofObl(InitConfig initConfig) |
ContractPO |
InformationFlowContractImpl.createProofObl(InitConfig initConfig) |
ContractPO |
FunctionalBlockContract.createProofObl(InitConfig initConfig) |
ContractPO |
DependencyContractImpl.createProofObl(InitConfig initConfig) |
ContractPO |
WellDefinednessCheck.createProofObl(InitConfig initConfig) |
ContractPO |
Contract.createProofObl(InitConfig initConfig)
Returns a proof obligation to the passed initConfig.
|
ContractPO |
FunctionalLoopContract.createProofObl(InitConfig initConfig) |
Copyright © 2003-2019 The KeY-Project.