Tutorial Disprover: Difference between revisions

Line 5: Line 5:
We believe the Disprover to be useful. The disprover plugin is currently still experimental when used as a prover.
We believe the Disprover to be useful. The disprover plugin is currently still experimental when used as a prover.
Please keep in mind, that you might run into some rough edges or even get wrong results (please inform us about any issues).
Please keep in mind, that you might run into some rough edges or even get wrong results (please inform us about any issues).
See [http://stups.hhu.de/w/Special:Publication/disprover_eval for a paper describing the disprover as a prover].
See [http://stups.hhu.de/w/Special:Publication/disprover_eval the paper describing the disprover as a prover] for more details.


== Introduction ==
== Introduction ==

Revision as of 13:06, 6 September 2015


WARNING

We believe the Disprover to be useful. The disprover plugin is currently still experimental when used as a prover. Please keep in mind, that you might run into some rough edges or even get wrong results (please inform us about any issues). See the paper describing the disprover as a prover for more details.

Introduction

The ProB Disprover plugin for RODIN utilizes the ProB animator and model checker to automatically find counterexamples or proofs for a given proof obligation.

The Disprover is described in Debugging Event-B Models using the ProB Disprover Plug-in, Ligot, Bendisposto, Leuschel.

Recently, the Disprover has been extended to detect cases in which the search for a counter-example was complete, yet there was no result. In this cases, the absence of a counter-example will be reported as a proof.

Installation

The ProB Disprover is currently only available through the ProB Nightly Build Update Site (http://nightly.cobra.cs.uni-duesseldorf.de/rodin/updatesite/).


How to use it

Disprover-all.png: The proof obligation editor in Rodin presents the user with a number of Hypotheses and one Goal, to be proved. If the Disprover is installed, it is available in the tool bar alongside the other provers:

Disprover proof control.png

How it works

Upon selecting the Disprover, it builds a formula from the Hypotheses and the negated Goal. The ProB model checker then tries to find a model for that formula. If that is possible, this model is a counter example that will be presented back to the user in the proof tree. The disprover also checks if there cannot be a model for the formula. If this is the case it acts like a decision procedure, i.e., absence of a model is a proof for the goal. This is shown in the proof tree as follows:

Disprover proof.png

Unfortunately, sometimes neither a counter example nor a proof can be found.