Languages

Introduction

This section is related to the languages that are manipulated by Atelier B, namely:

  • the B language
  • the Event-B language
  • the THEORY language
  • the refinement rule language

The B language

The B language was invented by J.R Abrial. « The B-Book: assigning programs to meanings » (Cambridge University Press – ISBN 0-521-49619-5) contains the mathematical basis on which it is founded as well as the precise definitions of the notations used. However, over the years, the B language has been adapted to industrial needs (through Atelier B) and the current « operational » definition of this language is rather different from the one exposed in the B-Book. Among the various modifications, we can mention:

  • addition of LOCAL_OPERATIONS: operations call be specified, implemented and used in a single implementation (saving a new decomposition)
  • addition of records
  • removal of trees: trees, as defined in the B-Book, can’t be easily manipulated, leading to very difficult mathematical demonstrations

So we may consider that the current reference document describing the B language is

Another document, explaining how to use the B language for software development, is also available:

The Event-B language

Some history

The event-B language was born in the late 90’s, initially described in Guidelines to formal system studies.

The first reference manual was written during the european project MATISSE, as well as a tool, evt2b, translating event-B models into (« software ») B models supported by Atelier B 3.x.

Modalities were also added to the language, following « Introducing dynamic constraints in B ».

Event-B was then experimented during the project PUSSEE, leading to the development of an event-b to VHDL translator.
The project RODIN was initiated to develop a platform supporting event-B. The language was simplified (many B constructs and operators were removed, new ones added), leading to Event-B language description manual.

The project DEPLOY aims at enriching the platform and the language through industrial deployments (hence the name of the project). A second version of the language was released in 2009.

Atelier B 4.0 is the first Atelier B natively supporting event-B, even if the language slightly differs from the one supported by the Rodin platform.

The Event-B language supported by Atelier B 4.x

Summary

The event-B mathematical language is exactly the same as the B mathematical language, described in the B Language Reference Manual. The differences are in:

  • the kind of components supported: SYSTEM (for top-level component, ako specification) and REFINEMENT (IMPLEMENTATION is not supported)
  • the visibility clauses: only SEES and INCLUDES are supported.
  • the substitutions: events should match with one of these three substitutions:
    • BEGIN <subst> END
    • ANY <vars> WHERE <pred> THEN <subst> END
    • SELECT <pred> THEN <subst> END

However substitutions <subst> may any substitution allowed in the B Language Reference Manual. For example, an IF THEN ELSE substitution, a sequencing substitution, etc.

New kewords have been introduced:

  • ref: for indicating what event(s) an event is refining
  • WITNESS: when refinening an ANY substitution. It allows for simplifying the demonstration of existence of values for the local variables introduced in the ANYsubstitution.

Further extensions are being considered. For example, introduction of MODALITIES, as it was the case in the MATISSE version of event-B language. A draft specification has been produced and is available here.

Moreover, a RODIN to Atelier B importer is being developed, enabling the port of Rodin event-b projects to Atelier B projects.

Event-B language description

The language is described in Atelier B Event B Language.

There is also a very good Tutorial on the Event-B method, by Dominique Cansell and Dominique Méry.

The THEORY language

Presentation

This language was created to simplify the development of tools manipulating B models. It is close to PROLOG. Several Atelier B tools are implemented in THEORY language:

  • typechecker,
  • proof obligation generator,
  • prover,
  • predicate prover,
  • arithmetic prover,
  • well-definedness verifier (also called Delta tool).

A subset of the THEORY language allows to write mathematical rules that can be added to an Atelier B project, in order to improve Atelier B prover.

Tool

The THEORY language interpreter is part of the Atelier B distribution. The executable file is krt or krt.exe.

Reference documentation

  • Operations and guards
  • Semantics
  • Syntax
  • Writing Mathematical Rules

 

The Mathematical Rule Language

This language is a subset of the THEORY language, and is used to improve Atelier B automatic prover, by adding mathematical rules.

A document is describing this language:

  • Writing Mathematical Rules 1.1 (pdf-French)
  • Writing Mathematical Rules 1.1 (Wiki manual – English – Ongoing translation)
  • Image:Writing mathematical rules.pdf (PDF English)