B LANGUAGES


B AND ITS DIFFERENT LANGUAGES


pictos-bullecode-105x105

This page lists various terms related to the “B Method” and the different B programming languages. 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.

pictos-code-105x105

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.

SEE LINK
pictos-code-105x105

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.”

pictos-code-105x105

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.

SEE LINK
pictos-code-105x105

B PROCESS

Ce terme impropre (Car le B ne comprend pas de procédure) évoque le langage B défini dans le B Book. En effet, des niveaux de raffinements peuvent être traduits en des procédures informatiques. Ce terme a été utilisé avec l’apparition du B événementiel, pour éviter la confusion avec celui-ci.

pictos-code-105x105

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).

pictos-code-105x105

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.

pictos-code-105x105

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.

pictos-code-105x105

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.

pictos-code-105x105

B# (BSHARP)

Obsolete term that refers to the B Rodin language, rarely used today.

pictos-code-105x105

B RODIN

This is the Event-B defined within the context of the Rodin project

SEE LINK