Difference between revisions of "Event-B Mathematical Language"
imported>Wohuai |
imported>Wohuai |
||
Line 1: | Line 1: | ||
− | + | This page gives a brief summary of documents describing Event-B's logic aka mathematical language. | |
− | + | =Introductory Texts= | |
− | The | + | 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 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 [http://bscw.cs.ncl.ac.uk/bscw/bscw.cgi/d104165/logic.pdf current draft]. | ||
+ | |||
+ | 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]]. | The changes between these two versions are summarized in [[Changes_to_the_Mathematical_Language_of_Event-B]]. | ||
[[Category:User documentation]] | [[Category:User documentation]] | ||
[[Category:Event-B]] | [[Category:Event-B]] |
Revision as of 11:53, 30 August 2010
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.