Programming Research Group Technical Monograph PRG-92

P H B Gardiner and T N Vickers

January 1991, 62 pages, ISBN 0-902928-70-8

The two papers collected in this monograph describe the logic that forms the theoretical foundation of the proof assistant known as the B-tool. The B-tool was designed as a computerized support for the formal development of imperative programs from Z-like specifications. Its prime functions are to provide a simply-accessed database for recording program developments, and to provide a secure environment for interactively constructing the proofs necessary for those developments.