Event-B Mathematical Language: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Ladenberger No edit summary |
imported>Laurent →Specification Documents: Updated link to concise summary and added refcard |
||
| Line 13: | Line 13: | ||
*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]]. | *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]]. | ||
*There is also [ | *There is also [[Media:EventB-Summary.pdf|A Concise Summary of the Event B mathematical too]] and the associated [[Media:EventB-Summary-refcard.pdf|reference card]]. | ||
[[Category:User documentation]] | [[Category:User documentation]] | ||
[[Category:Event-B]] | [[Category:Event-B]] | ||
Latest revision as of 11:28, 23 January 2014
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 too and the associated reference card.
