Difference between revisions of "Event-B Mathematical Language"

From Event-B
Jump to: navigation, search
(Specification Documents: Updated link to concise summary and added refcard)
 
(2 intermediate revisions by one other user not shown)
Line 1: Line 1:
{| class="wikitable" style="font-style:italic; text-align: center; font-size:120%; border: 3px dashed red;"
 
|-
 
! scope="col" | Do not edit!  This content has been migrated to Subversion.
 
|-
 
|([http://handbook.event-b.org Nightly Handbook Build])
 
|}
 
 
 
This page gives a brief summary of documents describing Event-B's logic aka mathematical language.
 
This page gives a brief summary of documents describing Event-B's logic aka mathematical language.
  
=Introductory Texts=
+
=Rodin Handbook=
  
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".
+
[http://handbook.event-b.org/current/html/mathematical_notation.html Rodin Handbook (Mathematical Notation)]
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=
 
=Specification Documents=
  
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].
+
*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]]).
 +
 
 +
*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 [[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

  • A comprehensive specification of the logic (abstract syntax, semantics, proof calculus, core theories) is available as technical report.