Records Extension - Revision history

imported>Vitaly: /* Proving With Records */

2010-07-21T13:07:43Z

Proving With Records

← Older revision		Revision as of 13:07, 21 July 2010
Line 67:		Line 67:

	Other axioms use record and field labels in their labelling, which leads to a longer and slightly confusing but still interpretable format:		Other axioms use record and field labels in their labelling, which leads to a longer and slightly confusing but still interpretable format:
	* Feasibility axioms are in the format ''<recordName~~>.type<d~~>.feasibility'' (or ''<recordName~~>.type<d~~>.feasibility.ext<n>'' in case of record extensions)		* Feasibility axioms are in the format ''<recordName>.feasibility'' (or ''<recordName>.feasibility.ext<n>'' in case of record extensions)
	* Closure axioms are in the format ''<recordName~~>.type<d~~>.closure''		* Closure axioms are in the format ''<recordName>.closure''
	* Make function's 1st axiom (function's typing) is in the format ''<recordName~~>.type<d~~>.make.axm1''		* Make function's 1st axiom (function's typing) is in the format ''<recordName>.make.axm1''
	* Make function's 2nd axiom (for each field) is in the format ''<recordName>.<fieldName~~>.type<d~~>.make.axm2''		* Make function's 2nd axiom (for each field) is in the format ''<recordName>.<fieldName>.make.axm2''
	* Update function's 1st axiom (record field update function's typing) is in the format ''<recordName>.<fieldName~~>.type<d~~>.update.axm1''		* Update function's 1st axiom (record field update function's typing) is in the format ''<recordName>.<fieldName>.update.axm1''
	* Update function's 2nd axiom (equivalence to record construction with a specific value of updated field) is in the format ''<recordName>.<fieldName~~>.type<d~~>.update.axm2''		* Update function's 2nd axiom (equivalence to record construction with a specific value of updated field) is in the format ''<recordName>.<fieldName>.update.axm2''

	==Current Limitations==		==Current Limitations==

imported>Vitaly: /* Proving With Records */

2010-07-20T13:20:38Z

Proving With Records

← Older revision		Revision as of 13:20, 20 July 2010
Line 67:		Line 67:

	Other axioms use record and field labels in their labelling, which leads to a longer and slightly confusing but still interpretable format:		Other axioms use record and field labels in their labelling, which leads to a longer and slightly confusing but still interpretable format:
	* Feasibility axioms are in the format ''<recordName>.type<d>.feasibility''		* Feasibility axioms are in the format ''<recordName>.type<d>.feasibility'' (or ''<recordName>.type<d>.feasibility.ext<n>'' in case of record extensions)
	* Closure axioms are in the format ''<recordName>.type<d>.closure''		* Closure axioms are in the format ''<recordName>.type<d>.closure''
	* Make function's 1st axiom (function's typing) is in the format ''<recordName>.type<d>.make.axm1''		* Make function's 1st axiom (function's typing) is in the format ''<recordName>.type<d>.make.axm1''

imported>Vitaly at 10:35, 19 July 2010

2010-07-19T10:35:22Z

← Older revision		Revision as of 10:35, 19 July 2010
Line 10:		Line 10:
	The '''Event-B editor''' is extended to include two new top level clauses. These are '''Record Declarations''' and '''Record Extensions'''.		The '''Event-B editor''' is extended to include two new top level clauses. These are '''Record Declarations''' and '''Record Extensions'''.

	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.		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 or carrier set.

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

			Record Declaration clause also contains a toggle button to control the record's closure property. A closed record cannot be subtyped by other records or extended by record extensions.

	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.		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.
Line 41:		Line 43:
	==Usage==		==Usage==

	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).		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. <s>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.</s> To be correctly static-checked record definitions must be in order of their referencing i.e. a subtype record would follow a supertype record which it references (to know about its type). In opposite case static checker will show a typing problem.

			Add fields and give them a type by entering an expression that evaluates to a set. Note that this expression must be a basic type expression. You can use records, constants and sets in the expression.

			After a record is defined it can be declared as closed using a toggle button in its Record Declaration clause. When record is closed it cannot be subtyped or extended anymore. Another effect of closing a record is that additional axioms are generated for it in the checked context. These include a closure axiom, a make-function for the record and an update-function for each of its fields (also for derived fields from supertype records). Another axiom — feasibility axiom — is generated for every record independent of its closure attribute.

	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.		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. Only open (not closed) records can be extended, although the drop down list contains all the declared records.

	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.		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.
Line 57:		Line 63:

	The automatically generated labels use an easy to interpret format:		The automatically generated labels use an easy to interpret format:
	* Subtype Record typing axioms are in the format <recordName>.type<d> (where d is a decimal digit appended to ensure there are no name clashes)		* Subtype Record typing axioms are in the format ''<recordName>.type<d>'' (where d is a decimal digit appended to ensure there are no name clashes)
	* Field typing axioms are in the format <recordName>.<fieldName>.type<d> (where d is a decimal digit appended to ensure there are no name clashes)		* Field typing axioms are in the format ''<recordName>.<fieldName>.type<d>'' (where d is a decimal digit appended to ensure there are no name clashes)

			Other axioms use record and field labels in their labelling, which leads to a longer and slightly confusing but still interpretable format:
			* Feasibility axioms are in the format ''<recordName>.type<d>.feasibility''
			* Closure axioms are in the format ''<recordName>.type<d>.closure''
			* Make function's 1st axiom (function's typing) is in the format ''<recordName>.type<d>.make.axm1''
			* Make function's 2nd axiom (for each field) is in the format ''<recordName>.<fieldName>.type<d>.make.axm2''
			* Update function's 1st axiom (record field update function's typing) is in the format ''<recordName>.<fieldName>.type<d>.update.axm1''
			* Update function's 2nd axiom (equivalence to record construction with a specific value of updated field) is in the format ''<recordName>.<fieldName>.type<d>.update.axm2''

	==Current Limitations==		==Current Limitations==
	* Records are not supported by the Camille text editor (see warning below)		* Records are not supported by the Camille text editor (see warning below)
	* Records are not supported by the Pretty print facility		* <s>Records are not supported by the Pretty print facility</s>
	* Records are not supported by the Synthesis view facility		* <s>Records are not supported by the Synthesis view facility</s>
	* Records are not supported by the EventB2Latex plug-in		* Records are not supported by the EventB2Latex plug-in
	* Records are not supported by the Refactoring plug-in		* <s>Records are not supported by the Refactoring plug-in</s>
	* Records are partially supported by the Decomposition plug-in (Machines that use records can be decomposed, but the Context that contains the record cannot).		* Records are partially supported by the Decomposition plug-in (Machines that use records can be decomposed, but the Context that contains the record cannot).
	* Records may have, at most, one supertype.		* Records may have, at most, one supertype.
	* Records may only have records as supertypes (not carrier sets)		* <s>Records may only have records as supertypes (not carrier sets)</s>
	* There is no finalisation of a record - hence make functions are not supported		* <s>There is no finalisation of a record - hence make functions are not supported</s>

	==Warning==		==Warning==

imported>Colin: /* Usage */

2010-04-28T13:28:22Z

Usage

← Older revision		Revision as of 13:28, 28 April 2010
Line 48:		Line 48:

	You use fields as if they were functions (which is what they are in the checked context).		You use fields as if they were functions (which is what they are in the checked context).
	e,g if ~~r1,~~ belongs to myRecord which has a field myField ~~: NAT~~ then I could write in a predicate~~...~~ myField(r1) > 5
			e.g. if <math>r</math> belongs to <math>myRecord</math> which has a field, <math>myField \in \nat</math> then I could write in a predicate <math> myField(r) > 5 </math>.

	==Proving With Records==		==Proving With Records==

imported>Colin: /* Semantics of Records */

2010-04-28T13:19:57Z

Semantics of Records

← Older revision		Revision as of 13:19, 28 April 2010
Line 24:		Line 24:
	==Semantics of Records==		==Semantics of Records==
	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.		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.


	<center>		<center>
Line 33:		Line 34:
	\|<math> \textbf{ FIELD}~~~~ f \in F</math> \|\| <math> \textbf{~~CONSTANT}~~~~ f , ~~~~\textbf{AXIOM}~~~~ f \in R \rightarrow F ~~~~</math>		\|<math> \textbf{ FIELD}~~~~ f \in F</math> \|\| <math> \textbf{~~CONSTANT}~~~~ f , ~~~~\textbf{AXIOM}~~~~ f \in R \rightarrow F ~~~~</math>
	\|}		\|}
	<center>		</center>


	[It may be instructive to open the *.bcc file with a text editor to examine the generated carrier sets, constants, and axioms]		[It may be instructive to open the *.bcc file with a text editor to examine the generated carrier sets, constants, and axioms]

imported>Colin: /* Semantics of Records */

2010-04-28T13:19:17Z

Semantics of Records

← Older revision		Revision as of 13:19, 28 April 2010
Line 25:		Line 25:
	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.		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.

	<~~centre~~>		<center>
	{\| align="centre" border = "1" cellpadding = "10" cellspacing="5"		{\| align="centre" border = "1" cellpadding = "10" cellspacing="5"
	\|<math> \textbf{ RECORD}~~~~ R </math> \|\| <math> \textbf{~~SET}~~~~ R </math>		\|<math> \textbf{ RECORD}~~~~ R </math> \|\| <math> \textbf{~~SET}~~~~ R </math>
Line 33:		Line 33:
	\|<math> \textbf{ FIELD}~~~~ f \in F</math> \|\| <math> \textbf{~~CONSTANT}~~~~ f , ~~~~\textbf{AXIOM}~~~~ f \in R \rightarrow F ~~~~</math>		\|<math> \textbf{ FIELD}~~~~ f \in F</math> \|\| <math> \textbf{~~CONSTANT}~~~~ f , ~~~~\textbf{AXIOM}~~~~ f \in R \rightarrow F ~~~~</math>
	\|}		\|}
	<~~centre~~>		<center>

	[It may be instructive to open the *.bcc file with a text editor to examine the generated carrier sets, constants, and axioms]		[It may be instructive to open the *.bcc file with a text editor to examine the generated carrier sets, constants, and axioms]

imported>Colin: /* Semantics of Records */

2010-04-28T13:17:13Z

Semantics of Records

← Older revision		Revision as of 13:17, 28 April 2010
Line 25:		Line 25:
	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.		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.

	<~~formatting/presentation of this will be improved~~>		<centre>
			{\| align="centre" border = "1" cellpadding = "10" cellspacing="5"
	~~Record~~ R ~~Supertypes~~ <~~null~~> --> ~~Carrier Set~~ R		\|<math> \textbf{ RECORD}~~~~ R </math> \|\| <math> \textbf{~~SET}~~~~ R </math>
			\|-
	~~Record~~ S ~~Supertypes R --~~> ~~Constant S~~, ~~Axiom~~ S ~~: POW(R~~)		\|<math> \textbf{ RECORD}~~~~ R, ~~~~\textbf{SUPERTYPE}~~~~ S ~~~~</math> \|\| <math> \textbf{~~CONSTANT}~~~~ R , ~~~~\textbf{AXIOM}~~~~ R \in \pow (S) ~~~~</math>
			\|-
	~~Field~~ f : F --> ~~Constant~~ f, ~~Axiom~~ f : R --> F		\|<math> \textbf{ FIELD}~~~~ f \in F</math> \|\| <math> \textbf{~~CONSTANT}~~~~ f , ~~~~\textbf{AXIOM}~~~~ f \in R \rightarrow F ~~~~</math>
			\|}
			<centre>

	[It may be instructive to open the *.bcc file with a text editor to examine the generated carrier sets, constants, and axioms]		[It may be instructive to open the *.bcc file with a text editor to examine the generated carrier sets, constants, and axioms]


	==Usage==		==Usage==

imported>Colin: /* Current Limitations */

2010-03-18T13:15:17Z

Current Limitations

← Older revision		Revision as of 13:15, 18 March 2010
Line 61:		Line 61:
	* Records are not supported by the Synthesis view facility		* Records are not supported by the Synthesis view facility
	* Records are not supported by the EventB2Latex plug-in		* Records are not supported by the EventB2Latex plug-in
	* Records are not supported by the Decomposition plug-in (Machines that use records can ~~not~~ be decomposed).		* Records are not supported by the Refactoring plug-in
			* Records are partially supported by the Decomposition plug-in (Machines that use records can be decomposed, but the Context that contains the record cannot).
	* Records may have, at most, one supertype.		* Records may have, at most, one supertype.
	* Records may only have records as supertypes (not carrier sets)		* Records may only have records as supertypes (not carrier sets)

imported>Colin: /* Current Limitations */

2010-02-22T15:15:49Z

Current Limitations

← Older revision		Revision as of 15:15, 22 February 2010
Line 64:		Line 64:
	* Records may have, at most, one supertype.		* Records may have, at most, one supertype.
	* Records may only have records as supertypes (not carrier sets)		* Records may only have records as supertypes (not carrier sets)
	* There is finalisation of a record - hence make functions are not supported		* There is no finalisation of a record - hence make functions are not supported

	==Warning==		==Warning==

imported>Colin: /* Usage */

2010-02-19T19:03:51Z

Usage

← Older revision		Revision as of 19:03, 19 February 2010
Line 46:		Line 46:
	You use fields as if they were functions (which is what they are in the checked context).		You use fields as if they were functions (which is what they are in the checked context).
	e,g if r1, belongs to myRecord which has a field myField : NAT then I could write in a predicate... myField(r1) > 5		e,g if r1, belongs to myRecord which has a field myField : NAT then I could write in a predicate... myField(r1) > 5

			==Proving With Records==
			The prover will refer to records as sets and constants, and to fields as constants. Therefore for proving you may need to be aware of this.

			Axioms that are automatically generated for typing records and their fields will have automatically generated labels and these may be referenced in the prover interface.

			The automatically generated labels use an easy to interpret format:
			* Subtype Record typing axioms are in the format <recordName>.type<d> (where d is a decimal digit appended to ensure there are no name clashes)
			* Field typing axioms are in the format <recordName>.<fieldName>.type<d> (where d is a decimal digit appended to ensure there are no name clashes)

	==Current Limitations==		==Current Limitations==