Download Interactive Prover

TUNING-UP PHASE
47
• the Prover higher forces could be launched on non-discarded proof obligations without loosing time on the admitted ones.
But, application of the admission rule is saved as a manual demonstration for the concerned
proof obligations - which can be a problem when the component is modified. Indeed, the
proof obligations can then have been modified and application of the admission rule can
lead to think they are true. Using an admission rule requires a fair knowledge of the
Interactive Prover. Here, we shall only see when this method applies during a tuning-up
phase. To learn how to use admission rules, read section 6.
5.5
Simplifying B component expressions
Some components create too many proof obligations or too complex ones. It even happens
that the number of proof obligations to be generated for a component is so large that the
generator saturates and fails. In all these cases it is on the components themselves that
we must act to select the forms of the expressions facilitating the proof.
On the other hand, simplifying the expressions of formal specifications often enables to
understand the problem better, as the contemplated software is then better modeled, in a
form that facilitates reasoning as it facilitates the proof. The spirit of B method is to build
the software in order to prove it satisfies the considered need (read the B-Book foreword).
It must be clear that not every true project is necessarily demonstrable. Proof is
a high level check that can only be performed when various separation requirements are
respected (Divide and Conquer). A standard example of this, is the analysis of proof
obligations concerning operations in sequence after an if: these POs are split n times, n
being the number of if pathes.
Transforming the component to return to expressions that facilitate the proof is a complex
methodological subject that we will study very briefly here. We will merely give a number
of “recipes”.
5.5.1
Separating components
Proof obligations too numerous or too complex often denote a bad separation of the
components. Instruction sequences will then be too lengthy (see above), nested loops, etc.
A new separation is the first method to try to reduce proof difficulty. Think specially
about :
• Create imported machines to separate the implementation complex parts in major
operations.
• Insert refinements when a proof implementation is too complex.