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

From Event-B

Jump to navigationJump to searchimported>Ladenberger |
imported>Ladenberger |
||

Line 3: | Line 3: | ||

=Rodin Handbook= | =Rodin Handbook= | ||

− | [http://handbook.event-b.org/current/html/mathematical_notation.html Mathematical Notation | + | [http://handbook.event-b.org/current/html/mathematical_notation.html Rodin Handbook (Mathematical Notation)] |

=Specification Documents= | =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]. |

− | Event-B's concrete syntax (V2, supported since Rodin 1.0.0) is specified in [http://deploy-eprints.ecs.soton.ac.uk/11/4/kernel_lang.pdf kernel_lang.pdf]. | + | *Event-B's concrete syntax (V2, supported since Rodin 1.0.0) is specified in [http://deploy-eprints.ecs.soton.ac.uk/11/4/kernel_lang.pdf kernel_lang.pdf].An older version (available in [http://deploy-eprints.ecs.soton.ac.uk/11/2/mathLanguage-2007-10-26.pdf 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]]. |

− | An older version (available in [http://deploy-eprints.ecs.soton.ac.uk/11/2/mathLanguage-2007-10-26.pdf 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 [http://lfm.iti.uni-karlsruhe.de/download/EventB_Summary.pdf A Concise Summary of the Event B mathematical tool]. | + | *There is also [http://lfm.iti.uni-karlsruhe.de/download/EventB_Summary.pdf A Concise Summary of the Event B mathematical tool]. |

[[Category:User documentation]] | [[Category:User documentation]] | ||

[[Category:Event-B]] | [[Category:Event-B]] |

## Revision as of 08:34, 27 October 2011

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

# Rodin Handbook

Rodin Handbook (Mathematical Notation)

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