Difference between revisions of "TextEditor EBNF"
From Event-B
Jump to navigationJump to searchimported>Fabian (New page: ''Coming soon'') |
imported>Fabian |
||
Line 1: | Line 1: | ||
− | '' | + | ===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)* ; |
Revision as of 14:31, 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)* ;