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.
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.
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.
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.”
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.
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.
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).
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 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.
The “classical B” term is used to designate the B language described in the B Book and the reference manual for Language B.
Obsolete term that refers to the B Rodin language, rarely used today.
This is the Event-B defined within the context of the Rodin project