Difference between revisions of "TextEditor EBNF"

From Event-B
Jump to navigationJump to search
imported>Fabian
imported>Mathieu
 
(14 intermediate revisions by 2 users not shown)
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.
 +
 
 +
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 ===
  
 
  parse_unit =
 
  parse_unit =
    comment?
+
     'machine' identifier_literal comment*
     'machine' identifier_literal
 
 
     ('refines' identifier_literal (',' identifier_literal)*)?
 
     ('refines' identifier_literal (',' identifier_literal)*)?
 
     ('sees' identifier_literal (',' identifier_literal)*)?
 
     ('sees' identifier_literal (',' identifier_literal)*)?
Line 17: Line 22:
 
     end |
 
     end |
 
      
 
      
    comment?
+
     'context' identifier_literal comment*
     'context' identifier_literal
 
 
     ('extends' identifier_literal (',' identifier_literal)*)?
 
     ('extends' identifier_literal (',' identifier_literal)*)?
 
     ('sets' identifier_list)?
 
     ('sets' identifier_list)?
Line 25: Line 29:
 
     end ;
 
     end ;
 
   
 
   
  variant = comment? expression ;
+
  variant = expression comment*;
 
   
 
   
 
  event =
 
  event =
    comment?
+
     convergence? 'event' identifier_literal comment*
     convergence? 'event' identifier_literal
 
 
     event_refinement?
 
     event_refinement?
 
     ('any' identifier_list)?
 
     ('any' identifier_list)?
Line 42: Line 45:
 
     'extends' identifier_literal ;
 
     'extends' identifier_literal ;
 
   
 
   
  labeled_action = comment? '@' identifier_literal action ;
+
  labeled_action = '@' label action comment*;
 
   
 
   
  labeled_predicate = comment? '@' identifier_literal predicate ;
+
  labeled_predicate = '@' label predicate comment*;
 
   
 
   
 
  labeled_predicate_with_theorem =
 
  labeled_predicate_with_theorem =
     comment? '@' identifier_literal predicate |
+
     '@' label predicate comment*|
     comment? 'theorem' '@' identifier_literal predicate ;
+
     'theorem' '@' identifier_literal predicate comment*;
 
   
 
   
  identifier = comment? identifier_literal ;
+
  identifier = identifier_literal comment*;
 
   
 
   
  identifier_list = identifier (',' identifier)* ;
+
  identifier_list = identifier identifier* ;
 
   
 
   
 
  comment =
 
  comment =
Line 58: Line 61:
 
     '/*' 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 ===
Line 64: Line 69:
  
 
====Comments ====
 
====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.
+
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 so the grammar reflects this by only allowing one comment in front of elements.
+
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 ===
 +
''Feel free to add own examples!''
 +
 
 +
=====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].
 +
 
 +
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
 +
 
 +
=====Context 'array' from example 'maximum' =====
 +
 
 +
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
 +
 +
constants n a
 +
 +
axioms
 +
  @axm1 n ∈ ℕ1
 +
  @axm2 a ∈ 1‥n → ℤ
 +
end
 +
 
 +
[[Category:Text editor]]
 +
[[Category:User documentation]]

Latest revision as of 12:43, 12 August 2009

This page describes the text syntax for Event-B models in the TextEditor. It shows its EBNF, explains some details and design decisions and gives some 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 screenshot page.


EBNF for the TextEditor's syntax

parse_unit =
   '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 = '@' label action comment*;

labeled_predicate = '@' label predicate comment*;

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

identifier = identifier_literal comment*;

identifier_list = identifier identifier* ;

comment =
   '//' string-to-next-linebreak |
   '/*' string '*/' ;


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

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

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

Feel free to add own examples!

Machine 'm0' from example 'maximum'

See the screenshot of this example or download the project.

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
Context 'array' from example 'maximum'

See the screenshot of this example or download the project.

context array

constants n a 

axioms
  @axm1 n ∈ ℕ1
  @axm2 a ∈ 1‥n → ℤ
end