The Proof Printer (ppf)

The ProofPrinter (ppf) is invoked from the Provers Environment, and is applicable to all machines, refinements and implementations which are pogenerated/ autoproved or btoolproved. Invoking the tool results in a selection showing those levels for the construct which have not been printed.

A `prf' construct containing either statements of proof obligations (in the case of Level 0 constructs produced by the POGenarator), or proof listings (for Levels greater than 0 produced by the AutoProver/ BToolProver) results.

Proof constructs are displayed in both the Provers and Documents Environments.

In the case of proofs, Laws (either those provided by the B-Toolkit Library, or those provided by the user through a PROOFMETHOD) used in proofs contained in that `.prf' construct are presented at the end of the construct; note that the scope of the numbering of such Laws is the file in which they appear.

Each proof conforms to a B-formula and so may be machine-processed by other proof checkers, if required, to check the validity of the proof.

Each proof construct may be marked up and included in a DOCUMENT if required; this is accomplished in the Documents Environment.

Although the formatting is completely automatic, it is sometimes necessary to insert linebreaks or pagebreaks.

A linebreak - the LaTeX `\\' - may be inserted immediately following (ie. no whitespace) an infix symbol. For example, following an ampersand `&\\' or implication `=>\\' (to break predicates) or a comma `,\\' (to break proof step justification lists).

A pagebreak - the LaTeX `\newpage' - may be inserted immediately following the comma `,\newpage' separating the proof steps, or immediately following the semicolon `;\newpage' which separates the proofs/Laws.

No other editing of proof constructs is permitted!

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