The B-Method has been developed by Jean-Raymond Abrial - also originator of the Z notation - and others. B is a formal method for the development of program code from a specification in the Abstract Machine Notation. It includes tool support and has been used in some significant industrial applications (e.g., by GEC Alsthom).
Email email@example.com with the message "subscribe bug" to join the BUG mailing list. Contact Georges Mariano on firstname.lastname@example.org for further BUG information.
Information also available in French. See La Lettre B newsletter.
Email Ib.Sorensen@comlab.ox.ac.uk for further information.
A mailing list for discussion about B has been established. Send an email message containing "subscribe b-talk" to email@example.com to join.
A list of references relevant to B is available on-line from the Z bibliography.
Both bibliographies are in BibTeX format suitable for use with the LaTeX document preparation system.
Contents: Mathematical reasoning; Set notation; Mathematical objects; Introduction to abstract machines; Formal definition of abstract machines; Theory of abstract machines; Construction large abstract machines; Example of abstract machines; Sequencing and loop; Programming examples; Refinement; Construction large software systems; Example of refinement;
Appendices: Summary of the most current notations; Syntax; Definitions; Visibility rules; Rules and axioms; Proof obligations.
Atelier B, a tool supporting the Abstract Machine Notation (AMN), is available under licence. from Digilog, France. Features include syntax, type and static semantics checking, proof support, refinement, a graphical interface and pretty-printing. An animator is planned. Test case generation is not supported. Contact Francois Bustany on firstname.lastname@example.org (tel: +33 42 39 93 19, fax: +33 42 24 38 06).
Further information: Atelier B is composed of a complete set of integrated tools enabling the development of applications using the method invented by Jean-Raymond Abrial, the B-Method. Atelier B assists developers in the formalization of their aplications, performing automatically on specifications and their refinements, syntax analysis, type checking, generation and demonstration of proof obligations. Extra components are supplied such as translators into current computer programming languages (C, Ada, ...), a mathematical editor, libraries of predefined machines and various project analysis tools. Access to Atelier B software tools is by a graphical MOTIF interface or by a batch language; in each mode it manages multi-users projects. Atelier B has been designed by Digilog and GEC Alsthom Transport in close collaboration with Jean-Raymond Abrial. The first version of Atelier B will be upgraded in 1995 with an animator of specifications, a new generation of prover, a powerful project documentation generator and various interfaces with standard tools (SGML, Interleaf, ...). Atelier B is sponsored by RATP, SNCF and INRETS and developed with their technical co-operation.
Part of the OUCL archive.