imported>Fabian |
imported>Fabian |
| 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]].
| |
| | | | |
| − | 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]].
| + | Some impression of the TextEditor... |
| | | | |
| − | ===EBNF for the TextEditor's syntax === | + | ====Machine 'm0' from example 'maximum' ==== |
| | | | |
| − | parse_unit =
| + | See [[TextEditor_EBNF#Examples|TextEditor EBNF - Examples]] for the code or download the [http://deploy-eprints.ecs.soton.ac.uk/56/4/maximum.zip project]. |
| − | 'machine' identifier_literal comment*
| |
| − | ('refines' identifier_literal (',' identifier_literal)*)?
| |
| − | ('sees' identifier_literal (',' identifier_literal)*)?
| |
| − | ('variables' identifier_list)?
| |
| − | ('invariants' labeled_predicate_with_theorem+)?
| |
| − | ('variant' variant)?
| |
| − | ('events' event+)?
| |
| − | end |
| |
| − |
| |
| − | 'context' identifier_literal comment*
| |
| − | ('extends' identifier_literal (',' identifier_literal)*)?
| |
| − | ('sets' identifier_list)?
| |
| − | ('constants' identifier_list)?
| |
| − | ('axioms' labeled_predicate_with_theorem+)?
| |
| − | end ;
| |
| − |
| |
| − | variant = expression comment*;
| |
| − |
| |
| − | event =
| |
| − | convergence? 'event' identifier_literal comment*
| |
| − | 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 = '@' identifier_literal action comment*;
| |
| − |
| |
| − | labeled_predicate = '@' identifier_literal predicate comment*;
| |
| − |
| |
| − | labeled_predicate_with_theorem =
| |
| − | '@' identifier_literal predicate comment*|
| |
| − | 'theorem' '@' identifier_literal predicate comment*;
| |
| − |
| |
| − | identifier = identifier_literal comment*;
| |
| − |
| |
| − | identifier_list = identifier identifier* ;
| |
| − |
| |
| − | comment =
| |
| − | '//' string-to-next-linebreak |
| |
| − | '/*' string '*/' ;
| |
| | | | |
| | | | |
| − | ===Explanation ===
| + | [[Image:Screen_max_m0.png]] |
| − | ====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 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.
| |
| | | | |
| | + | ====Context 'array' from example 'maximum' ==== |
| | | | |
| − | ===Examples ===
| + | See [[TextEditor_EBNF#Examples|TextEditor EBNF - Examples]] for the code or download the [http://deploy-eprints.ecs.soton.ac.uk/56/4/maximum.zip project]. |
| − | ''Feel free to add own examples!''
| |
| | | | |
| | | | |
| − | =====Machine 'm0' from example 'maximum' =====
| + | [[Image:Screen_max_array.png]] |
| | | | |
| − | 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].
| |
| | | | |
| − | machine m0 sees array
| + | ====Code completion for an event template ==== |
| − |
| |
| − | 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
| |
| | | | |
| − | =====Context 'array' from example 'maximum' =====
| + | [[Image:Screen_max_completion_event.png]] |
| | | | |
| − | See the [[TextEditor_Screenshots#Context_.27array.27_from_example_.27maximum.27|screenshot]] of this example or download the [http://deploy-eprints.ecs.soton.ac.uk/56/4/maximum.zip project].
| |
| | | | |
| − | context array
| + | ====Code completion for a constant name ==== |
| − |
| + | The screenshot shows how the code completion provides easy access to identifiers such as constants. In this case the two variables of the machine and the two constants from the seen context ''array'' are offered to be inserted. |
| − | constants n a
| + | |
| − |
| + | [[Image:Screen_max_completion_constant.png]] |
| − | axioms
| |
| − | @axm1 n ∈ ℕ1
| |
| − | @axm2 a ∈ 1‥n → ℤ
| |
| − | end
| |
