Rodin POs and ProB: Difference between revisions
Created page with " What is the relationship between Rodin proof obligations (POs) and ProB. == ProB Prover Disprover == ProB can be applied to individual POs by clicking the ProB button in th..." |
No edit summary |
||
| Line 8: | Line 8: | ||
[[File:disprover_proof_control.png]] | [[File:disprover_proof_control.png]] | ||
See [Tutorial_Disprover the tutorial on the ProB Prover/Disprover] for more details. | See [[Tutorial_Disprover| the tutorial on the ProB Prover/Disprover]] for more details. | ||
One can also export the POs of a particular Event-B machine for use with the command-line version of ProB. | One can also export the POs of a particular Event-B machine for use with the command-line version of ProB. | ||
This will generate a Prolog file (with .pl ending) which can be read by probcli. It will then check the individual proof obligations. | This will generate a Prolog file (with .pl ending) which can be read by probcli. It will then check the individual proof obligations. | ||
Revision as of 10:21, 5 March 2020
What is the relationship between Rodin proof obligations (POs) and ProB.
ProB Prover Disprover
ProB can be applied to individual POs by clicking the ProB button in the Proof Control view of Rodin.
See the tutorial on the ProB Prover/Disprover for more details.
One can also export the POs of a particular Event-B machine for use with the command-line version of ProB.
This will generate a Prolog file (with .pl ending) which can be read by probcli. It will then check the individual proof obligations.