Differences

This shows you the differences between two versions of the page.

Link to this comparison view

vv-lab:formalspec.g [2015/02/18 22:13] (current)
egm created
Line 1: Line 1:
 +[[Formal Specification Language|Back]]
  
 +<​code>​
 +/**
 + ​* Formal Specification Language grammar ​
 + ​* @author Everett Morse
 + * (c) 2009 - 2010 Brigham Young University
 + */
 +grammar FormalSpec;
 +
 +options {
 + language = Java;
 + output = AST;
 +
 + //k = 2;
 + backtrack = true;  //using this we get rid of warnings about infix portion of grammar
 + memoize = true;​  ​  //​remembers what's already been tried when backtracking
 + //​caseSensitive = false;
 +}
 +
 +tokens {
 + //Used to build trees (where another token would be ambiguous)
 + PROC;​ //​Procedure call (to differentiate from func call)
 + FUNC;​ //​Function call (to diff from proc call)
 + UMINUS;​ //​Unary minus (diff from subtraction)
 + VAR;​ //​Variable declaration (in the state)
 + SET_BUILDER;//​to differentiate between {(x : x=1)} and {x : x=1} in the AST.
 + SLIST;​ //​Statement list, for a list of compound commands
 + PLIST;​ //​parameter list for Function/​Procedure definition.
 + KLIST;​ //​list of continuation conditions.
 + KGUARD;​ //​for when just a continuation guard is given, and the rest of the current SLIST 
 +             //  should be used as the effect inside the continuation.
 +
 + //Not used in full syntax, but used in desugaring
 + DESET;
 +
 + //Not used in full syntax, but used for the kernel language
 + RET;
 +
 + //ANLTR gets errors when trying to use tokens with backslashes in derived tree grammars
 + SETMINUS;
 + UNION;
 + INTERSECT;
 + FORALL;
 + EXISTS;
 + IN;
 + NOTIN;
 + AND;
 + OR;
 +}
 +
 +@header {
 +package fspecc.generated;​
 +
 +}
 +
 +@lexer::​header {
 +package fspecc.generated;​
 +}
 +
 +
 +/*----- EBNF: Formal Specification Language -------*/
 +
 +program ​
 + : (transition | daemon | function | procedure | state)* ​
 + ;
 +
 +state 
 + : '​state'​^ state_variable_decl* '​end'​!
 + ;
 +state_variable_decl ​
 + : id ('​='​ expression)?​ -> ^(VAR id expression?​) ​
 + ;
 +
 +transition ​
 + : '​transition'​^ id (input_list)?​ let_decl* success_rule error_rules?​ '​end'​!
 + ;
 +daemon
 + : '​daemon'​^ id let_decl* success_rule error_rules?​ '​end'​!
 + ;
 +input_list ​
 + : '​input'​^ id_list ​
 + ;
 +success_rule ​
 + : '​rule'​^ rule+ '​end'​!
 + ;
 +error_rules ​
 + : '​errors'​^ rule+ '​end'​!
 + ;
 +rule 
 + : condition '​==>'​^ compound_command
 + ;
 +condition ​
 + : expression
 + ;
 +let_decl
 + : '​let'​^ id '​='​! expression
 + ;
 +
 +procedure ​
 + : '​procedure'​^ id '​('​! foraml_param_list?​ '​)'​! compound_command '​end'​!
 + ;
 +function ​
 + : '​function'​^ id '​('​! foraml_param_list?​ '​)'​! expression '​end'​!
 + ;
 +
 +foraml_param_list
 + : id_list -> ^(PLIST id_list)
 + ;
 +
 +id_list ​
 + : id (','​! id)*
 + ;
 +compound_command ​
 + : command (command)* -> ^(SLIST command+)
 + ;
 +command
 + :​ procedure_call ';'​!
 + | assignment ';'​!
 + | '​tmp'​^ id ';'​!
 + | '​call'​^ id '​('​! param_list? '​)'​! continuation_condition ';'​!
 + | '​let'​^ id '​='​! expression ';'​!
 + | '​choose'​^ id '​in'​! expression ';'​!
 + ;
 +
 +procedure_call ​
 + : id '​('​ param_list? '​)'​ -> ^(PROC id param_list?​) ​
 + ;
 +function_call ​
 + : id '​('​ param_list? '​)'​ ->  ^(FUNC id param_list?​)
 + ;
 +param_list ​
 + : expression (','​! expression)* ​
 + ;
 +
 +assignment ​
 + : ('​@'​)?​ id '​\''​! ':​='​^ expression ​
 + ;
 +
 +continuation_condition
 + : '​['​ expression '​]'​ -> ^(KGUARD expression) //single condition before continuing
 + | '​{'​ rule+ '​}'​ -> ^(KLIST rule+) //multiple paths
 + | /*empty*/ -> ^(KGUARD BOOLEAN["​true"​]) //no guard given, so always true
 + ;
 +
 +
 +expression
 + : or_expr
 + | '​truncate'​^ '​('​! expression ','​! expression '​)'​!
 + ;
 +
 +or_expr
 + : and_expr (orop^ or_expr)*
 + ;
 +orop
 + : '​\\/'​ -> OR
 + ;
 +
 +and_expr
 + :​ inc_excl_expr (andop^ and_expr)*
 + ;
 +andop
 + : '/​\\'​ -> AND
 + ;
 +
 +inc_excl_expr
 + :​ diff_expr (inc_excl_op^ inc_excl_expr)*
 + ;
 +
 +inc_excl_op
 + :​ '​\\in'​ -> IN
 + | '​\\notin'​ -> NOTIN
 + ;
 +
 +diff_expr
 + :​ intersect_expr (setminusop^ diff_expr)*
 + ;
 +setminusop
 + : '​\\'​ -> SETMINUS
 + ;
 +
 +intersect_expr
 + :​ union_expr (intop^ intersect_expr)*
 + ;
 +intop
 + : '​\\int'​ -> INTERSECT
 + ;
 +
 +union_expr
 + :​ quantification_expr (unionop^ union_expr)*
 + ;
 +unionop
 + : '​\\U'​ -> UNION
 + ;
 +
 +quantification_expr
 + :​ compare_expr
 + | quantop^ such_that_expr
 + ;
 +quantop
 + : '​\\E'​ -> EXISTS
 + | '​\\A'​ -> FORALL
 + ;
 +
 +sym_expr
 + :​ command_id
 + | '​['​^ command_id (','​! command_id)* '​]'​!
 + ;
 +
 +command_id
 + : id
 +// | id '​\''​^
 + ;
 +
 +compare_expr
 + :​ equality_expr (cmp_op^ compare_expr)*
 + ;
 +
 +cmp_op
 + :​ '>'​
 + | '<'​
 + | '>​='​
 + | '<​='​
 + ;
 +
 +equality_expr
 + : add_expr (eq_op^ equality_expr)*
 + ;
 +
 +eq_op
 + :​ '​='​
 + | '​!='​
 + ;
 +
 +add_expr
 + :​ mult_expr (add_op^ add_expr)*
 + ;
 +
 +add_op
 + :​ '​+'​
 + | '​-'​
 + ;
 +
 +mult_expr
 + : exp_expr (mult_op^ mult_expr)*
 + ;
 +
 +mult_op
 + :​ '​*'​
 + | '/'​
 + | '​%'​
 + ;
 +
 +exp_expr
 + :​ unary_expr ('​^'​^ exp_expr)*
 + ;
 +
 +unary_expr
 + :​ vecref_expr
 + | '​!'​^ vecref_expr
 + | '​-'​ vecref_expr -> ^(UMINUS vecref_expr)
 + | '​typeof'​^ vecref_expr
 + ;
 +
 +vecref_expr
 + :​ tuple_expr ('​.'​^ NUMBER)?
 + ;
 +
 +tuple_expr
 + : set_expr
 + | '​['​^ expr_or_empty_list '​]'​!
 + ;
 +
 +set_expr
 + :​ secondary_expr
 + | '​{'​^ expr_or_empty_list '​}'​!
 + | '​{'​ such_that_expr '​}'​ -> ^(SET_BUILDER such_that_expr)
 + | '​{'​ '​|'​ expression '​|'​ such_that_expr '​}'​ -> ^(SET_BUILDER ^('​|'​ expression) such_that_expr)
 + ;
 +
 +expr_or_empty_list
 + :​ expression (','​! expression)*
 + |
 + ;
 +
 +secondary_expr
 + :​ primary_expr
 + | function_call
 + | if_expr
 + | bind_expr
 + ;
 +
 +if_expr
 + :​ '​if'​^ expression '​then'​! expression '​else'​! expression '​fi'​!
 + ;
 +
 +bind_expr
 + :​ '​let'​^ id '​='​! expression '​in'​! expression
 + ;
 +
 +primary_expr
 + : constant
 + | variable_expr
 + | '​@'​^ id
 + | '​('​! expression '​)'​!
 + | '​('​! such_that_expr '​)'​!
 + ;
 +
 +//​There'​s some kind of ambiguity when I use "​x[1]",​ so I put "​x.1"​ instead for now
 +//Also, to support the struct tuple idea (see above), this would have to allow 
 +//the following:
 +//​ command_id '​.'​^ (NUMBER|ID)
 +//and probably something more involved, like:
 +//​ command_id ('​.'​^ (NUMBER|ID))*
 +//though this could be handled by single accesses bound with a let... expression.
 +variable_expr
 + :​ command_id
 +//​ | command_id '​.'​^ NUMBER
 + ;
 +
 +such_that_expr
 + : sym_expr '​in'​! expression ':'​^ expression
 + ;
 +
 +constant
 + : NUMBER
 + | STRING
 + | BOOLEAN
 + | '​ERROR'​
 + ;
 +
 +id
 + : ID { 
 + //Make sure we don't use any kernal language key words (ones that aren't FSpec keywords)
 + String[] reserved = { "​set",​ "​addr",​ "​int",​ "​union",​ "​tuple",​ "​deset",​ "​setBuild",​
 + "​setFilter",​ "​id"​};​
 + for(String check : reserved) {
 + if( check.equalsIgnoreCase($ID.text) ) {
 + //just add $, which is a legal id in kernel, but not FSpec, so unique
 + String text = $ID.text + "​$";​
 + //​Replace returned token
 + root_0 = (Object)adaptor.nil();​
 + Object tok_tree = (Object)adaptor.create(new CommonToken(ID,​text));​
 + adaptor.addChild(root_0,​ tok_tree);
 + break;
 + }
 + }
 + }
 + ;
 +
 +//// Lexical Rules ////
 +
 +BOOLEAN
 + :​ '​true' ​
 + | '​false' ​
 + ;
 +
 +ID
 + : ID_CHAR (ID_CHAR | DIGIT)*
 + ;
 +
 +//Without "​fragment"​ it was complaining about prior tokens. ​ Since we never need ID_CHAR as a token, ​
 +//​let'​s call it a fragment so it can be used in the ID rule merely for convenience.
 +fragment ID_CHAR
 + :​ '​a'​..'​z'​
 + | '​A'​..'​Z'​
 + | '​_'​
 + //​| '​$'​ //​|'​+'​|'​*'​|'/'​|'​%'​|'​-'​
 + ;
 +
 +NUMBER
 + : DIGIT+ ('​.'​ DIGIT+)? ​
 + ;
 +
 +fragment DIGIT
 + :​ ('​0'​..'​9'​)
 + ;
 +
 +//*
 +STRING
 + : '"'​ ( ~('​\\'​ | '"'​) | ('​\\'​ .) )* '"'​
 + //any char other than \ or ", ​ or \ followed by any one char
 + ;
 +//*/
 +
 +/* Example of parsing a string * /
 +STRING: '"'​ ( ESCAPE | ~('"'​|'​\\'​) )* '"'​ ;
 +
 +protected
 +ESCAPE
 +    :    '​\\'​
 +         ( '​n'​ { $setText("​\n"​);​ }
 +         | '​r'​ { $setText("​\r"​);​ }
 +         | '​t'​ { $setText("​\t"​);​ }
 +         | '"'​ { $setText("​\""​);​ }
 +         )
 +    ;
 +//*/
 +
 +COMMENT
 + :​ '#'​ ~('​\n'​|'​\r'​)* '​\r'?​ '​\n'​
 + { $channel = HIDDEN; }
 + | '​(#'​ ( (~'#'​) | ('#'​ ~'​)'​) )* '#​)'​
 + { $channel = HIDDEN; }
 + ;
 +
 +
 +WS
 + : (' ' | '​\r'​ | '​\t'​ | '​\u000C'​ | '​\n'​)
 + { $channel = HIDDEN; }
 + ;
 +
 +</​code>​
vv-lab/formalspec.g.txt ยท Last modified: 2015/02/18 22:13 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0