Changes to the Mathematical Language of Event-B - Revision history

imported>Nicolas: /* Partition */

2009-04-17T12:38:59Z

Partition

← Older revision		Revision as of 12:38, 17 April 2009
Line 80:		Line 80:

	which is a particular case of a set being defined by listing all its elements.		which is a particular case of a set being defined by listing all its elements.


			=== Partition Wizard ===
			{{TODO}}

	== Operator Associativity ==		== Operator Associativity ==

imported>Laurent at 08:45, 7 April 2009

2009-04-07T08:45:54Z

← Older revision		Revision as of 08:45, 7 April 2009
Line 1:		Line 1:
	This document describes the evolution of the Event-B mathematical language that ~~will soon take place~~. ~~The previous version~~ of the language ~~will still be supported~~.		This document describes the evolution of the Event-B mathematical language that happened in release 1.0.0. See [[Event-B_Mathematical_Language]] for a full description of the language.

	== Generic Identity and Projections ==		== Generic Identity and Projections ==

imported>Mathieu: category

2009-04-06T14:05:48Z

imported>Laurent: /* Operator Associativity */

2009-04-01T12:43:55Z

Operator Associativity

← Older revision		Revision as of 12:43, 1 April 2009
Line 96:		Line 96:
	* bijection		* bijection

	have no more relative priorities and ~~lose~~ associativity. Instead, users have to make it explicit by entering parenthesis in formulas.		have no more relative priorities and loose associativity. Instead, users have to make it explicit by entering parenthesis in formulas.

imported>Laurent: /* Identity and Projections */

2009-03-12T17:57:40Z

Identity and Projections

← Older revision		Revision as of 17:57, 12 March 2009
Line 1:		Line 1:
	This document describes the evolution of the Event-B mathematical language that will soon take place. The previous version of the language will still be supported.		This document describes the evolution of the Event-B mathematical language that will soon take place. The previous version of the language will still be supported.

	== Identity and Projections ==		== Generic Identity and Projections ==

	Three operators were still unary while they could be atomic:		Three operators were still unary while they could be atomic and generic:
	* the identity relation <math>\id</math>		* the identity relation <math>\id</math>
	* the first projection <math>\prjone</math>		* the first projection <math>\prjone</math>

imported>Nicolas: /* Identity and Projections */

2009-03-12T16:22:13Z

Identity and Projections

← Older revision		Revision as of 16:22, 12 March 2009
Line 8:		Line 8:
	* the second projection <math>\prjtwo</math>		* the second projection <math>\prjtwo</math>

	These operators are defined as follows:		These operators are defined as follows in the old version:

	<math>		<math>

imported>Nicolas: /* Identity and Projections */

2009-03-12T16:18:14Z

Identity and Projections

← Older revision		Revision as of 16:18, 12 March 2009
Line 10:		Line 10:
	These operators are defined as follows:		These operators are defined as follows:

	<math>		<math>
	\begin{matrix}		\begin{matrix}
	E\mapsto F &\in\id(S) && E\in S\;\land\; F = E\\		E\mapsto F &\in\id(S) && E\in S\;\land\; F = E\\
	(E\mapsto F)\mapsto G &\in\prjone(r)		(E\mapsto F)\mapsto G &\in\prjone(r)
Line 17:		Line 17:
	(E\mapsto F)\mapsto G &\in\prjtwo(r)		(E\mapsto F)\mapsto G &\in\prjtwo(r)
	&& E\mapsto F\in r\;\land\; G = F .		&& E\mapsto F\in r\;\land\; G = F .
	\end{matrix}		\end{matrix}
	</math>		</math>

	If we drop the parameter, we get		If we drop the parameter, we get
Line 24:		Line 24:
	operator. The new definitions are		operator. The new definitions are

	<math>		<math>
	\begin{matrix}		\begin{matrix}
	E\mapsto F &\in\id && E = F\\		E\mapsto F &\in\id && E = F\\
	(E\mapsto F)\mapsto G &\in\prjone && E = G\\		(E\mapsto F)\mapsto G &\in\prjone && E = G\\
	(E\mapsto F)\mapsto G &\in\prjtwo && F = G .		(E\mapsto F)\mapsto G &\in\prjtwo && F = G .
	\end{matrix}		\end{matrix}
	</math>		</math>

	We have the following equivalence between the old		We have the following equivalence between the old
	and the new versions of the operators		and the new versions of the operators

	<math>		<math>
	\begin{matrix}		\begin{matrix}
	\textbf{Old Version} & \textbf{New Version}\\		\textbf{Old Version} & \textbf{New Version}\\
	\id(S) & S\domres id\\		\id(S) & S\domres id\\
	\prjone(r) & r\domres\prjone\\		\prjone(r) & r\domres\prjone\\
	\prjtwo(r) & r\domres\prjtwo .		\prjtwo(r) & r\domres\prjtwo .
	\end{matrix}		\end{matrix}
	</math>		</math>

	Moreover, in the case where the parameter is not needed, then it can		Moreover, in the case where the parameter is not needed, then it can
Line 48:		Line 48:
	to express that a relation <math>r</math> is irreflexive, one would now write		to express that a relation <math>r</math> is irreflexive, one would now write
	<math>r\binter\id = \emptyset</math>.		<math>r\binter\id = \emptyset</math>.



	== Partition ==		== Partition ==

imported>Nicolas: /* Operator Associativity */

2009-03-12T16:11:12Z

Operator Associativity

← Older revision		Revision as of 16:11, 12 March 2009
Line 85:		Line 85:
	== Operator Associativity ==		== Operator Associativity ==

	~~{{TODO}}~~		Operators used to build sets of relations or functions, viz.
			* relation
			* total relation
			* surjective relation
			* total surjective relation
			* partial function
			* total function
			* partial injection
			* total injection
			* partial surjection
			* total surjection
			* bijection

			have no more relative priorities and lose associativity. Instead, users have to make it explicit by entering parenthesis in formulas.

imported>Nicolas: /* Partition */

2009-03-12T15:28:06Z

Partition

← Older revision		Revision as of 15:28, 12 March 2009
Line 56:		Line 56:

	<math>		<math>
	\begin{~~matrix~~}		\begin{array}{ll}
	partition(E_0, E_1, \ldots, E_n)\defi &		partition(E_0, E_1, \ldots, E_n)\defi &
	E_0 = E_1\bunion \cdots\bunion E_n \\ &		E_0 = E_1\bunion \cdots\bunion E_n \\ &
Line 63:		Line 63:
	\;\land\; E_{n-1}\binter E_n = \emptyset \\ &		\;\land\; E_{n-1}\binter E_n = \emptyset \\ &
	(\;\land\; i \ne j \limp E_i \binter E_j = \emptyset ) \\		(\;\land\; i \ne j \limp E_i \binter E_j = \emptyset ) \\
	\end{~~matrix~~}		\end{array}
	</math>		</math>

Line 80:		Line 80:
	\end{array}		\end{array}
	</math>		</math>

			which is a particular case of a set being defined by listing all its elements.

	== Operator Associativity ==		== Operator Associativity ==

	{{TODO}}		{{TODO}}

imported>Nicolas: /* Partition */

2009-03-12T15:21:06Z

Partition

@@ Line 53: / Line 53: @@
 == Partition ==
-{{TODO}}
+A new partition predicate is introduced. It is intended to provide an easier way to enter enumerated sets, while getting rid of the <math>\frac{n(n-1)}{2}</math> axioms needed to express pairwise distinctness (or disjointness). The partition operator is defined as follows:
 == Operator Associativity ==
 {{TODO}}

← Older revision		Revision as of 14:05, 6 April 2009
Line 97:		Line 97:

	have no more relative priorities and loose associativity. Instead, users have to make it explicit by entering parenthesis in formulas.		have no more relative priorities and loose associativity. Instead, users have to make it explicit by entering parenthesis in formulas.

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