Difference between pages "Records Extension" and "Help:Preferences"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Colin
 
imported>Mathieu
m (importing help from mediawiki)
 
Line 1: Line 1:
−
This page is under development.
 
  
−
It is intended to be a user oriented manual for using records in Event-B. This page is derived from the  [[Structured_Types|Structured Types]] page which gives a more theoretical description of the origin of the Records extension.
 
  
−
==Introduction==
+
Clicking on the [[special:preferences|my preferences]] link in the upper right while logged in allows you to change your preferences. You will be presented with the User profile section, as well as a bar of tabs across the top for changing other types of settings.
−
The Event-B mathematical language currently does not support a syntax for the direct definition of structured types such as records or class structures.
 
−
The Records Extension introduces a new modelling construct to provide a notion of structured types in Event-B Contexts.
 
  
−
Currently, structured variables are not supported. Variables that are typed as an instance of a record type can be thought of as identifying a particular record value. Hence it is not possible to vary an individual field, the variable must be assigned a complete new record value instance. To vary an individual field this new record value instance can be selected to have the same field value for every other field.)
+
==User profile==
 +
===User profile===
 +
* ''Username'': Your user name. Only bureaucrats can change your username, and the wiki must also have the [[mw:Extension:Renameuser|Renameuser extension]] installed.
 +
* ''User ID'': A number assigned to your account when you created it (for example, if your number is 42 you are the 42nd user to sign up at this particular wiki). This number is used for internal purposes.
 +
* ''Number of edits'': How many edits you have made. Not all wikis will have this.
 +
* ''Real name'': If provided, this will be used for attribution (rather than using your username). Providing your real name is entirely optional. Some wikis do not have this option.
 +
* ''E-mail'': Your email address, if you have supplied one. You can also change or remove your address here.
 +
* ''Nickname'': When you sign your name (using <code><nowiki>~~~~</nowiki></code>), what you enter here will be used at the start instead of a simple link to your user page. By default, anything you enter here will be wrapped with <code><nowiki>[[ ]]</nowiki></code>; if you want to use special linking, enable ''Raw signatures (without automatic link)''.
 +
* ''Language'': This controls what language the interface is displayed in.  MediaWiki's default interface includes localisations for all supported languages, but this is not necessarily the case with extensions or custom skins. Page text will '''not''' be translated, nor will templates (unless the templates integrate text localisation).
  
−
==UI Extensions==
+
===Change password===
−
The '''Event-B editor''' is extended to include two new top level clauses. These are '''Record Declarations''' and '''Record Extensions'''.
+
To change your password, enter your old password in the first box and your new password in the last two. If you want this site to remember your login, check ''Remember my login on this computer''. Note that this function requires you to have cookies enabled in your browser, and if your cookie is cleared or expires you will no longer be remembered.
  
−
Records (or sub-records) are introduced in the Record Declarations clause. Records that are introduced here without a '''Supertypes''' clause are equivalent to carrier sets. Those that have a Supertypes clause are equivalent to constants that are a subset of the referenced (i.e. subtyped) record.
+
===E-mail===
 +
If you have supplied an email address, you will need to click the ''verify address'' button in order to use these functions. You will receive an email; simply open it and follow the link to enable the following functions.
  
−
Record Extensions may only add new fields to a record that has previously been declared in a Record Declaration. The extended record is referenced in an 'extends' clause.
+
* ''E-mail me when a page I'm watching is changed''
 +
* ''E-mail me when my user talk page is changed''
 +
* ''E-mail me also for minor edits of pages''
 +
* ''Enable e-mail from other users''
 +
* ''Send me copies of emails I send to other users''
  
−
The '''Event-B navigator''' is extended to show a new node '''Records'''. Under this node are listed the records and records extensions in the Context.
+
===Languages===
−
Record Extensions are displayed as the name of the extended record appended with a + sign. Each record or record extension can be expanded to show the owned fields. (Note that this list is not cumulative, only the new fields are shown).
 
−
(Currently in the Navigator, the Records node is shown as the first item in the Context whereas eleswhere it appears between carrier sets and constants. This is due to a limitation in the Rodin tool extension facilities).
 
  
−
The '''Outline''' panel shows the records followed by record extensions as a plain list without the Records node. Again, the record or record extension can be expanded to show the fields.
+
From your preferences you can select what language you would like the interface to be in. Only the buttons like 'edit' and 'talk', in addition to a few pages in the sidebar, will be affected. The main text of the pages will not be changed by this for the vast majority of pages, although there are a few pages where it will, like some in the Wikimedia Meta Wiki.
  
−
In all  cases, the '''icon''' used for a record reflects its equivalence. That is, if it does not have a supertypes clause, it is displayed with the same icon as a carrier set. otherwise it is displayed with the same icon as a constant.
+
==Skin==
 +
Here you can choose the skin you want to use (use ''Preview'' if you want to see a skin before you choose it). By default, MediaWiki includes the following skins:
 +
* Chick
 +
* Classic
 +
* Cologne Blue
 +
* MonoBook (default)
 +
* MySkin
 +
* Nostalgia
 +
* Simple
 +
While you can choose whatever skin you like, bear in mind that some wikis will incorporate templates or layout elements that will not display as intended in some of these skins. Generally speaking, sticking with MonoBook (or whatever the wiki's default skin is) will ensure you see pages as intended.
  
−
==Semantics of Records==
+
==Math==
−
The semantics of Records are given by their translation into 'pure' Event-B. This translation is performed by extensions to the static checker which generates a 'checked context' (.BCC file) containing pure Event-B from an unchecked (.BUC file) containing record elements. Hence the translated Event-B is not visible to the user.
+
Here you can control how mathematical equations described using the <code><nowiki><math></nowiki></code> tag will be displayed. Mathematical formulae uploaded as images or written outside the math tag will not be affected by this setting.
 +
* ''Always render PNG''
 +
* ''HTML if very simple or else PNG''
 +
* ''HTML if possible or else PNG''
 +
* ''Leave it as TeX (for text browsers)''
 +
* ''Recommended for modern browsers''
 +
* ''MathML if possible (experimental)''
  
−
<formatting/presentation of this will be improved>
+
==Files==
 +
Here you can determine how images will be displayed. Images displayed by direct pasting of a URL (if the wiki has it enabled) will not be affected by this setting.
  
−
Record R Supertypes <null> --> Carrier Set R
+
* ''Limit images on image description pages to'': This setting lets you choose how big image previews will be on the Image: pages. If you know what your current screen resolution is you may like to set this to one or two sizes smaller than your own screen. If you have a slow connection (such as dial-up) you may want to limit them to 320×240.
 +
* ''Thumbnail size'': Define how big you want thumbnails to appear. This setting will not affect thumbnails with dimensions determined by an editor, nor can it increase images beyond their original dimensions.
  
−
Record S Supertypes R          -->  Constant S,  Axiom S : POW(R)
+
==Date and time==
 +
The following is normally rendered depending on preferences:
  
−
Field f : F                                --> Constant f, Axiom f : R --> F
+
<pre>
 +
[[2001-01-05]] (or [[2001]]-[[01-05]]) (with leading zeros)
 +
[[2001]] [[January 5]] ([[2001]] [[January 05]])
 +
  [[January 5]], [[2001]] ([[January 05]], [[2001]])
 +
  [[5 January]] [[2001]] ([[05 January]] [[2001]])
 +
[[January 5]] ([[January 05]])
 +
[[5 January]] ([[05 January]])
 +
</pre>
  
−
[It may be instructive to open the *.bcc file with a text editor to examine the generated carrier sets, constants, and axioms]
+
With your current preference setting on this project the seven are rendered as follows:
  
 +
#[[2001-01-05]] ([[2001]]-[[01-05]])
 +
#[[2001]] [[January 5]] ([[2001]] [[January 05]])
 +
#[[January 5]], [[2001]] ([[January 05]], [[2001]])
 +
#[[5 January]] [[2001]] ([[05 January]] [[2001]])
 +
#[[January 5]] ([[January 05]])
 +
#[[5 January]] ([[05 January]])
  
−
==Usage==
+
The user-specified date format does not seem to work on the [[mw:]] wiki for links! It works in Recent Changes etc.
  
−
First define Records in the Record Declarations section. Some of these can subtype others but you need at least one that is not a subset, i.e. has no supertypes. Note that we decided not to allow records to subtype or extend Carrier Sets, but you can do the equivalent by defining a record without any fields and subtyping/extending that. Add fields and give them a type by entering an expression that evaluates to a set. (You can use records, fields, constants and sets  in the expression).
+
==Editing==
 +
Settings to control editing pages, including the size of the edit box displayed and whether to watch pages that you have edited or created automatically.
  
−
For Record Extensions just select the record you want to add new fields to from the drop down list. and then add the new fields.
+
==Recent changes==
 +
* ''Days to show in recent changes'': Here you can specify how far back the [[Help:Tracking changes|recent changes]] pages will go. Note that the list will stop prematurely if the number of edits is exceeded (see below)
 +
* ''Number of edits to show in recent changes'': Here you can specify how many edits should be displayed.
 +
* ''Hide minor edits in recent changes'': This enables you to hide edits marked as minor (see [[Help:Editing pages]]). Since some users will rapidly make a lot of tiny tweaks to update templates or fix spelling errors you may find enabling this to be useful. You can also turn this on temporarily from the recent changes page (see [[Help:Tracking changes]]).
 +
* ''Enhanced recent changes (JavaScript)'': Enhanced recent changes condenses edits into a per-page list. As indicated, this requires JavaScript to be enabled. See [[Help:Tracking changes]] for more information on this feature.
  
−
You can refer to records and fields in axioms/theorems. E.g., you could define a constant to be an instance of a record. In all cases you can refer to records and fields in the current or visible abstract (extended*) contexts.
+
==Watchlist==
  
−
You use fields as if they were functions (which is what they are in the checked context).  
+
==Search==
−
e,g if r1, belongs to myRecord which has a field myField : NAT then I could write in a predicate... myField(r1) > 5
+
Default settings for searches including how many results to display and how much context to show for each result. Check the boxes next to the namespaces which you want to show up, the first time that you search for something. You can override this when doing an actual search, by checking or unchecking the boxes at the bottom of the search results screen.
  
−
==Current Limitations==
+
''Administrators'': To change the namespace default preferences for new users (or users who haven't changed their preferences yet), see [[Manual:$wgNamespacesToBeSearchedDefault]]
−
* Records are not supported by the Camille text editor (see warning below)
 
−
* Records are not supported by the Pretty print facility
 
−
* Records are not supported by the Synthesis view facility
 
−
* Records are not supported by the EventB2Latex plug-in
 
−
* Records may have, at most, one supertype.
 
−
* Records may only have records as supertypes (not carrier sets)
 
  
−
==Warning==
+
==Misc==
 +
Other settings such as numbering and justification.
  
−
Records are not supported in the Camille text editor. Editing a context that contains records with the Camille editor may result in the Records being lost.
+
== See also ==
 +
* [[Help:Skins]]
  
−
==Copy of the original Structured Types wiki page from which this page is currently being derived <This will be removed> ==
+
[[Category:Help|Preferences]]
−
 
 
−
The Event-B mathematical language currently does not support a syntax for the direct definition of structured types such as records or class structures.
 
−
Nevertheless it is possible to model structured types using projection functions to represent the fields/attributes.  For example,
 
−
suppose we wish to model a record structure ''R'' with fields ''e'' and ''f'' (with type ''E'' and ''F'' respectively).
 
−
Let us use the following 'invented' syntax for this (based on VDM syntax but currently not part of Event-B syntax):
 
−
 
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{lcl}
 
−
\textbf{RECORD}~~~~ R &::&  e\in E\\
 
−
    &&  f \in F
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
We can model this structure in Event-B by introducing (in a context) a carrier set ''R'' and two
 
−
functions ''e'' and ''f'' as constants as follows:
 
−
 
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
\textbf{SETS}~~ R\\
 
−
\textbf{CONSTANTS}~~ e,~ f\\
 
−
\textbf{AXIOMS}\\
 
−
~~~~\begin{array}{l}
 
−
  e \in  R \tfun E\\
 
−
  f \in  R \tfun F\\
 
−
\end{array}
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
 
 
−
The (constant) functions ''e'' and ''f'' are ''projection'' functions that can be used to extract the appropriate field values.
 
−
That is, given an element <math>r\in R</math> representing a record structure, we write <math>e(r)</math> for the ''e'' component of ''r'' and <math>f(r)</math> for the ''f'' component of ''r''.
 
−
 
 
−
''E'' and ''F'' can be any  type definable in Event-B, including a type representing a record structure.
 
−
 
 
−
The approach to modelling structured types is based on a proposal by Evans and Butler
 
−
[http://eprints.ecs.soton.ac.uk/12024/].
 
−
We refer to this approach to modelling records as a ''projection-based'' approach. 
 
−
Later we will look at a ''constructor-based'' approach and make the link between the two approaches.
 
−
 
 
−
 
 
−
==Constructing Structured Values==
 
−
 
 
−
Suppose we have a variable ''v'' in a machine whose type is the structure ''R'' defined above:
 
−
 
 
−
<center>
 
−
<math>\textbf{INVARIANT}~~ v\in R</math>
 
−
</center>
 
−
 
 
−
We wish to assign a structured value to ''v'' whose ''e'' field has some value ''e1'' and whose ''f'' field has some value ''f1''.
 
−
This can be achieved by specifying the choice of an event parameter ''r'' whose fields are constrained by appropriate guards
 
−
and assigning parameter ''r'' to the machine variable ''v''.  This is shown in the following event:
 
−
 
 
−
<center><math>
 
−
Ev1 ~=\begin{array}[t]{l}
 
−
\textbf{ANY}~~ r ~~\textbf{WHERE} \\
 
−
~~~~ r \in R  \\
 
−
~~~~ e( r ) = e1 \\
 
−
~~~~ f( r ) = f1 \\
 
−
\textbf{THEN} \\
 
−
~~~~ v := r \\
 
−
\textbf{END}
 
−
\end{array}
 
−
</math></center>
 
−
 
 
−
If we only wish to update some fields and leave others changed, this needs to be done by specifying explicitly that some fields
 
−
remain unchanged.  This is shown in the following example where only the ''e'' field is modified:
 
−
 
 
−
<center><math>
 
−
Ev2 ~=\begin{array}[t]{l}
 
−
\textbf{ANY}~~ r ~~\textbf{WHERE} \\
 
−
~~~~ r \in R  \\
 
−
~~~~ e( r ) = e1 \\
 
−
~~~~ f( r ) = f(v) \\
 
−
\textbf{THEN} \\
 
−
~~~~ v := r \\
 
−
\textbf{END}
 
−
\end{array}
 
−
</math></center>
 
−
 
 
−
If we don't care about the value of some field (e.g., ''f''), we simply omit any guard on that field as follows:
 
−
 
 
−
<center><math>
 
−
Ev3 ~= \begin{array}[t]{l}
 
−
\textbf{ANY}~~ r ~~\textbf{WHERE} \\
 
−
~~~~ r \in R  \\
 
−
~~~~ e( r ) = e1 \\
 
−
\textbf{THEN} \\
 
−
~~~~ v := r \\
 
−
\textbf{END}
 
−
\end{array}
 
−
</math></center>
 
−
 
 
−
 
 
−
Sometimes we will wish to model a set of structured elements as a machine variable, e.g.,
 
−
 
 
−
<center>
 
−
<math>\textbf{INVARIANT}~~ vs\subseteq R</math>
 
−
</center>
 
−
 
 
−
We can add a structured element to this set using the following event:
 
−
 
 
−
<center><math>
 
−
AddElement ~=
 
−
\begin{array}[t]{l}
 
−
\textbf{ANY}~~ r ~~\textbf{WHERE} \\
 
−
~~~~ r \in R  \\
 
−
~~~~ e( r ) = e1 \\
 
−
~~~~ f( r ) = f1 \\
 
−
\textbf{THEN} \\
 
−
~~~~ vs := vs \cup \{r\} \\
 
−
\textbf{END}
 
−
\end{array}
 
−
</math></center>
 
−
 
 
−
==Extending Structured Types==
 
−
 
 
−
In a refinement we can introduce new fields to an existing structured type.  Suppose R is defined in context C1
 
−
with fields ''e'' and ''f'' as before.
 
−
For the refinement, suppose we wish to add a field ''g'' of type ''G'' to structured type ''R''.
 
−
Let us use the following invented syntax for this (not part of Event-B syntax):
 
−
 
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
\textbf{EXTEND~~ RECORD}~~ R ~~\textbf{WITH}~~  g\in G
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
This can be done by including the new field ''g'' as  projection function on ''R'' in a context ''C2'' (that extends ''C1'').
 
−
The new field is defined as follows:
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
\textbf{CONSTANTS}~~ g \\
 
−
\textbf{AXIOMS}\\
 
−
~~~~\begin{array}{l}
 
−
  g \in  R \tfun G \\
 
−
\end{array}
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
Above, we saw the ''AddElement'' event that adds a structured element to the set ''vs''.
 
−
We may want to specify a value for the new ''g'' field in the refinement of this event.
 
−
Using the event extension mechanism, this can be achieved as follows:
 
−
<center><math>
 
−
AddElement~= \begin{array}[t]{l}
 
−
\textbf{EXTENDS}~~ AddElement \\
 
−
\textbf{WHEN} \\
 
−
~~~~ g( r ) = g1 \\
 
−
\textbf{THEN} \\
 
−
~~~~ skip  \\
 
−
\textbf{END}
 
−
\end{array}
 
−
</math></center>
 
−
 
 
−
This is a form of superposition refinement where we add more data structure to the state by
 
−
adding a new field to elements of the structured type ''R''.  In the above event we strengthen
 
−
the specification by adding a guard using the event extension mechanism.
 
−
The event extension mechanism means that this short form is the same as specifying
 
−
the refined event as follows:
 
−
<center><math>
 
−
AddElement ~=
 
−
\begin{array}[t]{l}
 
−
\textbf{REFINES}~~ AddElement \\
 
−
\textbf{ANY}~~ r ~~\textbf{WHERE} \\
 
−
~~~~ r \in R  \\
 
−
~~~~ e( r ) = e1 \\
 
−
~~~~ f( r ) = f1 \\
 
−
~~~~ g( r ) = g1 \\
 
−
\textbf{THEN} \\
 
−
~~~~ vs := vs \cup \{r\} \\
 
−
\textbf{END}
 
−
\end{array}
 
−
</math></center>
 
−
 
 
−
==Sub-Typing==
 
−
 
 
−
Extension, as described above, is used when adding new fields to a structured type as part of a refinement step.
 
−
That is, at different abstraction levels, we may have different numbers of fields in a structured type.
 
−
 
 
−
Sometimes we wish to have different subtypes of a structure at the ''same'' abstraction level.
 
−
We can achieve this by defining subsets of the structure type and defining projection functions for those
 
−
subsets only.  For example suppose we define a message type that has ''sender'' and ''receiver'' fields as well
 
−
as a message ''identifier''.
 
−
In our invented notation this would be:
 
−
 
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{lcl}
 
−
\textbf{RECORD}~~~~ Message &::&  sender\in Agent\\
 
−
    &&  receiver \in Agent \\
 
−
    &&  ident \in Ident
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
In Event-B this would be:
 
−
 
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
\textbf{SETS}~~ Message\\
 
−
\textbf{CONSTANTS}~~ sender,~ receiver, ident\\
 
−
\textbf{AXIOMS}\\
 
−
~~~~\begin{array}{l}
 
−
  sender \in  Message \tfun Agent\\
 
−
  receiver \in  Message \tfun Agent\\
 
−
  ident \in Message \tfun Ident
 
−
\end{array}
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
We wish to have two subtypes of message, ''request'' messages and ''confirmation'' messages.
 
−
We define two subsets of ''Message'' as follows:
 
−
 
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
\textbf{CONSTANTS}~~ \textit{ReqMessage},~ \textit{ConfMessage}\\
 
−
\textbf{AXIOMS}\\
 
−
~~~~\begin{array}{l}
 
−
  \textit{ReqMessage} \subseteq Message \\
 
−
  \textit{ConfMessage} \subseteq Message \\
 
−
\end{array}
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
 
 
−
We require requests to have a product and an amount field and a confirmation to have a price field.
 
−
In our invented notation this would be specified as follows:
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
\textbf{EXTEND~~ RECORD}~~ \textit{ReqMessage}~~\textbf{WITH}\\
 
−
  ~~~~~~~~~~~~  product\in Product\\
 
−
  ~~~~~~~~~~~~  amount\in \nat\\
 
−
\textbf{EXTEND~~ RECORD}~~ \textit{ConfMessage}~~\textbf{WITH}\\
 
−
  ~~~~~~~~~~~~  price\in \nat\\ \end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
In Event-B the additional fields are specified as projection functions on the relevant message subsets:
 
−
 
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
\textbf{CONSTANTS}~~ product,~ amount,~ price\\
 
−
\textbf{AXIOMS}\\
 
−
~~~~\begin{array}{l}
 
−
  product \in  \textit{ReqMessage}  \tfun Product\\
 
−
  amount \in  \textit{ReqMessage}  \tfun \nat\\ ~\\
 
−
  price \in \textit{ConfMessage} \tfun \nat
 
−
\end{array}
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
Typically we would require that the message subtypes are disjoint.  In that case we would add an additional axiom:
 
−
 
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
\textbf{AXIOMS}\\
 
−
~~~~\begin{array}{l}
 
−
  \textit{ReqMessage} \cap  \textit{ConfMessage} ~=~ \emptyset \\
 
−
\end{array}
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
If we know that there are no other subtypes besides requests and confirmations and that they should be disjoint,
 
−
then we can condense the subset and disjointness axioms into a partitions axiom:
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
\textbf{AXIOMS}\\
 
−
~~~~\begin{array}{l}
 
−
  partition(~ Message, ~\textit{ReqMessage},~ \textit{ConfMessage} ~)
 
−
\end{array}
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
 
 
−
Suppose we have 2 variables representing request and confirmation channels repsectively:
 
−
 
 
−
<center>
 
−
<math>
 
−
\begin{array}{l}
 
−
\textbf{INVARIANT}~~ \\
 
−
~~~~req\_channel \subseteq \textit{ReqMessage} \\
 
−
~~~~\textit{conf\_channel} \subseteq \textit{ConfMessage}
 
−
\end{array}
 
−
</math>
 
−
</center>
 
−
 
 
−
The following ''Confirm'' event models an agent responding to request by issuing a confirmation message.
 
−
The ''Confirm'' event is enabled for the agent if there is a request message, ''req'', whose receiver is that agent.
 
−
The effect of the event is to chose a confirmation message, ''conf'', whose fields are constrained with appropriate guards and add that confirmation message to the confirmations channel:
 
−
 
 
−
<center><math>
 
−
Confirm ~=
 
−
\begin{array}[t]{l}
 
−
\textbf{ANY}~~ req,~ conf, ~ agent ~~\textbf{WHERE} \\
 
−
~~~~ req \in req\_channel  \\
 
−
~~~~ agent  = receiver(req) \\
 
−
~~~~ conf \in \textit{ConfMessage}  \\
 
−
~~~~ sender( conf ) = agent \\
 
−
~~~~ receiver( conf ) = sender(req) \\
 
−
~~~~ price(conf) = calculate\_price(~  product(req)\mapsto amount(req) ~) \\
 
−
\textbf{THEN} \\
 
−
~~~~ \textit{conf\_channel} := \textit{conf\_channel} \cup \{conf\} \\
 
−
\textbf{END}
 
−
\end{array}
 
−
</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>
 
−
 
 
−
 
 
−
 
 
−
For an example of a Rodin development that uses the projection-based approach to modelling and extending records see [http://deploy-eprints.ecs.soton.ac.uk/9/]
 
−
 
 
−
==Constructor-based Records==
 
−
 
 
−
An alternative style of modelling records is to define constructor functions that
 
−
construct a record from a tuple of the components of that record.
 
−
This is the approach that VDM follows, for example.
 
−
Suppose we wish to model the following record structure:
 
−
 
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{lcl}
 
−
\textbf{RECORD}~~~~ R &::&  e\in E\\
 
−
    &&  f \in F
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
We introduce the constructor function for ''R'' records, ''mk-R'', as follows:
 
−
 
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
\textbf{SETS}~~ R\\
 
−
\textbf{CONSTANTS}~~ \textit{mk-R},~ e,~ f\\
 
−
\textbf{AXIOMS}\\
 
−
~~~~\begin{array}{l}
 
−
  \textit{mk-R} ~\in~  (E\times F) \tbij R\\
 
−
  e \in  R \tfun E\\
 
−
  f \in  R \tfun F\\
 
−
  \forall x,y \cdot e( \textit{mk-R}(x\mapsto y) ) = x  \\
 
−
  \forall x,y \cdot  f( \textit{mk-R}(x\mapsto y) ) = y
 
−
\end{array}
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
The ''mk-R'' function is specified as a constructor for type ''R'' that takes an element of type ''E'' and an element of type ''F''
 
−
and constructs an value of type ''R''.
 
−
The constructor is specified as injective because when the components are different, then the corresponding records should be different.
 
−
The above declaration also makes the constructor surjective which means that the constructor provides a way of generating all
 
−
records of type ''R''.
 
−
 
 
−
With the constructor based approach, the ''AddElement'' event already shown above does not require a selection of a
 
−
record satisfying the required properties.  Instead we use the constructor directly:
 
−
 
 
−
<center><math>
 
−
AddElement ~=
 
−
\begin{array}[t]{l}
 
−
\textbf{BEGIN}\\
 
−
~~~~ vs := vs \cup \{~ \textit{mk-R}(e1,f1) ~\} \\
 
−
\textbf{END}
 
−
\end{array}
 
−
</math></center>
 
−
 
 
−
It is possible to define different subtypes in a similar way as in the projection-based approach by defining separate constructors for
 
−
each (disjoint) subtype.
 
−
 
 
−
Adding new fields in a refinement is more difficult with the constructor approach however.
 
−
We would need to introduce a completely new constructor for the full extended record structure and
 
−
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.
 
−
 
 
−
==Projections versus Constructors==
 
−
 
 
−
As we have seen, the constructor approach can lead to more succinct event specifications
 
−
than the projection approach.
 
−
The downside of the constructor approach is that it is difficult to extend records in refinement steps and
 
−
stepwise refinement and introduction of structure through refinement is an major feature of the
 
−
Event-B approach.
 
−
 
 
−
We could say that the projection approach gives us ''open'' record structures, that is,
 
−
structures that are easy to extend in a refinement.  The constructor approach gives us
 
−
''closed'' records that are not directly extendable in refinement steps. 
 
−
 
 
−
The constructor approach can be seen as a strengtening of the projection approach
 
−
as is now explained. Consider again the two projection  functions introduced to
 
−
represent fields of the record structure ''R'' in the projection approach:
 
−
 
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
\textbf{AXIOMS}\\
 
−
~~~~\begin{array}{l}
 
−
  e \in  R \tfun E\\
 
−
  f \in  R \tfun F
 
−
\end{array}
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
The direct product of these two projections <math>(e \otimes f)</math> has the following type:
 
−
 
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
~~~~\begin{array}{l}
 
−
  e \otimes f ~\in~ R \tfun (E\times F)
 
−
\end{array}
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
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>.
 
−
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 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
 
−
the direct product of the fields is injective:
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
\textbf{AXIOMS}~~~~~~\textit{ (Closing) }\\
 
−
~~~~\begin{array}{l}
 
−
      e \otimes f ~\in~ R \tinj (E\times F)
 
−
\end{array}
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
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
 
−
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''.
 
−
 
 
−
Regardless of whether the closing axiom is introduced, some feasibility proof obligations arising from the use of the
 
−
projection approach will require the existence of a record corresponding to any tuple of field components.  This can be
 
−
specified by the following ''feasibility'' axiom stating that the product of the projections is surjective:
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
\textbf{AXIOMS}~~~~~~\textit{ (Feasibility) }\\
 
−
~~~~\begin{array}{l}
 
−
      e \otimes f ~\in~ R \tsur (E\times F)
 
−
\end{array}
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
==Recursive Structured Types==
 
−
 
 
−
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 where proposals for inductive datatypes are made (see [[Mathematical_extensions]]).
 
−
Inductive datatypes are defined by constructor functions similar to constructor-based records.
 
−
For example, to define lists we would use two disjoint constructors, ''nil'' and ''cons''.
 
−
The ''cons'' constructor for lists typically comes with two projections, ''head'' and ''tail''.
 
−
The structural induction principle for inductive datatypes is well known.
 
−
 
 
−
With the projection approach we can define two subtypes, for empty and non-empty lists,
 
−
and extend the non-empty subtype with ''head'' and ''tail'' projections.
 
−
<center>
 
−
{{SimpleHeader}}
 
−
|<math> \begin{array}{l}
 
−
\textbf{SETS}~~ T,~ Node\\
 
−
\textbf{CONSTANTS}~~ Nil,~ Cons\\
 
−
\textbf{AXIOMS}\\
 
−
~~~~\begin{array}{l}
 
−
  partition(~ Node, ~Nil,~ Cons ~)
 
−
\end{array} \\~\\
 
−
\textbf{EXTEND~~ RECORD}~~ \textit{Cons}~~\textbf{WITH}\\
 
−
  ~~~~~~~~~~~~  head\in T \\
 
−
  ~~~~~~~~~~~~  tail\in LIST
 
−
\end{array}
 
−
</math>
 
−
|}
 
−
</center>
 
−
 
 
−
The appropriate induction principle for the projection based approach needs to be explored further.
 
−
 
 
−
==Structured Variables==
 
−
 
 
−
To be done...
 
−
 
 
−
[[Category:Work in progress]] [[Category:Design]]
 

Latest revision as of 08:56, 5 July 2008


Clicking on the my preferences link in the upper right while logged in allows you to change your preferences. You will be presented with the User profile section, as well as a bar of tabs across the top for changing other types of settings.

User profile

User profile

  • Username: Your user name. Only bureaucrats can change your username, and the wiki must also have the Renameuser extension installed.
  • User ID: A number assigned to your account when you created it (for example, if your number is 42 you are the 42nd user to sign up at this particular wiki). This number is used for internal purposes.
  • Number of edits: How many edits you have made. Not all wikis will have this.
  • Real name: If provided, this will be used for attribution (rather than using your username). Providing your real name is entirely optional. Some wikis do not have this option.
  • E-mail: Your email address, if you have supplied one. You can also change or remove your address here.
  • Nickname: When you sign your name (using ~~~~), what you enter here will be used at the start instead of a simple link to your user page. By default, anything you enter here will be wrapped with [[ ]]; if you want to use special linking, enable Raw signatures (without automatic link).
  • Language: This controls what language the interface is displayed in. MediaWiki's default interface includes localisations for all supported languages, but this is not necessarily the case with extensions or custom skins. Page text will not be translated, nor will templates (unless the templates integrate text localisation).

Change password

To change your password, enter your old password in the first box and your new password in the last two. If you want this site to remember your login, check Remember my login on this computer. Note that this function requires you to have cookies enabled in your browser, and if your cookie is cleared or expires you will no longer be remembered.

E-mail

If you have supplied an email address, you will need to click the verify address button in order to use these functions. You will receive an email; simply open it and follow the link to enable the following functions.

  • E-mail me when a page I'm watching is changed
  • E-mail me when my user talk page is changed
  • E-mail me also for minor edits of pages
  • Enable e-mail from other users
  • Send me copies of emails I send to other users

Languages

From your preferences you can select what language you would like the interface to be in. Only the buttons like 'edit' and 'talk', in addition to a few pages in the sidebar, will be affected. The main text of the pages will not be changed by this for the vast majority of pages, although there are a few pages where it will, like some in the Wikimedia Meta Wiki.

Skin

Here you can choose the skin you want to use (use Preview if you want to see a skin before you choose it). By default, MediaWiki includes the following skins:

  • Chick
  • Classic
  • Cologne Blue
  • MonoBook (default)
  • MySkin
  • Nostalgia
  • Simple

While you can choose whatever skin you like, bear in mind that some wikis will incorporate templates or layout elements that will not display as intended in some of these skins. Generally speaking, sticking with MonoBook (or whatever the wiki's default skin is) will ensure you see pages as intended.

Math

Here you can control how mathematical equations described using the <math> tag will be displayed. Mathematical formulae uploaded as images or written outside the math tag will not be affected by this setting.

  • Always render PNG
  • HTML if very simple or else PNG
  • HTML if possible or else PNG
  • Leave it as TeX (for text browsers)
  • Recommended for modern browsers
  • MathML if possible (experimental)

Files

Here you can determine how images will be displayed. Images displayed by direct pasting of a URL (if the wiki has it enabled) will not be affected by this setting.

  • Limit images on image description pages to: This setting lets you choose how big image previews will be on the Image: pages. If you know what your current screen resolution is you may like to set this to one or two sizes smaller than your own screen. If you have a slow connection (such as dial-up) you may want to limit them to 320×240.
  • Thumbnail size: Define how big you want thumbnails to appear. This setting will not affect thumbnails with dimensions determined by an editor, nor can it increase images beyond their original dimensions.

Date and time

The following is normally rendered depending on preferences: 

 [[2001-01-05]] (or [[2001]]-[[01-05]]) (with leading zeros)
 [[2001]] [[January 5]] ([[2001]] [[January 05]])
 [[January 5]], [[2001]] ([[January 05]], [[2001]])
 [[5 January]] [[2001]] ([[05 January]] [[2001]])
 [[January 5]] ([[January 05]])
 [[5 January]] ([[05 January]])

With your current preference setting on this project the seven are rendered as follows:

  1. 2001-01-05 (2001-01-05)
  2. 2001 January 5 (2001 January 05)
  3. January 5, 2001 (January 05, 2001)
  4. 5 January 2001 (05 January 2001)
  5. January 5 (January 05)
  6. 5 January (05 January)

The user-specified date format does not seem to work on the mw: wiki for links! It works in Recent Changes etc.

Editing

Settings to control editing pages, including the size of the edit box displayed and whether to watch pages that you have edited or created automatically.

Recent changes

  • Days to show in recent changes: Here you can specify how far back the recent changes pages will go. Note that the list will stop prematurely if the number of edits is exceeded (see below)
  • Number of edits to show in recent changes: Here you can specify how many edits should be displayed.
  • Hide minor edits in recent changes: This enables you to hide edits marked as minor (see Help:Editing pages). Since some users will rapidly make a lot of tiny tweaks to update templates or fix spelling errors you may find enabling this to be useful. You can also turn this on temporarily from the recent changes page (see Help:Tracking changes).
  • Enhanced recent changes (JavaScript): Enhanced recent changes condenses edits into a per-page list. As indicated, this requires JavaScript to be enabled. See Help:Tracking changes for more information on this feature.

Watchlist

Search

Default settings for searches including how many results to display and how much context to show for each result. Check the boxes next to the namespaces which you want to show up, the first time that you search for something. You can override this when doing an actual search, by checking or unchecking the boxes at the bottom of the search results screen.

Administrators: To change the namespace default preferences for new users (or users who haven't changed their preferences yet), see Manual:$wgNamespacesToBeSearchedDefault

Misc

Other settings such as numbering and justification.

See also

Retrieved from ‘https://wiki.event-b.org/index.php?title=Records_Extension&oldid=13333’