Home |
B News |
B Method |
R&D Activities |
Formal Proof |
Publications |
Conferences |
B, the different languages |
Open Source Projects |
B Tools |
Documents |
Links |
Contact
B, The Different Languages...
This page lists various terms related to the "B Method". 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 - B Language - B Method - Atelier B - B System - Event-B - Procedure B - B Software - Classical B - B Rodin - B# (Bsharp)
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. Also see http://www.atelierb.eu/ressources/manref1.8.6.fr.zip
B Method
This term is often misunderstood because of the use of the word "method". "B Method" usually refers to the set that includes: 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.
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).
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.
B Process
This incorrect term (as B has no process) refers to the B language described in the B Book. In fact, levels of refinement can be translated into computer procedures. This term was used when Event-B appeared in order to avoid confusion.
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.
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 Rodin
This is the Event-B defined within the context of the Rodin project.
B# (Bsharp)
Obsolete term that refers to the B Rodin language, rarely used today.