Difference between revisions of "Event-B Mathematical Language"
imported>Ladenberger |
imported>Ladenberger |
||
Line 1: | Line 1: | ||
− | + | This page gives a brief summary of documents describing Event-B's logic aka mathematical language. | |
− | |||
− | |||
− | |||
− | |||
− | |||
− | + | =Rodin Handbook= | |
+ | |||
+ | [http://handbook.event-b.org/current/html/mathematical_notation.html Mathematical Notation Reference Section in Rodin Handbook] | ||
− | = | + | =Specification Documents= |
The logic is introduced in [http://deploy-eprints.ecs.soton.ac.uk/53/2/sld_mth1.pdf these slides] and Jean-Raymond Abrial's book "Modeling in Event-B". | The logic is introduced in [http://deploy-eprints.ecs.soton.ac.uk/53/2/sld_mth1.pdf 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]]). | Note that those introductory texts are partially outdated w.r.t. the version implemented by Rodin (see [[How Rodin Deviates from Abrial's Book]]). | ||
− | |||
− | |||
A comprehensive specification of the logic (abstract syntax, semantics, proof calculus, core theories) is available as [ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/6xx/698.pdf technical report]. | A comprehensive specification of the logic (abstract syntax, semantics, proof calculus, core theories) is available as [ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/6xx/698.pdf technical report]. |
Revision as of 08:32, 27 October 2011
This page gives a brief summary of documents describing Event-B's logic aka mathematical language.
Rodin Handbook
Mathematical Notation Reference Section in Rodin Handbook
Specification Documents
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).
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.