How Rodin Deviates from Abrial's Book - Revision history

imported>Laurent: Added link for JRA's book

2012-01-25T11:10:47Z

Added link for JRA's book

← Older revision		Revision as of 11:10, 25 January 2012
Line 1:		Line 1:
	This page summarizes (some) differences between the version of Event-B described in Abrial's book an the version implemented by Rodin.		This page summarizes (some) differences between the version of Event-B described in [http://www.event-b.org/abook.html Abrial's book] and the version implemented by Rodin.

	=== Types ===		=== Types ===

imported>Ladenberger: /* Well-Definedness */

2011-10-27T10:42:37Z

Well-Definedness

← Older revision		Revision as of 10:42, 27 October 2011
Line 11:		Line 11:
	On the one hand, the proof calculus devised in Chapter 9 allows one to prove <math>1\div 0 = 1\div0</math>.		On the one hand, the proof calculus devised in Chapter 9 allows one to prove <math>1\div 0 = 1\div0</math>.
	On the other hand, it is impossible to prove <math>1\div0=1\div0</math> in Rodin, because <math>1\div0</math> is regarded as ill-defined.		On the other hand, it is impossible to prove <math>1\div0=1\div0</math> in Rodin, because <math>1\div0</math> is regarded as ill-defined.
	Well-definedness is described [http://handbook.event-b.org/current/html/well_definedness.html ~~Well-definedness in Event-B\|~~here] and [[Event-B Mathematical Language\|here]].		Well-definedness is described [http://handbook.event-b.org/current/html/well_definedness.html here] and [[Event-B Mathematical Language\|here]].

	=== Proof Calculus ===		=== Proof Calculus ===

	The proof calculus used in Abrial's book is different from the proof calculus implemented by Rodin, i.e., rules have different names, and some rules available in Abrial's book are unavailable in Rodin and vice versa.		The proof calculus used in Abrial's book is different from the proof calculus implemented by Rodin, i.e., rules have different names, and some rules available in Abrial's book are unavailable in Rodin and vice versa.

imported>Ladenberger: /* Well-Definedness */

2011-10-27T10:42:26Z

Well-Definedness

← Older revision		Revision as of 10:42, 27 October 2011
Line 11:		Line 11:
	On the one hand, the proof calculus devised in Chapter 9 allows one to prove <math>1\div 0 = 1\div0</math>.		On the one hand, the proof calculus devised in Chapter 9 allows one to prove <math>1\div 0 = 1\div0</math>.
	On the other hand, it is impossible to prove <math>1\div0=1\div0</math> in Rodin, because <math>1\div0</math> is regarded as ill-defined.		On the other hand, it is impossible to prove <math>1\div0=1\div0</math> in Rodin, because <math>1\div0</math> is regarded as ill-defined.
	Well-definedness is described [[Well-definedness in Event-B\|here]] and [[Event-B Mathematical Language\|here]].		Well-definedness is described [http://handbook.event-b.org/current/html/well_definedness.html Well-definedness in Event-B\|here] and [[Event-B Mathematical Language\|here]].

	=== Proof Calculus ===		=== Proof Calculus ===

	The proof calculus used in Abrial's book is different from the proof calculus implemented by Rodin, i.e., rules have different names, and some rules available in Abrial's book are unavailable in Rodin and vice versa.		The proof calculus used in Abrial's book is different from the proof calculus implemented by Rodin, i.e., rules have different names, and some rules available in Abrial's book are unavailable in Rodin and vice versa.

imported>Wohuai: New page: This page summarizes (some) differences between the version of Event-B described in Abrial's book an the version implemented by Rodin. === Types === One may understand from Chapter 9 tha...

2010-08-30T13:34:16Z

New page: This page summarizes (some) differences between the version of Event-B described in Abrial's book an the version implemented by Rodin. === Types === One may understand from Chapter 9 tha...

New page

This page summarizes (some) differences between the version of Event-B described in Abrial's book an the version implemented by Rodin.

=== Types ===

One may understand from Chapter 9 that Event-B is based on naive set theory, and therefore has terms like <math>\{X | X \notin X\}</math>.
This is not the case in Rodin: in Rodin terms are typed similarly as in higher order logic, and <math>\{X | X \notin X\}</math> is therefore ill-typed.
For the details see the page about the [[Event-B Mathematical Language]].

=== Well-Definedness ===

On the one hand, the proof calculus devised in Chapter 9 allows one to prove <math>1\div 0 = 1\div0</math>.
On the other hand, it is impossible to prove <math>1\div0=1\div0</math> in Rodin, because <math>1\div0</math> is regarded as ill-defined.
Well-definedness is described [[Well-definedness in Event-B|here]] and [[Event-B Mathematical Language|here]].

=== Proof Calculus ===

The proof calculus used in Abrial's book is different from the proof calculus implemented by Rodin, i.e., rules have different names, and some rules available in Abrial's book are unavailable in Rodin and vice versa.