Specify what "is equivalent to" means.

docs/language/dartLangSpec.tex

 \documentclass{article}
 \usepackage{epsfig}
 \usepackage{color}
 \usepackage{dart}
 \usepackage{bnf}
 \usepackage{hyperref}
 \usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \newcommand{\code}[1]{{\sf #1}}
 \title{Dart Programming Language Specification  \\
 {5th edition draft}\\
 {\large Version 2.0.0-dev}}
 
 % For information about Location Markers (and in particular the
 % commands \LMHash and \LMLabel), see the long comment at the
 % end of this file.
 
 % CHANGES
 % =======
 % Significant changes to the specification.
 %
 % 2.0
 % - Don't allow functions as assert test values.
 % - Start running "async" functions synchronously.
+% - Specify what "is equivalent to" means.
 %
 % 1.15
 % - Change how language specification describes control flow.
 % - Object initialization now specifies initialization order correctly.
 % - Specifies that leaving an await-for loop must wait for the subscription
 %   to be canceled.
 % - An await-for loop only pauses the subscription if it does something async.
 % - Assert statements allows a "message" operand and a trailing comma.
 % - The Null type is now considered a subtype of all types in most cases.
 % - Specify what NEWLINE means in multiline strings.
@@ skipping 142 matching lines @@
 The notation $[x_1, \ldots, x_n/y_1, \ldots, y_n]E$ denotes a copy of $E$ in which all occurrences of $y_i, 1 \le i \le n$ have been replaced with $x_i$.
 
 \LMHash{}
 We sometimes abuse list or map literal syntax, writing $[o_1, \ldots, o_n]$  (respectively $\{k_1: o_1, \ldots, k_n: o_n\}$) where the $o_i$ and $k_i$ may be objects rather than expressions. The intent is to denote a list (respectively map) object whose elements are the $o_i$ (respectively, whose keys are the $k_i$ and values are the $o_i$).
 
 \LMHash{}
 The specifications of operators often involve statements such as $x$ $op$ $y$ is equivalent to the method invocation $x.op(y)$. Such specifications should be understood as a shorthand for:
 \begin{itemize}
 \item
  $x$ $op$ $y$ is equivalent to the method invocation $x.op^\prime(y)$, assuming the class of $x$ actually declared a non-operator method named $op^\prime$ defining the same function as the operator $op$.
- \end{itemize}
+\end{itemize}
 
  \rationale{This circumlocution is required because x.op(y), where op is an operator, is not legal syntax. However, it is painfully verbose, and we prefer to state this rule once here, and use a concise and clear notation across the specification.
  }
 
 \LMHash{}
 When the specification refers to the order given in the program, it means the order of the program source code text, scanning left-to-right and top-to-bottom.
 
 \LMHash{}
 When the specification refers to a {\em fresh variable}, it means a variable with a name that doesn't occur anywhere in the current program.
 When the specification introduces a fresh variable bound to a value, the fresh variable is implicitly bound in a surrounding scope.
 
 \LMHash{}
 References to otherwise unspecified names of program entities (such as classes or functions) are interpreted as the names of members of the Dart core library.
 
 \commentary{
 Examples would be the classes \code{Object} and \code{Type} representing the root of the class hierarchy and the reification of runtime types respectively.
 }
 
+\LMHash{}
+When the specification says that one piece of syntax {\em is equivalent to} another piece of syntax, it means that it is equivalent in all ways, and the former syntax should generate the same static warnings and have the same runtime behavior as the latter.
+\commentary {
+Error messages, if any, should always refer to the original syntax.
+}
+If execution or evaluation of a construct is said to be equivalent to execution or evaluation of another construct, then only the runtime behavior is equivalent, and only the static warnings or errors mentioned for the original syntax applies.
+
 \section{Overview}
 \LMLabel{overview}
 
 \LMHash{}
 Dart is a class-based, single-inheritance, pure object-oriented programming language. Dart is optionally typed (\ref{types}) and supports reified generics. The run-time type of every object is represented as an instance of class \code{Type}  which can be obtained by calling the getter  \code{runtimeType} declared in class \code{Object}, the root of the Dart class hierarchy.
 
 \LMHash{}
 Dart programs may be statically checked. The static checker will report some violations of the type rules, but such violations do not abort compilation or preclude execution.
 
 \LMHash{}
@@ skipping 318 matching lines @@
 }
 
 \end{dartCode}
 
 % the grammar does not support local getters and setters. The local var discussion does not seem to mention getters and setters based semantics. It simply discusses the creation of the variable, not its access. Access is either assignment or identifiers. Identifiers ignore the getter story.
 
 \LMHash{}
 The following rules apply to all static and instance variables.
 
 \LMHash{}
-A  variable declaration  of one of the forms \code{$T$ $v$;},  \code{$T$ $v$ = $e$;} ,  \code{\CONST{} $T$ $v$ = $e$;}, \code{\FINAL{} $T$ $v$;}  or \code{\FINAL{} $T$ $v$ = $e$;} always induces an implicit  getter function (\ref{getters}) with signature
+A  variable declaration  of one of the forms \code{$T$ $v$;}, \code{$T$ $v$ = $e$;}  \code{\CONST{} $T$ $v$ = $e$;}, \code{\FINAL{} $T$ $v$;} or \code{\FINAL{} $T$ $v$ = $e$;} always induces an implicit  getter function (\ref{getters}) with signature
 
 $T$ \GET{} $v$
 
 whose invocation evaluates as described below (\ref{evaluationOfImplicitVariableGetters}).
 
 
 \LMHash{}
 A  variable declaration  of one of the forms \code{\VAR{} $v$;},  \code{\VAR{} $v$ = $e$;} ,  \code{\CONST{} $v$ = $e$;}, \code{\FINAL{} $v$;} or \code{\FINAL{}  $v$ = $e$;}  always induces an implicit  getter function with signature
 
  \GET{} $v$
@@ skipping 266 matching lines @@
 \begin{grammar}
 {\bf defaultFormalParameter:}
       normalFormalParameter (`=' expression)?
     .
 
 {\bf defaultNamedParameter:}normalFormalParameter (`=' expression)?;
       normalFormalParameter ( `{\escapegrammar :}' expression)?
     .
 \end{grammar}
 
-A {\bf defaultNamedParameter} on the form:
+A {\bf defaultNamedParameter} of the form:
 \begin{code}
    normalFormalParameter : expression
 \end{code}
-is equivalent to one on the form:
+is equivalent to one of the form:
 \begin{code}
    normalFormalParameter = expression
 \end{code}
 The colon-syntax is included only for backwards compatibility.
 It is deprecated and will be removed in a later version of the language specification.
 
 \LMHash{}
 It is a compile-time error if the default value of an optional parameter is not a compile-time constant (\ref{constants}). If no default is explicitly specified for an optional parameter an implicit default of \NULL{} is provided.
 
 \LMHash{}
@@ skipping 3109 matching lines @@
 
 If $e_f$ is a property extraction expression (\ref{propertyExtraction}), then $i$ isn't a function expression invocation and is instead recognized as an ordinary method invocation (\ref{ordinaryInvocation}).
 
 \commentary{
 \code{$a.b(x)$} is parsed as a method invocation of method \code{$b()$} on object \code{$a$}, not as an invocation of getter \code{$b$} on \code{$a$} followed by a function call \code{$(a.b)(x)$}.  If a method or getter \code{$b$} exists, the two will be equivalent. However, if \code{$b$} is not defined on \code{$a$}, the resulting invocation of \code{noSuchMethod()} would differ.  The \code{Invocation} passed to \code{noSuchMethod()} would describe a call to a method \code{$b$} with argument \code{$x$} in the former case, and a call to a getter \code{$b$} (with no arguments) in the latter.
 }
 
 \LMHash{}
 Otherwise:
 
-A function expression invocation $e_f(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is equivalent to $e_f.call(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
+Execution of a function expression invocation $e_f(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is equivalent to execution of $e_f.call(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
 
 \commentary{
 The implication of this definition, and the other definitions involving the method \code{call()}, is that user defined types can be used as function values provided they define a \CALL{} method. The method \CALL{} is special in this regard. The signature of the \CALL{} method determines the signature used when using the object via the built-in invocation syntax.
 }
 
 \LMHash{}
 It is a static warning if the static type $F$ of $e_f$ may not be assigned to a function type.  If $F$ is not a function type, the static type of $i$ is \DYNAMIC{}. Otherwise
 the static type of $i$ is the declared return type of  $F$.
 %\item Let $T_i$ be the static type of $a_i, i \in 1 .. n+k$. It is a static warning if $F$ is not a supertype of  $(T_1, \ldots, T_n, [T_{n+1}$ $x_{n+1}, \ldots, T_{n+k}$ $x_{n+k}]) \to \bot$.
 %\end{itemize}
@@ skipping 913 matching lines @@
 \LMHash{}
 An {\em equality expression} is either a relational expression (\ref{relationalExpressions}), or an invocation of an equality operator on either \SUPER{} or an expression $e_1$, with argument $e_2$.
 
 
 \LMHash{}
 Evaluation of an equality expression $ee$ of the form \code{$e_1$ == $e_2$} proceeds as follows:
 \begin{itemize}
 \item The expression $e_1$ is evaluated to an object $o_1$.
 \item The expression $e_2$ is evaluated to an object $o_2$.
 \item If either $o_1$ or $o_2$ is \NULL{}, then $ee$ evaluates to \TRUE{} if both $o_1$ and $o_2$ are \NULL{} and to \FALSE{} otherwise.  Otherwise,
-\item $ee$ is equivalent to the method invocation \code{$o_1$.==($o_2$)}.
+\item evaluation of $ee$ is equivalent to the method invocation \code{$o_1$.==($o_2$)}.
 \end{itemize}
 
 
 \LMHash{}
 Evaluation of an equality expression $ee$ of the form \code{\SUPER{} == $e$} proceeds as follows:
 \begin{itemize}
 \item The expression $e$ is evaluated to an object $o$.
 \item If either \THIS{} or $o$ is \NULL{}, then $ee$ evaluates to evaluates to \TRUE{} if both \THIS{} and $o$ are \NULL{} and to \FALSE{} otherwise. Otherwise,
-\item $ee$ is equivalent to the method invocation \code{\SUPER{}.==($o$)}.
+\item evaluation of $ee$ is equivalent to the method invocation \code{\SUPER{}.==($o$)}.
 \end{itemize}
 
 \commentary{As a result of the above definition, user defined \code{==} methods can assume that their argument is non-null, and avoid the standard boiler-plate prelude:
 
  \code{if (identical(\NULL{}, arg)) return \FALSE{};}
 
 Another implication is that there is never a need to use \code{identical()} to test against \NULL{}, nor should anyone ever worry about whether to write \NULL{} == $e$ or $e$ == \NULL{}.
 }
 
 \LMHash{}
@@ skipping 55 matching lines @@
 {\bf bitwiseOperator:}`\&';
       `\^{}';
       `$|$'
     .
  \end{grammar}
 
 \LMHash{}
 A {\em bitwise expression} is either a shift expression (\ref{shift}), or an invocation of a bitwise operator on either \SUPER{} or an expression $e_1$, with argument $e_2$.
 
 \LMHash{}
- A bitwise expression of the form  $e_1$ $op$ $e_2$ is equivalent to the method invocation $e_1.op(e_2)$.
-A bitwise expression of the form  \code{\SUPER{} $op$ $e_2$} is equivalent to the method invocation \code{\SUPER{}.op($e_2$)}.
+A bitwise expression of the form \code{$e_1$ $op$ $e_2$} is equivalent to the method invocation $e_1.op(e_2)$.
+A bitwise expression of the form \code{\SUPER{} $op$ $e_2$} is equivalent to the method invocation \code{\SUPER{}.$op$($e_2$)}.
 
 \commentary{
 It should be obvious that the static type rules for these expressions are defined by the equivalence above - ergo, by the type rules for method invocation and the signatures of the operators on the type $e_1$. The same holds in similar situations throughout this specification.
 }
 
 
 \subsection{ Shift}
 \LMLabel{shift}
 
 \LMHash{}
@@ skipping 107 matching lines @@
     {\bf tildeOperator:}  `\~{}'
     .
 
 
 \end{grammar}
 
 \LMHash{}
 A {\em unary expression} is either a postfix expression  (\ref{postfixExpressions}), an await expression (\ref{awaitExpressions}) or an invocation of a prefix operator on an expression or an invocation of a unary operator on either \SUPER{} or an expression $e$.
 
 \LMHash{}
-The expression $!e$ is equivalent to the expression $e?$ $ \FALSE{} :\TRUE{}$.
+The expression $!e$ is equivalent to the expression \code{$e$ ? \FALSE{} : \TRUE{}}.
 
 \LMHash{}
 Evaluation of an expression of the form \code{++$e$} is equivalent to \code{$e$ += 1}.  Evaluation of an expression of the form \code{-{}-$e$} is equivalent to \code{$e$ -= 1}.
 
 %The expression $-e$ is equivalent to the method invocation \code{$e$.-()}.  The expression \code{-\SUPER{}} is equivalent  to the method invocation \code{\SUPER{}.-()}.
 
 \LMHash{}
 An expression of the form \code{$op$ $e$} is equivalent to the method invocation \code{$e.op()$}. An expression of the form \code{$op$ \SUPER{}} is equivalent to the method invocation  (\ref{superInvocation}) \code{\SUPER{}.$op()$}.
 
 \subsection{ Await Expressions}
@@ skipping 184 matching lines @@
 Evaluate \code{$a$[$i$]} to an object $r$
 and let $y$ be a fresh variable bound to $r$.
 Evaluate \code{$a$[$i$] = $y$ - 1}.
 Then $e$ evaluates to $r$.
 
 \LMHash{}
 The static type of such an expression is the static type of \code{$e_1$[$e_2$]}.
 
 \LMHash{}
 Evaluation of a postfix expression $e$ of the form \code{$e_1$?.$v$++}
-where $e_1$ is not a type literal, proceeds as follows:
+proceeds as follows:
 
 \LMHash{}
-If $e_1$ is a type literal, $e$ is equivalent to \code{$e_1$.$v$++}.
+If $e_1$ is a type literal, evaluation of $e$ is equivalent to
+evaluation of \code{$e_1$.$v$++}.
 
 \LMHash{}
 Otherwise evaluate $e_1$ to an object $u$.
 if $u$ is the null value, $e$ evaluates to the null value.
 Otherwise let $x$ be a fresh variable bound to $u$.
 Evaluate \code{$x$.$v$++} to an object $o$.
 Then $e$ evaluates to $o$.
 
 \LMHash{}
 The static type of such an expression is the static type of \code{$e_1$.$v$}.
 
 \LMHash{}
 Evaluation of a postfix expression $e$ of the form \code{$e_1$?.$v$-{}-}
-where $e_1$ is not a type literal, proceeds as follows:
+proceeds as follows:
 
-If $e_1$ is a type literal, $e$ is equivalent to \code{$e_1$.$v$-{}-}.
+If $e_1$ is a type literal, evaluation of $e$ is equivalent to
+evaluation of \code{$e_1$.$v$-{}-}.
 
 Otherwise evaluate $e_1$ to an object $u$.
 If $u$ is the null value, $e$ evaluates to the null value.
 Otherwise let $x$ be a fresh variable bound to $u$.
 Evaluate \code{$x$.$v$-{}-} to an object $o$.
 Then $e$ evaluates to $o$.
 
 
 \LMHash{}
 The static type of such an expression is the static type of \code{$e_1$.$v$}.
@@ skipping 48 matching lines @@
 \LMHash{}
 An assignable expression of the form $e.id$ or $e?.id$ is evaluated as a property extraction  (\ref{propertyExtraction}).
 
 \LMHash{}
 An assignable expression of the form \code{$e_1$[$e_2$]} is evaluated as a method invocation of the operator method \code{[]} on $e_1$ with argument $e_2$.
 
 \LMHash{}
 An assignable expression of the form \code{\SUPER{}.id}  is evaluated as a property extraction.
 
 \LMHash{}
-An assignable expression of the form \code{\SUPER{}[$e_2$]} is equivalent to the method invocation  \code{\SUPER{}.[]($e_2$)}.
+Evaluation of an assignable expression of the form \code{\SUPER{}[$e_2$]} is equivalent to evaluation of the method invocation  \code{\SUPER{}.[]($e_2$)}.
 
 \subsection{ Identifier Reference}
 \LMLabel{identifierReference}
 
 \LMHash{}
 An {\em identifier expression} consists of a single identifier; it provides access to an object via an unqualified name.
 
 \begin{grammar}
 {\bf identifier:}
       IDENTIFIER
@@ skipping 80 matching lines @@
 %\item If $d$ is a library variable then:
 %  \begin{itemize}
 %  \item If $d$ is of one of the forms \code{\VAR{} $v$ = $e_i$;} , \code{$T$ $v$ = $e_i$;} , \code{\FINAL{} $v$ = $e_i$;}  or \code{\FINAL{} $T$ $v$ = $e_i$;} and no value has yet been stored into $v$ then the initializer expression $e_i$ is evaluated. If, during the evaluation of $e_i$, the getter for $v$ is referenced, a \code{CyclicInitializationError} is thrown. If the evaluation succeeded yielding an object $o$, let $r = o$, otherwise let $r = \NULL{}$. In any case, $r$ is stored into $v$. The value of $e$ is $r$.
  \item  If $d$ is a constant variable of one of the forms  \code{\CONST{} $v$ = $e$;} or \code{\CONST{} $T$ $v$ = $e$;} then the value $id$ is the value of the compile-time constant $e$.
 %  Otherwise
 %  \item $e$ evaluates to the current binding of $id$.
 %  \end{itemize}
 \item If $d$ is a local variable or formal parameter then $e$ evaluates to the current binding of $id$.
 %\item If $d$ is a library variable, local variable, or formal parameter, then $e$ evaluates to the current binding of $id$. \commentary{This case also applies if d is a library or local function declaration, as these are equivalent to function-valued variable declarations.}
 \item If $d$ is a static method, top-level function or local function then $e$ evaluates to the function defined by $d$.
-\item If $d$ is the declaration of a static variable, static getter or static setter declared in class $C$, then $e$ is equivalent to the property extraction (\ref{propertyExtraction}) $C.id$.
-\item If $d$ is the declaration of a library variable, top-level getter or top-level setter, then $e$ is equivalent to the top level getter invocation (\ref{topLevelGetterInvocation}) $id$.
+\item If $d$ is the declaration of a static variable, static getter or static setter declared in class $C$, then evaluation of $e$ is equivalent to evaluation of the property extraction (\ref{propertyExtraction}) $C.id$.
+\item If $d$ is the declaration of a library variable, top-level getter or top-level setter, then evaluation of $e$ is equivalent to evaluation of the top level getter invocation (\ref{topLevelGetterInvocation}) $id$.
 \item Otherwise, if $e$ occurs inside a top level or static function (be it function, method, getter,  or setter) or variable initializer, evaluation of $e$ causes a \code{NoSuchMethod} to be thrown.
-\item Otherwise, $e$ is equivalent to the property extraction (\ref{propertyExtraction}) \THIS{}.$id$.
+\item Otherwise, evaluation of $e$ is equivalent to evaluation of the property extraction (\ref{propertyExtraction}) \THIS{}.$id$.
 % This implies that referring to an undefined static getter by simple name is an error, whereas doing so by qualified name is only a warning. Same with assignments.  Revise?
 \end{itemize}
 
 \LMHash{}
 The static type of $e$ is determined as follows:
 
 \begin{itemize}
 \item If $d$ is a class, type alias or type parameter the static type of $e$ is \code{Type}.
 \item If $d$ is a local variable or formal parameter the static type of $e$ is the type of the variable $id$, unless $id$ is known to have some type $T$, in which case the static type of $e$ is $T$, provided that $T$ is more specific than any other type $S$ such that $v$ is known to have type $S$.
 \item If $d$ is a static method, top-level function or local function the static type of $e$ is the function type defined by $d$.
@@ skipping 205 matching lines @@
  \begin{grammar}
 {\bf localVariableDeclaration:}
     initializedVariableDeclaration `{\escapegrammar ;}'
   .
  \end{grammar}
 
 \LMHash{}
  Executing a variable declaration statement of one of the forms  \VAR{} $v = e;$, $T$ $v = e; $, \CONST{}  $v = e;$, \CONST{} $T$ $v = e;$, \FINAL{}  $v = e;$ or \FINAL{} $T$ $v = e;$ proceeds as follows:
 
 \LMHash{}
- The expression $e$ is evaluated to an object $o$. Then, the variable $v$ is set to $o$.
+The expression $e$ is evaluated to an object $o$. Then, the variable $v$ is set to $o$.
 
 \LMHash{}
- A variable declaration statement of the form \VAR{} $v;$ is equivalent to \VAR{} $v = \NULL{};$. A variable declaration statement of the form $T$ $v;$ is equivalent to $T$ $v = \NULL{};$.
+A variable declaration statement of the form \code{\VAR{} $v$;} is equivalent to \code{\VAR{} $v$ = \NULL{};}. A variable declaration statement of the form \code{$T$ $v$;} is equivalent to \code{$T$ $v$ = \NULL{};}.
 
 \commentary{
 This holds regardless of the type $T$. For example, \code{int i;} does not cause \code{i} to be initialized to zero. Instead, \code{i} is initialized to \NULL{}, just as if we had written \VAR{} \code{i;} or \code{Object i;} or \code{Collection<String> i;}.
 }
 
 \rationale{
 To do otherwise would undermine the optionally typed nature of Dart, causing type annotations to modify program behavior.
 }
 
 %A variable declaration statement of one of the forms $T$ $v;$, $T$ $v = e;$, \CONST{} $T$ $v = e;$,  or \FINAL{} $T$ $v = e;$ causes a new getter named $v$ with static return type $T$ to be added to the innermost enclosing scope at the point following the variable declaration statement. The result of executing this getter is the value stored in $v$.
@@ skipping 68 matching lines @@
 \LMLabel{if}
 
 \LMHash{}
 The {\em if statement} allows for conditional execution of statements.
 
 \begin{grammar}
 {\bf ifStatement:}
       \IF{} `(' expression `)' statement ( \ELSE{} statement)?
     .
 \end{grammar}
+An if statement of the form \code{\IF{} ($e$) $s_1$ \ELSE{} $s_2$} where $s_1$ is not a block statement is equivalent to the statement \code{\IF{} ($e$) \{$s_1$\} \ELSE{} $s_2$}.
+An if statement of the form \code{\IF{} ($e$) $s_1$ \ELSE{} $s_2$} where $s_2$ is not a block statement is equivalent to the statement \code{\IF{} ($e$) $s_1$ \ELSE{} \{$s_2$\}}.
 
-Execution of an if statement of the form  \code {\IF{} (}$b$\code{)}$s_1$ \code{\ELSE{} } $s_2$ proceeds as follows:
-
-\LMHash{}
- First, the expression $b$ is evaluated to an object $o$. Then, $o$ is subjected to boolean conversion (\ref{booleanConversion}), producing an object $r$. If $r$ is \TRUE{}, then the statement $\{s_1\}$ is executed, otherwise statement $\{s_2\}$ is executed.
-
- \commentary {
- Put another way, \code {\IF{} (}$b$\code{)}$s_1$ \code{\ELSE{} } $s_2$ is equivalent to
- \code {\IF{} (}$b$\code{)}$\{s_1\}$ \code{\ELSE{} } $\{s_2\}$
- }
-
- \rationale {
- The reason for this equivalence is to catch errors such as
- }
- \begin{dartCode}
+\rationale {
+The reason for this equivalence is to catch errors such as
+}
+\begin{dartCode}
 \VOID{} main() \{
   \IF{} (somePredicate)
     \VAR{} v = 2;
   print(v);
 \}
 \end{dartCode}
 
 \rationale {
 Under reasonable scope rules  such code is problematic. If we assume that \code{v} is declared in the scope of the method \code{main()}, then when \code{somePredicate} is false, \code{v} will be uninitialized when accessed.  The cleanest approach would be to require a block following the test, rather than an arbitrary statement. However, this goes against long standing custom, undermining Dart's goal of familiarity.  Instead, we choose to insert a block, introducing a scope,  around the statement following the predicate (and similarly for \ELSE{} and loops). This will cause both a warning and a runtime error in the case above.  Of course, if there is a declaration of \code{v} in the surrounding scope, programmers might still be surprised. We expect tools to highlight cases of shadowing to help avoid such situations.
- }
+}
+
 
 \LMHash{}
-  It is a static type warning if the type of the expression $b$ may not be assigned to \code{bool}.
+Execution of an if statement of the form \code{\IF{} ($b$) $s_1$ \ELSE{} $s_2$} where $s_1$ and $s_2$ are block statements, proceeds as follows:
+
+\LMHash{}
+First, the expression $b$ is evaluated to an object $o$. Then, $o$ is subjected to boolean conversion (\ref{booleanConversion}), producing an object $r$. If $r$ is \TRUE{}, then the block statement $s_1$ is executed, otherwise the block statement $s_2$ is executed.
+
+\LMHash{}
+It is a static type warning if the type of the expression $b$ may not be assigned to \code{bool}.
 
 \LMHash{}
 If:
 \begin{itemize}
-\item  $b$ shows that a variable $v$ has type $T$.
-\item  $v$ is not potentially mutated in $s_1$ or within a closure.
+\item $b$ shows that a variable $v$ has type $T$.
+\item $v$ is not potentially mutated in $s_1$ or within a closure.
 \item If the variable $v$ is accessed by a closure in $s_1$ then the variable $v$ is not potentially mutated anywhere in the scope of $v$.
 \end{itemize}
 then the type of $v$ is known to be $T$ in $s_1$.
 
 \LMHash{}
- An if statement of the form  \code {\IF{} (}$b$\code{)}$s_1$ is equivalent to the if statement
-
- \code {\IF{} (}$b$\code{)}$s_1$ \code{\ELSE{} \{\}}.
-
+An if statement of the form \code{\IF{} ($e$) $s$} is equivalent to the if statement \code{\IF{} ($e$) $s$ \ELSE{} \{\}}.
 
 
 \subsection{For}
 \LMLabel{for}
 
 \LMHash{}
 The {\em for statement} supports iteration.
 
 \begin{grammar}
 {\bf forStatement:}
@@ skipping 11 matching lines @@
  \end{grammar}
 
 \LMHash{}
  The for statement has three forms - the traditional for loop and two forms of the for-in statement - synchronous and asynchronous.
 
 \subsubsection{For Loop}
 \LMLabel{forLoop}
 
 
 \LMHash{}
-Execution of a for statement of the form   \code{ \FOR{} (\VAR{} $v$ = $e_0$ ; $c$; $e$) $s$} proceeds as follows:
+Execution of a for statement of the form \code{ \FOR{} (\VAR{} $v$ = $e_0$ ; $c$; $e$) $s$} proceeds as follows:
 
 \LMHash{}
 If $c$ is empty then let $c^\prime$ be \TRUE{} otherwise let  $c^\prime$ be $c$.
 
 \LMHash{}
 First the variable declaration statement \VAR{} $v = e_0$ is executed. Then:
 \begin{enumerate}
 \item
 \label{beginFor}
 If this is the first iteration of the for loop, let $v^\prime$ be $v$. Otherwise,  let $v^\prime$ be the variable $v^{\prime\prime}$ created in the previous execution of step \ref{allocateFreshVar}.
@@ skipping 490 matching lines @@
 
 \LMHash{}
 An \ON{}-\CATCH{} clause of the form  \code{\CATCH{} ($p$) $s$} is equivalent to an \ON{}-\CATCH{} clause \code{\ON{} \DYNAMIC{} \CATCH{} ($p$, $p_2$) $s$} where $p_2$ is a fresh identifier.
 
 An \ON{}-\CATCH{} clause of the form \code{\CATCH{} ($p_1$, $p_2$) $s$} is equivalent to an \ON{}-\CATCH{} clause \code{\ON{} \DYNAMIC{} \CATCH{} ($p_1$, $p_2$) $s$}.
 
 \LMHash{}
 An \ON{}-\CATCH{} clause of the form   \code{\ON{} $T$ \CATCH{} ($p_1$, $p_2$) $s$} introduces a new scope $CS$ in which final local variables specified by $p_1$ and $p_2$ are defined. The statement $s$ is enclosed within $CS$. The static type of $p_1$ is $T$ and the static type of $p_2$ is \code{StackTrace}.
 
 \LMHash{}
-Execution of a \TRY{} statement $s$ on the form:
+Execution of a \TRY{} statement $s$ of the form:
 \begin{dartCode}
 \TRY{} $b$
 \ON{} $T_1$ \CATCH{} ($e_1$, $t_1$) $c_1$
 \ldots{}
 \ON{} $T_n$ \CATCH{} ($e_n$, $t_n$) $c_n$
 \FINALLY{} $f$
 \end{dartCode}
 proceeds as follows:
 
 \LMHash{}
 First $b$ is executed.
 If execution of $b$ throws (\ref{completion}) with exception object $e$ and stack trace $t$, then $e$ and $t$ are matched against the \ON{}-\CATCH{} clauses to yield a new completion (\ref{on-catch}).
 
 Then, even if execution of $b$ did not complete normally or matching against the \ON{}-\CATCH{} clauses did not complete normally, the $f$ block is executed.
 
 If execution of $f$ does not complete normally,
 execution of the \TRY{} statement completes in the same way.
 Otherwise if execution of $b$ threw (\ref{completion}), the \TRY{} statement completes in the same way as the matching against the \ON{}-\CATCH{} clauses.
 Otherwise the \TRY{} statement completes in the same way as the execution of $b$.
 
 \LMHash{}
 If $T_1$ is a malformed or deferred type (\ref{staticTypes}), then performing a match causes a run time error.
 It is a static warning if $T_i$, $1 \le i \le n$ is a deferred or malformed type.
 
 \subsubsection{\ON{}-\CATCH{} clauses}
 \LMLabel{on-catch}
 
 \LMHash{}
-Matching an exception object $e$ and stack trace $t$ against a (potentially empty) sequence of \ON{}-\CATCH{} clauses on the form
+Matching an exception object $e$ and stack trace $t$ against a (potentially empty) sequence of \ON{}-\CATCH{} clauses of the form
 \begin{dartCode}
 \ON{} $T_1$ \CATCH{} ($e_1$, $st_1$) \{ $s_1$ \}
 \ldots
 \ON{} $T_n$ \CATCH{} ($e_n$, $st_n$) \{ $s_n$ \}
 \end{dartCode}
 proceeds as follows:
 
 \LMHash{}
 If there are no \ON{}-\CATCH{} clauses ($n = 0$), matching throws the exception object $e$ and stack trace $t$ (\ref{completion}).
 
@@ skipping 317 matching lines @@
     .
 \end{grammar}
 
 \LMHash{}
 The grammar allows a trailing comma before the closing parenthesis,
 similarly to an argument list. That comma, if present, has no effect.
 An assertion with a trailing comma is equivalent to one with that
 comma removed.
 
 \LMHash{}
-An assertion on the form \code{\ASSERT($e$))} is equivalent to an assertion on the form \code{\ASSERT($e$, null)}.
+An assertion of the form \code{\ASSERT($e$))} is equivalent to an assertion of the form \code{\ASSERT($e$, null)}.
 
 \LMHash{}
 Execution of an assert statement executes the assertion as described below
 and completes in the same way as the assertion.
 
 \LMHash{}
 In production mode an assertion has no effect
 and its execution immediately completes normally (\ref{completion}).
 In checked mode,
 execution of an assertion \code{\ASSERT{}($c$, $e$)} proceeds as follows:
@@ skipping 1455 matching lines @@
 
 The invariant that each normative paragraph is associated with a line
 containing the text \LMHash{} should be maintained.  Extra occurrences
 of \LMHash{} can be added if needed, e.g., in order to make
 individual \item{}s in itemized lists addressable.  Each \LM.. command
 must occur on a separate line.  \LMHash{} must occur immediately
 before the associated paragraph, and \LMLabel must occur immediately
 after the associated \section{}, \subsection{} etc.
 
 ----------------------------------------------------------------------