Added static warning on assignment to final locals; adjusted for-in.

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.
+% - It is a static warning and dynamic error to assign to final local.
 %
 % 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 407 matching lines @@
 \rationale{The lazy semantics are given because we do not want a language where one tends to define expensive initialization computations, causing long application startup times. This is especially crucial for Dart, which must support the coding of  client applications.
 }
 
 \LMHash{}
 A {\em final variable} is a variable whose binding is fixed upon initialization; a final variable $v$ will always refer to the same object after $v$ has been initialized. The declaration of a final variable must  include the modifier \FINAL{}.
 
 \LMHash{}
 It is a static warning if a final instance variable that has been initialized at its point of declaration  is  also initialized in a constructor.
 % It is a static warning if a final instance variable that has been initialized by means of an initializing formal of a constructor is  also initialized elsewhere in the same constructor.
 It is a compile-time error if a local variable $v$ is final and $v$ is not initialized at its point of declaration.
+It is a static warning and a dynamic error to assign to a final local variable.
 
 \commentary{
 
 A library or static variable is guaranteed to have an initializer at its declaration by the grammar.
 
 Attempting to assign to a final variable anywhere except in its declaration or in a constructor header  will cause a runtime error to be thrown as discussed below. The assignment will also give rise to a static warning. Any repeated assignment to a final variable will also lead to a runtime error.
 
 Taken as a whole, the rules ensure that any attempt to execute multiple assignments to a final variable will yield static warnings and repeated assignments will fail dynamically.
 }
 
@@ skipping 5472 matching lines @@
 %   $e$;
 %\}\}
 %}
 
 %If $c$ is empty, it is interpreted as \TRUE{}.
 
 \subsubsection{For-in}
 \LMLabel{for-in}
 
 \LMHash{}
-A for statement of the form \code{ \FOR{} ($finalConstVarOrType?$ id \IN{} $e$) $s$} is equivalent to the following code:
+Let $D$ be derived from \code{finalConstVarOrType?}
+and let $n0$ be an identifier that does not occur anywhere in the program.
+A for statement of the form \code{\FOR{} ($D$ $id$ \IN{} $e$) $s$} is equivalent to the following code:

[Lasse Reichstein Nielsen, 2017/08/18 19:11:58]

THANK you! That "pattern syntax in concrete code" category error deserved to be
fixed!

[eernst, 2017/08/21 14:20:44]

Acknowledged. ;-)

 
 \begin{dartCode}
-var n0 = $e$.iterator;
-\WHILE{} (n0.moveNext()) \{
-   $finalConstVarOrType?$ id = n0.current;
+\VAR{} $n0$ = $e$.iterator;
+\WHILE{} ($n0$.moveNext()) \{
+   $D$ $id$ = $n0$.current;
    $s$
 \}
 \end{dartCode}
-where \code{n0} is an identifier that does not occur anywhere in the program, except that for purposes of static typechecking, it is checked under the assumption that $n0$ is declared to be of type $T$, where $T$ is the static type of $e.iterator$.
+
+For purposes of static typechecking,
+this code is checked under the assumption that $n0$ is declared to be of type $T$,
+where $T$ is the static type of \code{$e$.iterator}.
+
+\commentary{
+It follows that it is a static warning if $D$ is omitted and $id$ is a final variable,

[Lasse Reichstein Nielsen, 2017/08/18 19:11:58]

D is omitted -> D is empty
(maybe?)

[eernst, 2017/08/21 14:20:44]

I thought about that, too. Switched to `empty`, which seems better today.

+and a dynamic error will then occur if the body is executed.
+}
 
 \subsubsection{Asynchronous For-in}
 \LMLabel{asynchronousFor-in}
 
 \LMHash{}
 A for-in statement may be asynchronous. The asynchronous form is designed to iterate over streams. An asynchronous for loop is distinguished by the keyword \AWAIT{} immediately preceding the keyword \FOR.
 
 \LMHash{}
-Execution of a for-in statement, $f$, of the form \code{\AWAIT{} \FOR{} (finalConstVarOrType? $id$ \IN{} $e$) $s$} proceeds as follows:
+Let $D$ be derived from \code{finalConstVarOrType?}.
+Execution of a for-in statement, $f$, of the form
+\code{\AWAIT{} \FOR{} ($D$ $id$ \IN{} $e$) $s$}
+proceeds as follows:
 
 \LMHash{}
 The expression $e$ is evaluated to an object $o$.
 It is a dynamic error if $o$ is not an instance of a class that implements \code{Stream}.
+It is a static warning if $D$ is omitted and $id$ is a final variable,
+and it is then a dynamic error if the body is executed.
 
 \LMHash{}
 The stream associated with the innermost enclosing asynchronous for loop, if any, is paused.
 The stream $o$ is listened to, producing a stream subscription $u$,
 and execution of the asynchronous for-in loop is suspended
 until a stream event is available.
 \commentary{
 This allows other asynchronous events to execute while this loop is waiting for stream events.
 }
 
@@ skipping 2257 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.
 
 ----------------------------------------------------------------------