# Difference between revisions of "Event-B Mathematical Language"

imported>Nomeata |
imported>Ladenberger |
||

Line 1: | Line 1: | ||

+ | {| class="wikitable" style="font-style:italic; text-align: center; font-size:120%; border: 3px dashed red;" | ||

+ | |- | ||

+ | ! scope="col" | Do not edit! This content has been migrated to Subversion. | ||

+ | |- | ||

+ | |([http://handbook.event-b.org Nightly Handbook Build]) | ||

+ | |} | ||

+ | |||

This page gives a brief summary of documents describing Event-B's logic aka mathematical language. | This page gives a brief summary of documents describing Event-B's logic aka mathematical language. | ||

## Revision as of 15:18, 16 September 2011

Do not edit! This content has been migrated to Subversion. |
---|

(Nightly Handbook Build) |

This page gives a brief summary of documents describing Event-B's logic aka mathematical language.

# Introductory Texts

The logic is introduced in these slides and Jean-Raymond Abrial's book "Modeling in Event-B". Note that those introductory texts are partially outdated w.r.t. the version implemented by Rodin (see How Rodin Deviates from Abrial's Book).

# Specification Documents

A comprehensive specification of the logic (abstract syntax, semantics, proof calculus, core theories) is available as technical report.

Event-B's concrete syntax (V2, supported since Rodin 1.0.0) is specified in kernel_lang.pdf. An older version (available in mathLanguage-2007-10-26.pdf) describes the concrete syntax used by the Rodin platform up to releases 0.9.x. The changes between these two versions are summarized in Changes_to_the_Mathematical_Language_of_Event-B.

There is also A Concise Summary of the Event B mathematical tool.