TextEditor EBNF: Difference between revisions
imported>Fabian |
imported>Fabian No edit summary |
||
Line 1: | Line 1: | ||
{| align="right" | |||
| __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. | |||
===EBNF for the TextEditor's syntax === | ===EBNF for the TextEditor's syntax === | ||
Line 52: | Line 57: | ||
'//' string-to-next-linebreak | | '//' string-to-next-linebreak | | ||
'/*' string '*/' ; | '/*' string '*/' ; | ||
===Explanation === | |||
====Formulas ==== | |||
As you might notice the grammar only describes the structure of machines and contexts. For the terminals ''predicate'', ''expression'' and ''action'' you can use the syntax for formulas which you already know from editing models with the graphical Event-B editor. You can use the ASCII representation of mathematical symbols or their unicode. See the Rodin help for details about the mathematical symbols and their ASCII counterparts. | |||
====Comments ==== | |||
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 following element. | |||
Additionally database only allows one comment per element so the grammar reflects this by only allowing one comment in front of elements. |
Revision as of 14:42, 13 May 2009
This page describes the text syntax for Event-B models in the TextEditor. It shows an EBNF and explains some details and design decisions.
EBNF for the TextEditor's syntax
parse_unit = comment? 'machine' identifier_literal ('refines' identifier_literal (',' identifier_literal)*)? ('sees' identifier_literal (',' identifier_literal)*)? ('variables' identifier_list)? ('invariants' labeled_predicate_with_theorem+)? ('variant' variant)? ('events' event+)? end | comment? 'context' identifier_literal ('extends' identifier_literal (',' identifier_literal)*)? ('sets' identifier_list)? ('constants' identifier_list)? ('axioms' labeled_predicate_with_theorem+)? end ; variant = comment? expression ; event = comment? convergence? 'event' identifier_literal event_refinement? ('any' identifier_list)? ('where' labeled_predicate+)? ('with' labeled_predicate+)? ('then' labeled_action+)? ; convergence = 'ordinary' | 'convergent' | 'anticipated' ; event_refinement = 'refines' identifier_literal (',' identifier_literal)* | 'extends' identifier_literal ; labeled_action = comment? '@' identifier_literal action ; labeled_predicate = comment? '@' identifier_literal predicate ; labeled_predicate_with_theorem = comment? '@' identifier_literal predicate | comment? 'theorem' '@' identifier_literal predicate ; identifier = comment? identifier_literal ; identifier_list = identifier (',' identifier)* ; comment = '//' string-to-next-linebreak | '/*' string '*/' ;
Explanation
Formulas
As you might notice the grammar only describes the structure of machines and contexts. For the terminals predicate, expression and action you can use the syntax for formulas which you already know from editing models with the graphical Event-B editor. You can use the ASCII representation of mathematical symbols or their unicode. See the Rodin help for details about the mathematical symbols and their ASCII counterparts.
Comments
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 following element. Additionally database only allows one comment per element so the grammar reflects this by only allowing one comment in front of elements.