UV Manual: Grammer of the Input Language
UV Manual: Grammer of the Input Language
Warning
Grammar Notation
The grammer for the UV input language is presented in an extended BNF
based on the following conventions:
::=",
"|", and "( )*" (without the quotation marks).
Their respective meaning is as follows:
::=|( )*
Lexical Conventions
The UV input language is case sensitive. The input is made up from a
sequence of tokens and whitespace (i.e. blanks, tabs, and newline
characters as well as comments). Whitespace only
is significant for separating tokens, beyond that it is ignored.
Tokens
Tokens are either terminals as appearing in the grammar rules below,
or strings of characters representing the <number>,
<name> and <external>
non-terminals.
Comments
A comments starts with the characters "//" (without the
quotation marks) and ends with the first following newline character.
Numbers
A number as generated by the non-terminal <number>
is a string one or more digits, restricted by some implementation
dependent limitations on the number size. It is guaranteed that 15 bit
numbers (i.e. numbers from 0 to 32767) are supported.
Names
A names as generated by the non-terminal <name> is
any string of one or more characters made up from letters and digits
starting with a letter. Names are case-sensitive and the following
keywords of the UV language are not available for names:
assign, by,
co, const,
constant, declare,
end, ensures,
if, in,
initially, invariant,
program, stable,
transient, type,
unless, and var.
Names are used for denoting variables, programs, types, and record fields.
Examples of names are hello, isDone, and
t34y0.
External Names
An external name as generated by the non-terminal
<external> consistes of the string
#expr followed (without any whitespace in between) by a
string of one or more digits. The maximum number of allowed digits is
implementation dependent, but at least four digits are guaranteed.
External names are used for denoting expressions that have been
generated interactively during a session with the UV system. Examples
of external names are #expr76 and #expr003.
Expressions
Expressions are generated by the non-terminal
<expr>. The following table lists all operators in
increasing order of their binding power (operators in the same group share the same binding power, in which case the operators are left associative (if allowed by the typing rules)):
== (boolean equivalence)=!= (boolean antiequivalence, exclusive or)
==> (boolean implication)<== (boolean follows-from)
/\ (boolean conjunction)\/ (boolean disjunction)
! (boolean negation)
=, !=, >,
>=, <,
<= (nonboolean relational operators)
+ (addition)- (subtraction)
+ (unary plus)- (unary negation)
. (record field access, mapping indexing)
<expr> ::= <name>
| <external>
| <number>
| ( <expr> )
| <expr> . <name>
| <expr> . <expr>
| + <expr>
| - <expr>
| <expr> + <expr>
| <expr> - <expr>
| <expr> = <expr>
| <expr> != <expr>
| <expr> > <expr>
| <expr> < <expr>
| <expr> >= <expr>
| <expr> <= <expr>
| true
| false
| ! <expr>
| <expr> /\ <expr>
| <expr> \/ <expr>
| <expr> ==> <expr>
| <expr> <== <expr>
| <expr> == <expr>
| <expr> =!= <expr>
<exprList> ::= <expr> (, <expr>)*
<type> ::= <name>
| boolean
| int( <expr> .. <expr> )
| cyclic( <expr> )
| bits( <expr> )
| enum( <nameList> )
| { <compList> }
| <type> -> <type>
<nameList> ::= <name> (, <name>)*
<compList> ::= <compItem> (, <compItem>)*
<compItem> ::= <name> : <type>
Relevant non-terminals:
<name>,
<expr>.
<program> ::= program <name>
<declare>
<always>
<initial>
<assign>
end
Relevant non-terminals:
<name>,
<declare>,
<always>,
<initially>,
<assign>.
<declare> ::= declare (<declItem> ;)*
<declItem> ::= var <declSymbols> : <type>
| type <declSymbols> = <type>
<declSymbols> ::= <name> (, <name>)*
Relevant non-terminals:
<name>,
<type>.
<always> ::= always (<defItem> ;)* <defItem> ::= <name> : <type> = <expr>Relevant non-terminals:
<name>,
<type>,
<expr>.
<initial> ::= initially (<expr> ;)*Relevant non-terminals:
<expr>.
<assign> ::= assign (<statement>)*
<statement> ::= <statLabel> <simpleStat>
<statLabel> ::= []
| [ <name> ]
<simpleStat> ::= <assignment> (|| <assignment>)*
<assignment> ::= <lhs> := <rhs>
<lhs> ::= <var> (, <lvalue>)*
<lvalue> ::= <name>
| <lvalue> . <name>
| <lvalue> . <expr>
<rhs> ::= <exprList>
| <condRhs> (~ <condRhs>)*
<condRhs> ::= <exprList> if <expr>
Relevant non-terminals:
<name>,
<expr>.
Properties
<property> ::= constant <expr>
| invariant <expr>
| stable <expr>
| transient <expr>
| <expr> co <expr>
| <expr> ensures <expr>
| <expr> unless <expr>
| <expr> --> <expr>
| <expr> --> <expr> by <regexp>
Relevant non-terminals:
<expr>.
Regular Expressions
<regexp> ::= []
| [ <name> ]
| ( <regexp> )
| <regexp> + <regexp>
| <regexp> <regexp>
| <regexp> *
Relevant non-terminals:
<name>.
<input> ::= <unit>*
<unit> ::=
| <scopedUnit> ;
| in <name> : <scopedUnit> ;
| <program> ;
| <declItem> ;
<scopedUnit> ::= <expr>
| <property> ;
Relevant non-terminals:
<name>,
<program>,
<declItem>,
<property>,
<expr>.