|
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. Tools
allow for a transfer from this language to the language accepted by Atelier
B. The European Rodin project currently
in progress intends to consolidate this language and create open tools that can
accept it.
|
| |
|
Procedure B
|
|
This
incorrect term (as B has no procedure) 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.
|
| |
|
Classic B
|
|
Like Procedure
B, Classic B refers to the B that existed prior to Procedure 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.
|
