The POGenerator (pog)

The POGenerator (pog) is invoked from the Main Environment, and is applicable to all non-library, non-generated specifications refinements and implementations which are not currently generated; the Analyser is invoked first, where necessary.

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:

cst
the constraints of the construct (the predicates of the CONSTRAINTS clause)
ctx
the context of the construct (the predicates of the PROPERTIES clause of the construct together with those of subordinate constructs)
inv
the invariant of the construct (the predicates of the INVARIANT clause, together with abstract/concrete equalities of any algorithmically-refined variables)
asn
the assertions of the construct (the predicates of the ASSERTIONS clause)
pre
the precondition of the operation (the predicates of the operation's PRE clause)

The generated proof obligations are stored in the environment directory POB, but some very simple obligations are discharged by the tool and do not appear in the proof obligation file.

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.

A full on-line help listing is available in the Contents Page Also available in the form of a complete Index. Blogo