Structured Types - Revision history

imported>Mathieu: Category:Work in progress Category:Design

2009-08-12T12:41:25Z

Category:Work in progress Category:Design

← Older revision		Revision as of 12:41, 12 August 2009
Line 547:		Line 547:

	To be done...		To be done...

			[[Category:Work in progress]] [[Category:Design]]

imported>WikiSysop: /* Sub-Typing */

2009-05-08T09:00:41Z

Sub-Typing

← Older revision		Revision as of 09:00, 8 May 2009
Line 334:		Line 334:
	\end{array}		\end{array}
	</math></center>		</math></center>


			It might seem that we should always specify that subtypes are disjoint, but this is not so.
			Not making them disjoint allows us to represent a form of 'mulitple inheritance'.
			For example, we could declare a new subtype ''ReqConfMessage'' that subsets both
			''ReqMessage'' and ''ConfMessage'':
			<center>
			{{SimpleHeader}}
			\|<math> \begin{array}{l}
			\textbf{CONSTANTS}~~ \textit{ReqConfMessage},\\
			\textbf{AXIOMS}\\
			~~~~\begin{array}{l}
			\textit{ReqConfMessage} \subseteq \textit{ReqMessage} \\
			\textit{ReqConfMessage} \subseteq \textit{ConfMessage} \\
			\end{array}
			\end{array}
			</math>
			\|}
			</center>
			Elements of ''ReqConfMessage'' will have the fields of both subtypes, i.e.,
			''sender'', ''receiver'', ''ident'', ''product'', ''amount'' and ''price''.

			This combined subtype could be further extended:
			<center>
			{{SimpleHeader}}
			\|<math> \begin{array}{l}
			\textbf{EXTEND~~ RECORD}~~ \textit{ReqConfMessage}~~\textbf{WITH}\\
			~~~~~~~~~~~~ time\in TIME\\ \end{array}
			</math>
			\|}
			</center>

imported>WikiSysop: /* Constructor-based Records */

2009-05-08T08:48:52Z

Constructor-based Records

← Older revision		Revision as of 08:48, 8 May 2009
Line 361:		Line 361:
	\|<math> \begin{array}{l}		\|<math> \begin{array}{l}
	\textbf{SETS}~~ R\\		\textbf{SETS}~~ R\\
	\textbf{CONSTANTS}~~ mk\!-\!R,~ e,~ f\\		\textbf{CONSTANTS}~~ \textit{mk-R},~ e,~ f\\
	\textbf{AXIOMS}\\		\textbf{AXIOMS}\\
	~~~~\begin{array}{l}		~~~~\begin{array}{l}
	mk\!-\!R \in (E\times F) \tbij R\\		\textit{mk-R} ~\in~ (E\times F) \tbij R\\
	e \in R \tfun E\\		e \in R \tfun E\\
	f \in R \tfun F\\		f \in R \tfun F\\
	\forall x,y \cdot e( mk\!-\!R(x\mapsto y) ) = x \\		\forall x,y \cdot e( \textit{mk-R}(x\mapsto y) ) = x \\
	\forall x,y \cdot f( mk\!-\!R(x\mapsto y) ) = y		\forall x,y \cdot f( \textit{mk-R}(x\mapsto y) ) = y
	\end{array}		\end{array}
	\end{array}		\end{array}
Line 387:		Line 387:
	\begin{array}[t]{l}		\begin{array}[t]{l}
	\textbf{BEGIN}\\		\textbf{BEGIN}\\
	~~~~ vs := vs \cup \{~ mk\!-\!R(e1,f1) ~\} \\		~~~~ vs := vs \cup \{~ \textit{mk-R}(e1,f1) ~\} \\
	\textbf{END}		\textbf{END}
	\end{array}		\end{array}
Line 399:		Line 399:
	to get the refinement to work correctly, we would need to define a relationship between the original		to get the refinement to work correctly, we would need to define a relationship between the original
	record and the extended version. This merits further exploration.		record and the extended version. This merits further exploration.


	==Projections versus Constructors==		==Projections versus Constructors==

imported>WikiSysop: /* Projections versus Constructors */

2009-05-08T08:44:07Z

Projections versus Constructors

← Older revision		Revision as of 08:44, 8 May 2009
Line 453:		Line 453:
	{{SimpleHeader}}		{{SimpleHeader}}
	\|<math> \begin{array}{l}		\|<math> \begin{array}{l}
	\textbf{AXIOMS}\\		\textbf{AXIOMS}~~~~~~\textit{ (Closing) }\\
	~~~~\begin{array}{l}		~~~~\begin{array}{l}
	e \otimes f ~\in~ R \tinj (E\times F)		e \otimes f ~\in~ R \tinj (E\times F)
Line 473:		Line 473:
	{{SimpleHeader}}		{{SimpleHeader}}
	\|<math> \begin{array}{l}		\|<math> \begin{array}{l}
	\textbf{AXIOMS}\\		\textbf{AXIOMS}~~~~~~\textit{ (Feasibility) }\\
	~~~~\begin{array}{l}		~~~~\begin{array}{l}
	e \otimes f ~\in~ R \tsur (E\times F)		e \otimes f ~\in~ R \tsur (E\times F)

imported>WikiSysop: /* Projections versus Constructors */

2009-05-08T08:42:05Z

Projections versus Constructors

← Older revision		Revision as of 08:42, 8 May 2009
Line 462:		Line 462:
	</center>		</center>

	Once this 'closing' axiom is introduced, we can no longer introduce new fields to the record structure - at least		Once this ''closing'' axiom is introduced, we can no longer introduce new fields to the record structure - at least
	not without introducing an inconsistency. If we were to now add a field ''g'', the ''closing'' axiom would mean		not without introducing an inconsistency. If we were to now add a field ''g'', the closing axiom would mean
	that records whose ''e'' and ''f'' fields are the same, must be correspond to the same record ''r'' even if they differ		that records whose ''e'' and ''f'' fields are the same, must be correspond to the same record ''r'' even if they differ
	in the ''g'' field. But since ''g'' is a function, different ''g'' values cannot be related to the same record ''r''.		in the ''g'' field. But since ''g'' is a function, different ''g'' values cannot be related to the same record ''r''.

imported>WikiSysop: /* Projections versus Constructors */

2009-05-08T08:38:20Z

Projections versus Constructors

@@ Line 466: / Line 466: @@
 that records whose ''e'' and ''f'' fields are the same, must be correspond to the same record ''r'' even if they differ
 in the ''g'' field.  But since ''g'' is a function, different ''g'' values cannot be related to the same record ''r''.
 ==Recursive Structured Types==

imported>WikiSysop: /* Projections versus Constructors */

2009-05-07T20:18:18Z

Projections versus Constructors

← Older revision		Revision as of 20:18, 7 May 2009
Line 445:		Line 445:
	The inverse of the direct product		The inverse of the direct product
	<math>(e \otimes f)^{-1}</math> relates pairs of type <math>E\times F</math> to elements of type <math>R</math>.		<math>(e \otimes f)^{-1}</math> relates pairs of type <math>E\times F</math> to elements of type <math>R</math>.
	If we specify that <math>(e \otimes f)</math> is injective, i.e., its inverse is a function, then <math>(e \otimes f)^{-1}</math>		If we specify that <math>e \otimes f</math> is injective, i.e., its inverse is a function, then <math>(e \otimes f)^{-1}</math>
	becomes a constructor ~~functions~~ for records of type <math>R</math>.		becomes a constructor function for records of type <math>R</math>.

	This means that an open record structure can be 'closed-off' by the addition of an axiom stating that		This means that an open record structure can be 'closed-off' by the addition of an axiom stating that
Line 462:		Line 462:
	</center>		</center>

	~~The addition of~~ this 'closing' axiom ~~means~~ we ~~cannot~~ introduce new fields to the record structure - at least		Once this 'closing' axiom is introduced, we can no longer introduce new fields to the record structure - at least
	not without introducing an inconsistency. If we were to now add a field ''g'', the ''closing'' axiom would mean		not without introducing an inconsistency. If we were to now add a field ''g'', the ''closing'' axiom would mean
	that records whose ''e'' and ''f'' fields are the same, must be correspond to the same record ''r'' ~~event~~ if they differ		that records whose ''e'' and ''f'' fields are the same, must be correspond to the same record ''r'' even if they differ
	in the ''g'' field. But since ''g'' is a function, different ''g'' values cannot be related to the same record ''r''.		in the ''g'' field. But since ''g'' is a function, different ''g'' values cannot be related to the same record ''r''.

imported>WikiSysop: Records moved to Structured Types

2009-05-07T19:04:01Z

Records moved to Structured Types

← Older revision	Revision as of 19:04, 7 May 2009
(No difference)

imported>WikiSysop: Modelling Tips/Records moved to Records

2009-05-07T19:03:31Z

Modelling Tips/Records moved to Records

← Older revision	Revision as of 19:03, 7 May 2009
(No difference)

imported>WikiSysop at 19:01, 7 May 2009

2009-05-07T19:01:58Z

@@ Line 471: / Line 471: @@
 It is well known how to deal with recursive records using the constructor approach.
 This is explored further in the context of Event-B and Rodin as part of the mathematical extension
-work. (see [[Mathematical_extensions]]).
+work where proposals for inductive datatypes are made (see [[Mathematical_extensions]]).
 ==Structured Variables==