Difference between revisions of "TextEditor EBNF"

From Event-B
Jump to navigationJump to search
imported>Fabian
imported>Fabian
Line 10: Line 10:
  
 
  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 20: Line 19:
 
     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 28: Line 26:
 
     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 45: Line 42:
 
     'extends' identifier_literal ;
 
     'extends' identifier_literal ;
 
   
 
   
  labeled_action = comment? '@' identifier_literal action ;
+
  labeled_action = '@' identifier_literal action comment*;
 
   
 
   
  labeled_predicate = comment? '@' identifier_literal predicate ;
+
  labeled_predicate = '@' identifier_literal predicate comment*;
 
   
 
   
 
  labeled_predicate_with_theorem =
 
  labeled_predicate_with_theorem =
     comment? '@' identifier_literal predicate |
+
     '@' identifier_literal 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 =
 
     '//' string-to-next-linebreak |
 
     '//' string-to-next-linebreak |
 
     '/*' string '*/' ;
 
     '/*' string '*/' ;
 
  
 
===Explanation ===
 
===Explanation ===

Revision as of 13:56, 27 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.

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


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 = '@' 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

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.