TextEditor EBNF: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Fabian No edit summary |
imported>Fabian |
||
Line 48: | Line 48: | ||
identifier_list = identifier (',' identifier)* ; | identifier_list = identifier (',' identifier)* ; | ||
comment = | |||
'//' string-to-next-linebreak | | |||
'/*' string '*/' ; |
Revision as of 14:33, 13 May 2009
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 '*/' ;