This page lists various terms related to the “B Method” and the different B programming languages. The B Method is evolving and therefore certain common terms have lost their original meaning. It is important to add to some of the definitions that Wikipedia already provides.
B
In the world of formal methods, B refers to “B” language, the “B” method and the related reference publication: the B Book. Its predecessor is Z, a specification language based on mathematical notations. In addition, B covers refinement and proof, two techniques that are a full part of B.
B LANGUAGE
Is a language that refers to the set theory and predicate logic, and also includes syntax to describe “substitutions”, operations and links betweens machines, refinements and implementations. A description of the language, the refinement and the proof associated with the language is available in the B Book.
B METHOD
This term is often misunderstood because of the use of the word “method”. “B Method” usually refers to the set that includes: the B language, refinement, proof and related tools. Also, unlike common computer languages, a construction approach is associated with B, which, based on specifications, allows for their refinement up to a level that is similar to a code. This approach includes the proof of the coherence of the set. However, this approach is not a method as no standard user guide exists for the application of B.
B Method is therefore: “a proven construction approach (referred to as correct) based on B Language, refinement and proof.”
ATELIER B
Tool supporting the B Method, which includes the ability to translate the refinements into a computer code. It accepts B language as described in the B Book. See Atelier B website.
B PROCESS
This improper term (because B does not include procedures) evokes the B language defined in the B Book. Indeed, levels of refinement can be translated into computer procedures. This term was used with the appearance of Event-B, to avoid confusion with it.
B SYSTEM
This term refers to the use of the B Method to specify a system, in other words, to specify something other than software (software can obviously be a part of the system).
B SOFTWARE
Refers to the B Language described in the B Book used to create software. For a given specification, when all the refinements and proof have been effected, a translation into the computer language of choice may be performed. B Software and B System are distinct: B Software creates B software, B System creates a system.
EVENT-B
Event-B Language is often used as a term to refer to the language utilised to describe a system with the help of events. Refinement and proof are associated with this language. This is one use of the B Method. This language was recently defined by Jean-Raymond Abrial, the inventor of the B Method. Event-B is supported by Atelier B and the European Rodin project, two projects currently in progress will intend to consolidate this language and create open tools that can accept it.
CLASSICAL B
The “classical B” term is used to designate the B language described in the B Book and the reference manual for Language B.
B# (BSHARP)
Obsolete term that refers to the B Rodin language, rarely used today.
B RODIN
This is the Event-B defined within the context of the Rodin project