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..d7f6a58451d2229fced943d760fd6dac8c938c66 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,12 @@ 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 "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}
 
@@ -828,11 +835,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:

[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}
@@ -3962,7 +3969,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 +4903,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 +4912,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,7 +4988,7 @@ 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  $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{
@@ -5110,7 +5117,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}.
@@ -5318,7 +5325,8 @@ 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$.
@@ -5334,7 +5342,8 @@ The static type of such an expression is the static type of \code{$e_1$.$v$}.
 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.
@@ -5403,7 +5412,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 +5513,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$.

[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}
 
@@ -5733,10 +5742,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 +5834,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;
@@ -5851,6 +5852,13 @@ Execution of an if statement of the form  \code {\IF{} (}$b$\code{)}$s_1$ \code{
 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}.
 
@@ -5864,10 +5872,7 @@ If:
 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}