TextEditor EBNF - Revision history

imported>Mathieu: Category:Text editor Category:User documentation

2009-08-12T12:43:31Z

Category:Text editor Category:User documentation

← Older revision		Revision as of 12:43, 12 August 2009
Line 118:		Line 118:
	@axm2 a ∈ 1‥n → ℤ		@axm2 a ∈ 1‥n → ℤ
	end		end

			[[Category:Text editor]]
			[[Category:User documentation]]

imported>PMatos: Note on incorrect EBNF with regards to implementation?

2009-07-07T13:42:29Z

Note on incorrect EBNF with regards to implementation?

← Older revision		Revision as of 13:42, 7 July 2009
Line 60:		Line 60:
	'//' string-to-next-linebreak \|		'//' string-to-next-linebreak \|
	'/' string '/' ;		'/' string '/' ;


			'''NOTE: the EBNF above for Contexts specifies that constants come after sets. It seems to be the other way around in RODIN.'''

	===Explanation ===		===Explanation ===

imported>Fabian: /* EBNF for the TextEditor's syntax */

2009-06-14T13:07:19Z

EBNF for the TextEditor's syntax

← Older revision		Revision as of 13:07, 14 June 2009
Line 45:		Line 45:
	'extends' identifier_literal ;		'extends' identifier_literal ;

	labeled_action = '@' ~~identifier_literal~~ action comment*;		labeled_action = '@' label action comment*;

	labeled_predicate = '@' ~~identifier_literal~~ predicate comment*;		labeled_predicate = '@' label predicate comment*;

	labeled_predicate_with_theorem =		labeled_predicate_with_theorem =
	'@' ~~identifier_literal~~ predicate comment*\|		'@' label predicate comment*\|
	'theorem' '@' identifier_literal predicate comment*;		'theorem' '@' identifier_literal predicate comment*;

Line 60:		Line 60:
	'//' string-to-next-linebreak \|		'//' string-to-next-linebreak \|
	'/' string '/' ;		'/' string '/' ;


	===Explanation ===		===Explanation ===

imported>Fabian at 12:48, 14 June 2009

2009-06-14T12:48:48Z

← Older revision		Revision as of 12:48, 14 June 2009
Line 69:		Line 69:
	Also note that the rather strict position for comments is necessary. In the RodinDB most elements can be commented. That means if you comment an element this comment is attached to the element. To reflect this in a text syntax we need to exactly specify to which textual element a comment belongs. Therefore we decided to always associate a comment to the previous element.		Also note that the rather strict position for comments is necessary. In the RodinDB most elements can be commented. That means if you comment an element this comment is attached to the element. To reflect this in a text syntax we need to exactly specify to which textual element a comment belongs. Therefore we decided to always associate a comment to the previous element.
	Additionally database only allows one comment per element. The grammar allows multiple comments, but to reflect the database restriction to one internally multiple comments are concatenated to one with linebreaks between the separate comments.		Additionally database only allows one comment per element. The grammar allows multiple comments, but to reflect the database restriction to one internally multiple comments are concatenated to one with linebreaks between the separate comments.

			====Labels ====
			The syntax doesn't allow whitespaces within labels. It assumes that all characters following an '@' belong to the label until the next whitespace character is found.


	===Examples ===		===Examples ===
	''Feel free to add own examples!''		''Feel free to add own examples!''


	=====Machine 'm0' from example 'maximum' =====		=====Machine 'm0' from example 'maximum' =====

imported>Fabian at 09:31, 31 May 2009

2009-05-31T09:31:32Z

← Older revision		Revision as of 09:31, 31 May 2009
Line 7:		Line 7:

	Screenshots which give an impression of the syntax in the text editor are shown on the [[TextEditor_Screenshots\| screenshot page]].		Screenshots which give an impression of the syntax in the text editor are shown on the [[TextEditor_Screenshots\| screenshot page]].



	===EBNF for the TextEditor's syntax ===		===EBNF for the TextEditor's syntax ===

imported>Fabian at 09:31, 31 May 2009

2009-05-31T09:31:05Z

← Older revision		Revision as of 09:31, 31 May 2009
Line 2:		Line 2:
	\| __TOC__		\| __TOC__
	\|}		\|}
	This page describes the text syntax for Event-B models in the TextEditor. It shows its EBNF, [[Explanation\|explains]] some details and design decisions and gives some [[#Examples\|examples]].		This page describes the text syntax for Event-B models in the TextEditor. It shows its EBNF, [[#Explanation\|explains]] some details and design decisions and gives some [[#Examples\|examples]].

	See the [[Text_Editor]] page for details of the editor and the usage of the text syntax.		See the [[Text_Editor]] page for details of the editor and the usage of the text syntax.

imported>Fabian at 09:30, 31 May 2009

2009-05-31T09:30:43Z

← Older revision		Revision as of 09:30, 31 May 2009
Line 2:		Line 2:
	\| __TOC__		\| __TOC__
	\|}		\|}
	This page describes the text syntax for Event-B models in the TextEditor. It shows an EBNF ~~and~~ explains some details and design decisions.		This page describes the text syntax for Event-B models in the TextEditor. It shows its EBNF, [[Explanation\|explains]] some details and design decisions and gives some [[#Examples\|examples]].

	See the [[Text_Editor]] page for details of the editor and the usage of the text syntax.		See the [[Text_Editor]] page for details of the editor and the usage of the text syntax.

			Screenshots which give an impression of the syntax in the text editor are shown on the [[TextEditor_Screenshots\| screenshot page]].

	===EBNF for the TextEditor's syntax ===		===EBNF for the TextEditor's syntax ===

imported>Fabian: /* Machine 'm0' from example project 'maximum' */

2009-05-31T09:27:18Z

Machine 'm0' from example project 'maximum'

← Older revision		Revision as of 09:27, 31 May 2009
Line 72:		Line 72:


	=====Machine 'm0' from example ~~project~~ 'maximum' =====		=====Machine 'm0' from example 'maximum' =====

	See the [[TextEditor_Screenshots#Machine_.27m0.27_from_example_.27maximum.27\|screenshot]] of this example or download the [http://deploy-eprints.ecs.soton.ac.uk/56/4/maximum.zip project].		See the [[TextEditor_Screenshots#Machine_.27m0.27_from_example_.27maximum.27\|screenshot]] of this example or download the [http://deploy-eprints.ecs.soton.ac.uk/56/4/maximum.zip project].
Line 98:		Line 98:
	end		end
	end		end


	=====Context 'array' from example 'maximum' =====		=====Context 'array' from example 'maximum' =====

imported>Fabian: /* Examples */

2009-05-31T09:19:50Z

Examples

@@ Line 97: / Line 97: @@
         @act1 i ≔ j
     end
   end

imported>Fabian at 09:18, 31 May 2009

2009-05-31T09:18:05Z

← Older revision		Revision as of 09:18, 31 May 2009
Line 72:		Line 72:


	Machine '''m0''' from example project '''maximum'''		=====Machine 'm0' from example project 'maximum' =====

			See the [[TextEditor_Screenshots#Machine_.27m0.27_from_example_.27maximum.27\|screenshot]] of this example or download the [http://deploy-eprints.ecs.soton.ac.uk/56/4/maximum.zip project].

	~~Also see the [[TextEditor_Screenshots#Machine_.27m0.27_from_example_.27maximum.27\|screenshot]] of this example.~~		machine m0 sees array

			variables i

			invariants
			@inv1 i ∈ ℕ

			events
			event INITIALISATION
			then
			@act1 i :∈ ℕ
			end

			event find_max
			any j
			where
			@grd1 j ∈ 1‥n
			@grd2 ∀k·k∈1‥n ⇒ a(k) ≤ a(j)
			then
			@act1 i ≔ j
			end
			end