Event-B Mathematical Language - Revision history

imported>Laurent: /* Specification Documents */ Updated link to concise summary and added refcard

2014-01-23T11:28:51Z

Specification Documents: Updated link to concise summary and added refcard

← Older revision		Revision as of 11:28, 23 January 2014
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 [~~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]]

imported>Ladenberger at 08:34, 27 October 2011

2011-10-27T08:34:58Z

← Older revision		Revision as of 08:34, 27 October 2011
Line 3:		Line 3:
	=Rodin Handbook=		=Rodin Handbook=

	[http://handbook.event-b.org/current/html/mathematical_notation.html Mathematical Notation ~~Reference Section in Rodin Handbook~~]		[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]]

imported>Ladenberger at 08:32, 27 October 2011

2011-10-27T08:32:58Z

← Older revision		Revision as of 08:32, 27 October 2011
Line 1:		Line 1:
	~~{\| class="wikitable" style="font-style:italic; text-align: center; font-size:120%; border: 3px dashed red;"~~		This page gives a brief summary of documents describing Event-B's logic aka mathematical language.
	\|-
	~~! 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~~.		=Rodin Handbook=

			[http://handbook.event-b.org/current/html/mathematical_notation.html Mathematical Notation Reference Section in Rodin Handbook]

	=~~Introductory Texts~~=		=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]]).

	~~=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].		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].

imported>Ladenberger at 15:18, 16 September 2011

2011-09-16T15:18:56Z

← Older revision		Revision as of 15:18, 16 September 2011
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.

imported>Nomeata at 15:28, 24 March 2011

2011-03-24T15:28:52Z

← Older revision		Revision as of 15:28, 24 March 2011
Line 13:		Line 13:
	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.		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]].

			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]]

imported>Wohuai at 19:25, 10 November 2010

2010-11-10T19:25:49Z

← Older revision		Revision as of 19:25, 10 November 2010
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].

imported>Wohuai at 13:35, 30 August 2010

2010-08-30T13:35:08Z

← Older revision		Revision as of 13:35, 30 August 2010
Line 4:		Line 4:

	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 ~~and / or neglect important aspects of the logic~~ (~~e.g. types and well-definedness~~).		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=

imported>Wohuai at 11:53, 30 August 2010

2010-08-30T11:53:35Z

← Older revision		Revision as of 11:53, 30 August 2010
Line 1:		Line 1:
	~~There are two versions~~ of ~~the~~ mathematical language.		This page gives a brief summary of documents describing Event-B's logic aka mathematical language.

	~~The latest version (V2) has been supported by the Rodin platform since release 1.0.0 and is available in [http://deploy-eprints.ecs.soton.ac.uk/11/4/kernel_lang.pdf PDF format].~~		=Introductory Texts=

	The ~~original version (also available~~ in [http://deploy-eprints.ecs.soton.ac.uk/11/2/~~mathLanguage~~-~~2007~~-~~10-26~~.~~pdf PDF format]) was used~~ by the ~~Rodin platform up to releases 0~~.9.x.		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]]

imported>Wohuai at 11:49, 17 August 2010

2010-08-17T11:49:58Z

← Older revision		Revision as of 11:49, 17 August 2010
Line 6:		Line 6:

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

	~~Proposals for changes to the mathematical language specification are collected [[Proposals of Changes to the Mathematical Language Specification\|here]].~~

	[[Category:User documentation]]		[[Category:User documentation]]
	[[Category:Event-B]]		[[Category:Event-B]]

imported>Wohuai at 09:22, 11 January 2010

2010-01-11T09:22:29Z

← Older revision		Revision as of 09:22, 11 January 2010
Line 6:		Line 6:

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

			Proposals for changes to the mathematical language specification are collected [[Proposals of Changes to the Mathematical Language Specification\|here]].

	[[Category:User documentation]]		[[Category:User documentation]]
	[[Category:Event-B]]		[[Category:Event-B]]