The different B languages
This page lists various terms that relate to the so-called “B formal method”. As the B method evolves, some common terms lose their original meaning. We feel the need to complete some definitions already given on Wikipedia.
B
B evokes, in the field of formal methods, the “B” language, the “B” method, the reference book: the B Book. Its ancestor is Z, a specification language based on mathematical notations. B also includes refinement and proof, two techniques that are an integral part of B.
B LANGUAGE
A language referring to set theory and predicate logic, also including a syntax for describing “substitutions”, operations, and links between machines, refinements and implementations. The description of the language and that of the refinement and proof associated with the language are described in the B Book.
B METHODE
This term is generally misunderstood because of the term. The “B method” traditionally refers to the whole of the B language, refinement, proof, and associated tools. Also, unlike the usual computer languages, B is associated with a constructive process that allows the specification to be refined to a code-like level. But this approach is not a method in the sense that there are no standard instructions for applying B.
The B method is therefore: “a proven (so-called correct) construction approach, based on the B language, refinement and proof”.
ATELIER B
A tool that supports the B method and includes the ability to translate refinements into computer code. It accepts the B language as described in the B Book.
B PROCESS
This misnomer (because B does not include procedures) refers to the B language defined in the B Book. Indeed, levels of refinement can be translated into software procedures. This term was used with the appearance of event-driven B, to avoid confusion with it.
SYSTEM B
This term refers to the use of the B method to specify a system, i.e. to specify something other than software (software can of course be part of a system).
SOFTWARE B
Refers to the B language described in the B Book, which is used to make software. For a given specification, when all the refinements have been made and the proof is complete, a translation can be made into the computer language of choice. We oppose B software and B system, B software to make software, B system to make system.
EVENT-B
The language used to describe a system using events is often referred to as the Event-B language. This language is associated with refinement and proof. It is a use of the B method. This language was defined by the inventor of the B method, Jean-Raymond Abrial. Event-B is supported by the Atelier B and the Rodin platform, both of which aim to consolidate this language and provide open tools capable of accepting it.
CLASSICAL B
The term “classical B” is used to refer to the B language described in the B Book and the B Language Reference Manual.
B# (BSHARP)
An obsolete term, referring to the Event-B language, which was mentioned a little but is no longer used.
B RODIN
This is the event-based B language defined for the Rodin project.