The tool automatically generates all the proof obligations which are required to be discharged in order to guarantee the internal consistency of a specification or the correctness of a refinement with respect to its abstraction. The POGenerator provides the same options as the Analyser when a construct being currently edited differs from that of the committed version.
The proof obligations are generated according to the correctness criteria which are required to hold within the B-Method. Thus, for example, the criteria require that an Abstract Machine initialisation must establish the invariant, and that each operation re-establish the invariant. Obligations are also generated to maintain the correct relationships between a machine and its refinements. (Full details of the proof obligations are given in the B-Technology Technical Overview.)
The following three-letter acronyms appear in B-Toolkit proof obligations:
If an error is detected during generation of the proof obligations then the Mini-remake option is offered.
The current number of outstanding proof obligations and total number
of proof obligations (where applicable) is displayed for each construct
in the Constructs Area in the
Provers Environment window
under `pob' and `tot' respectively.