Event-B Mathematical Language

From Event-B
Revision as of 11:53, 30 August 2010 by imported>Wohuai
Jump to navigationJump to search

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 and / or neglect important aspects of the logic (e.g. types and well-definedness).

Specification Documents

A comprehensive specification of the logic (abstract syntax, semantics, proof calculus, core theories) is currently being written. Partners of the DEPLOY project can access the current draft.

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.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Event-B_Mathematical_Language&oldid=4171’