Specify what "is equivalent to" means.

docs/language/dartLangSpec.tex

Index: docs/language/dartLangSpec.tex
diff --git a/docs/language/dartLangSpec.tex b/docs/language/dartLangSpec.tex
index 329de373ca67b08b58277fbe220bf65cd88bddcf..a50bbf761896b12b04b1df261e776b7db6554699 100644
--- a/docs/language/dartLangSpec.tex
+++ b/docs/language/dartLangSpec.tex
@@ -22,6 +22,7 @@
 % 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.
@@ -184,7 +185,7 @@ The specifications of operators often involve statements such as $x$ $op$ $y$ is
 \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.
  }
@@ -203,6 +204,13 @@ References to otherwise unspecified names of program entities (such as classes o
 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}
 
@@ -541,7 +549,7 @@ As a rule, type annotations are ignored in production mode. However, we do
 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$
 
@@ -828,11 +836,11 @@ Optional parameters may be specified and provided with default values.
     .
 \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}
@@ -3962,7 +3970,7 @@ If $e_f$ is a property extraction expression (\ref{propertyExtraction}), then $i
 \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.
@@ -4896,7 +4904,7 @@ Evaluation of an equality expression $ee$ of the form \code{$e_1$ == $e_2$} proc
 \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}
 
 
@@ -4905,7 +4913,7 @@ Evaluation of an equality expression $ee$ of the form \code{\SUPER{} == $e$} pro
 \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:
@@ -4981,8 +4989,8 @@ Bitwise expressions invoke the bitwise operators on objects.
 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.
@@ -5110,7 +5118,7 @@ Unary expressions invoke unary operators on objects.
 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}.
@@ -5315,10 +5323,11 @@ 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$.
@@ -5332,9 +5341,10 @@ 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.
@@ -5403,7 +5413,7 @@ An assignable expression of the form \code{$e_1$[$e_2$]} is evaluated as a metho
 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}
@@ -5504,10 +5514,10 @@ Let $d$ be the innermost declaration in the enclosing lexical scope whose name i
 \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}
 
@@ -5733,10 +5743,10 @@ A {\em variable declaration statement }declares a new local variable.
  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;}.
@@ -5825,21 +5835,13 @@ The {\em if statement} allows for conditional execution of statements.
       \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;
@@ -5849,25 +5851,29 @@ Execution of an if statement of the form  \code {\IF{} (}$b$\code{)}$s_1$ \code{
 
 \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}
@@ -5899,7 +5905,7 @@ The {\em for statement} supports iteration.
 
 
 \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$.
@@ -6410,7 +6416,7 @@ An \ON{}-\CATCH{} clause of the form \code{\CATCH{} ($p_1$, $p_2$) $s$} is equiv
 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$
@@ -6439,7 +6445,7 @@ It is a static warning if $T_i$, $1 \le i \le n$ is a deferred or malformed type
 \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
@@ -6777,7 +6783,7 @@ 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