<letter>	::=	A | B |... | Z | a |... | z
<digit>	::=	0 | 1 |... | 9
<alphanumeric>	::=	<letter> | <digit> | '
<special symbol>	::=	<basic symbol> | <operator>
<basic symbol>	::=	begin | end | endof | ; | : | ( | ) | $ | :: | & |
		if | then | else | fi | case |
		of | esac | fo | with | in | ni | first | suchthat | from | do | od |
		for | exitloop | leave | skip | assert |
		var | const | aux | as specified | = | init |
		final | unk | ? | proc | vproc | func | sel | label |
		note | eton | ! | elif | elof | pform | while | > | < | . | # |
		copy | alias | form | inline | pre | post | rule |
		is | forward | external | specs | impl | shared |
		invariant | initially | axiom | repmap |
		record | enumerated | assumes | value | generator
<operator>	::=	<binary operator> | <unary operator>
<binary operator>	::=	↑ | * | / | div | rem | + | - | < | ≤ | = | <> | ≥ | > | and | or | cand | cor | imp |
		<assign op>
<unary operator>	::=	+ | - | not
<identifier>	::=	<letter> {<alphanumeric>}*
<special identifier>	::=	&start | &finish | &next | &done | &value | &subscript | &<operator>
<identifier list>	::=	<identifier>,+
<special literal>	::=	<unsigned integer> | <unsigned real> | <string> | <boolean> | <radix>
<unsigned integer>	::=	{<digit>}+
<unsigned real>	::=	<unsigned rational>{E<scale-factor>}# | <unsigned integer>E<scale-factor>
<unsigned rational>	::=	<unsigned integer>.<unsigned integer>
<scale-factor>	::=	{+|-}#<unsigned integer>
<string>	::=	"<any sequence of characters with all quotes doubled>"
<boolean>	::=	true | false
<radix>	::=	{<alphanumeric>}+#<alphanumeric>
<compilation unit>	::=	begin <block> end | <exec decl list>
<block>	::=	{<exec decl list>;}# {<stmt>};+ {;}#
<exec decl list>	::=	{ <exec decl> };*
<exec decl>	::=	<var decl> | <const decl> | <proc decl> | <form decl> | <label decl>
<expression>	::=	<invocation> | <conditional expression> | <value expression> |
		<with expression> | <first expression>
<stmt>	::=	<expression> | <loop stmt> | <exit stmt> | <null stmt> |
		<inner block> | <labeled stmt> | <assert stmt>
<labeled stmt>	::=	<identifier> : <stmt>
<invocation>	::=	<special literal> | <simple invocation>{<actuals>}# | (<invocation>)
<actuals>	::=	({<actual>},*)
<actual>	::=	<expression> | <type description>
<simple invocation>	::=	{ <identifier>$ }* <identifier> | <special identifier>
<conditional expression>	::=	<if expression> | <case expression>
<if expression>	::=	if <expression> then <block> { elif <expression> then <block> }# { else <block> }# fi
<case expression>	::=	case <expression> of <case> { elof <case> }* { else <block> }# esac
<case>	::=	{ <expression> },+ :: <block>
<value expression>	::=	value <identifier>{:<obj type>}# of <block> fo
<with expression>	::=	with <with list> in <block> ni
<with list>	::=	{ <identifier>:<invocation> },+
<first expression>	::=	first <template> suchthat <expression> { then <block> }# { else <block> }# fi
<template>	::=	<identifier> from {<identifier>:}#<type description> | <identifier> from <invocation>
<loop stmt>	::=	<simple loop> | <while stmt> | <for stmt>
<simple loop>	::=	do <block> od
<while stmt>	::=	while <expression> <simple loop>
<for stmt>	::=	for <template> <simple loop>
<exit stmt>	::=	exitloop | leave <identifier>
<null stmt>	::=	skip
<inner block>	::=	begin <block> end | begin <block> endof {<identifier>}#
<assert stmt>	::=	assert <assertion>
<label decl>	::=	label <identifier list>
<var decl>	::=	<aux> var { <obj decl group>{<init fin clause>}# },+
<const decl>	::=	<aux> const {<obj decl group> {<init fin clause>}# | <const assign>},+
<aux>	::=	{ aux }#
<obj decl group>	::=	<identifier list> : <obj type>
<obj type >	::=	<type description> | as specified
<init fin clause>	::=	= <expression> | { init <stmt> }# { final <stmt> }#
<const assign>	::=	<identifier list> = <expression>
<type description>	::=	<simple invocation> { ( {<formal qual>},+ ) }# {<update set>}# |
		?<identifier> { <update set> }#
<formal qual>	::=	<expression> | ?<identifier> { <update set> }# | { <identifier>: }# <type description> |
		unk
<update set>	::=	< { <identifier> | <special identifier> },+ >
<formals>	::=	( { <routine formal> | <binding> <obj formal> | <type formal> },+ )
<routine formal>	::=	<formal id list> proc <parms> | <formal id list> { vproc | func | sel } <v parms>
<binding>	::=	{ copy | { alias }# { const | var } }#
<formal id list>	::=	<identifier list> :
<obj formal>	::=	<formal id list> <type description>
<type formal>	::=	<formal id list> { form | pform } { <update set> }#
<routine decl>	::=	<vproc decl> | <proc decl> | <sel decl>
<vproc decl>	::=	<aux> {inline}# {vproc | func} <routine id> <v parms> <pre post> <assumes>
		{ <routine body> }#
<proc decl>	::=	<aux> {inline}# proc <routine id> <parms> <pre post> <assumes> { <routine body> }#
<sel decl>	::=	<aux> {inline}# sel <routine id> <v parms> <pre post> <assumes> { <routine body> }#
<routine id>	::=	<identifier> | <special identifier>
<parms>	::=	{ <formals> }#
<v parms>	::=	{ <formals> }# : <type description>
<pre>	::=	{ pre <assertion>; }#
<pre post>	::=	<pre> { post <assertion>; }#
<routine body>	::=	is <stmt> | is as specified | is forward | is external (<system specs>)
<form decl>	::=	<aux> form <identifier> { <formals> }# <pre> <assumes> is <form body>
<form body>	::=	{ <specs> }# { <impl> }# end { <identifier> }# | <abbrev body> | forward | external
		( <system specs> ) | as specified
<specs>	::=	specs { <var decl> | <other form decls> };+
<impl>	::=	impl { <shared> <var decl> | <other form decls> };
<other form decls>	::=	<routine decl> | <form decl> | <axiom>| <shared> <const decl>
<shared>	::=	shared #
<axiom>	::=	invariant <assertion> | initially <assertion> | axiom <assertion> | repmap
		<assertion> | rule <identifier> <assertion>
<abbrev body>	::=	<record type> | <enumerated type>
<record type>	::=	record ( { <obj decl group> },+ )
<enumerated type>	::=	enumerated ( <identifier list> )
<form decl>	::=	<aux> generator <identifier> { <formals> }# : <type description> <pre> <assumes>
		is <form body>
<assumes>	::=	{assumes <form decl>},*