Download Interactive Prover

40
Interactive Prover - User Manual
2. intuitive justification: determine for which reasons this goal must be true within
the component context (refer to section 5.4.2);
3. selecting hypotheses: in the proof obligation isolate the hypotheses corresponding
to these reasons (refer to section 5.4.3);
4. intuitive demonstration: perform an intuitive demonstration of the proof obligation reduced to these hypotheses (refer to section 5.4.4).
5. notes and tests: the intuitive demonstration can give ideas for the formal demonstration, on the causes of the automatic demonstration failure, etc. In this last step,
we want to gain from these ideas. A quick formal demonstration will be looked
for and generalized to other obligations - thus enabling to reduce the number of
obligations to be examined (refer to section 5.4.5).
This list describes the recommended method for the tuning-up phase. We advise the user
to follow these steps for each proof obligation by checking the appropriate sections.
The key idea in this five step method consists in interpreting the proof obligation within
the context of the component to be proved. We then benefit from the full intellectual
process already performed to understand or build the component, a process that will in
time become a set of rigorous demonstrations.
This method requires to read the component to be proven as well as its associated components. We therefore advise you to save in iconized window the appropriate component file and its associated components. For an abstract machine, these are seen
or included; for an implementation, the superior refinement and the imported machines 1 .
Since the Automatic Prover was able to unload proof obligations associated with full parts
of the component, it is sufficient to read a limited part of the component: the
user will get his/her bearings thanks to the operation name (stated in the prover windows
label bar) and to the goal.
In the following sections, we will rapidly review a few of the interactive prover commands
without making a general presentation of this tool, as for the tuning-up phase it is not
necessarily required to know all interactive commands fully. These are studied in detail
in chapter 6 which deals with the formal proof.
The five step analysis of a proof obligation might appear lengthy when dealt with in detail
- as done here. In fact, with force of habit, each obligation is quickly performed, in a
couple of minutes, without necessarily formally separating each step. These steps are only
used to tackle problems in the right order. If a proof obligation seems to be false then you
most probably have met an error in the source: follow the advice given in section 5.8 to
find and correct the error.
1
Notice that even when the interactive prover is started, it is still possible to open the components from
Atelier B: simply open the main (iconized) window and double-click on the component.