## 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

- B Language Reference Manual 1.8.6 (pdf – English)
- Manuel de Référence du Langage B 1.8.6 (pdf – French)

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

- B Language User Manual 1.2 (pdf – French)
- B Language User Manual 1.2 (English – Ongoing translation)

## 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*ANY*substitution.

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)