THE LOGIC OF B
P.H.B Gardiner and T.N. Vickers
Abstract
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.
Institution
OUCL
Month
January
Number
PRG92
Pages
64
Year
1991