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 "is equivalent to" another 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.

[eernst, 2017/08/21 10:15:20]

`"is equivalent to"` --> `{\em is equivalent to}`, for consistency with other
defining occurrences of a phrase. Might as well say `piece of syntax` both
times.

[Lasse Reichstein Nielsen, 2017/08/22 05:32:13]

Done.

+\commentary {
+If the syntax contains errors, implementations should obviously ensure that error messages only refer to the original syntax.

[eernst, 2017/08/21 10:15:20]

Maybe `Error messages, if any, should always refer to the original syntax.`

[Lasse Reichstein Nielsen, 2017/08/22 05:32:09]

Done.

+}
+If execution or evaluation of a construct is said to be equivalent with 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.

[eernst, 2017/08/21 10:15:21]

Might as well use `equivalent to` everywhere (`with` --> `to`).
Typo at the end: `applies` --> `apply`.
Then empty line before \section{..}.

[Lasse Reichstein Nielsen, 2017/08/22 05:32:10]

Done.

 \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 605 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:

[eernst, 2017/08/21 10:15:21]

I actually looked at this one at some point. Googling again for 'on the form'
and 'of the form' yield exactly 'About 498.000.000 results', so the search must
be abstracted into something like '{of,on} the form', but 'of the form' is
described as 'In mathematics, the phrase "of the form" indicates that a
mathematical object, or a collection of objects, follows a certain pattern of
expression.', https://en.wikipedia.org/wiki/Of_the_form.

So I concluded that 'of the form' is actually the standard phrase, even though I
also thought at first that it was funny and 'on the form' would be more natural.

Given that we have 194 'of the form' and 5 'on the form', I'd suggest that we
just stick to 'of the form' everywhere.

[Lasse Reichstein Nielsen, 2017/08/22 05:32:11]

Agree, and I have probably added all five of them. I'll just fix it all now.

 \begin{code}
    normalFormalParameter : expression
 \end{code}
-is equivalent to one on the form:
+is equivalent to one of the form:

[eernst, 2017/08/21 10:15:20]

Ditto.

 \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  $e_1$ $op$ $e_2$ is equivalent to the method invocation $e_1.op(e_2)$.

[eernst, 2017/08/21 10:15:20]

Can't really see any changes, but we might as well fix the double space.

[Lasse Reichstein Nielsen, 2017/08/22 05:32:11]

I removed a leading space, but yes, fixing double-space too, and wrapping the
code in \code.

 A bitwise expression of the form  \code{\SUPER{} $op$ $e_2$} is equivalent to the method invocation \code{\SUPER{}.op($e_2$)}.

[eernst, 2017/08/21 10:15:20]

Font typo: should be `$op$`. Double space.

[Lasse Reichstein Nielsen, 2017/08/22 05:32:11]

Done.

 
 \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:

[eernst, 2017/08/21 10:15:20]

Delete `where $e_1$ is not a type literal, `: The text ahead makes sense if and
only if it's deleted.

[Lasse Reichstein Nielsen, 2017/08/22 05:32:13]

Done.

 
 \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:

[eernst, 2017/08/21 10:15:20]

Ditto: delete `where $e_1$ is not a type literal, `.

[Lasse Reichstein Nielsen, 2017/08/22 05:32:09]

Done.

 
-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$.

[eernst, 2017/08/21 10:15:21]

Doesn't this eliminate the ability of the static analysis to recognize that `id`
is declared as a static variable/getter/setter, i.e., we can run it but it will
be a compile-time error (or it will be spuriously resolved to a global
declaration)?

I guess we had that problem all along because this piece of text says
`Evaluation of an identifier expression $e$ .. proceeds as follows:` (so it was
always just about the dynamic semantics), but it would be nice to know that the
spec actually ensures that static analysis treats this `id` as a static
variable/getter/setter as well. Do we have that somewhere else?

[Lasse Reichstein Nielsen, 2017/08/22 05:32:12]

I'm not actually sure. I worried about the same thing, and we should look into
it, but I decided, as you also say, that *this* change only affects the runtime
semantics anyway, no matter what it purported to say before.

+\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$.

[eernst, 2017/08/21 10:15:20]

Again, static analysis should also be able to see that some such
inherited-member access expressions will succeed (if we just leave them
unchanged during static analysis they will resolve to something wrong, or they
will be undefined).

[Lasse Reichstein Nielsen, 2017/08/22 05:32:10]

Acknowledged.

 % 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{}
+Execution of an if statement of the form  \code {\IF{} (}$b$\code{)} $s_1$ \code{\ELSE{} } $s_2$ where $s_1$ and $s_2$ are block statements, proceeds as follows:

[eernst, 2017/08/21 10:15:20]

Might as well keep the simpler "all \code" style that we've used in many other
locations: `of the form \code{\IF{} ($b$) $s_1$ \ELSE{}}`.

[Lasse Reichstein Nielsen, 2017/08/22 05:32:10]

Agree. This was moved verbatim from earlier, but let's improve it while we're
here.

+
+\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 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 2365 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.
 
 ----------------------------------------------------------------------