Difference between revisions of "Event-B Mathematical Language"

From Event-B
Jump to navigationJump to search
imported>Wohuai
m
imported>Wohuai
Line 8: Line 8:
 
=Specification Documents=
 
=Specification Documents=
  
A comprehensive specification of the logic (abstract syntax, semantics, proof calculus, core theories) is currently being written.
+
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].
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].
 
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].

Revision as of 19:25, 10 November 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 (see How Rodin Deviates from Abrial's Book).

Specification Documents

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.