Change how the language specification describes control flow.

docs/language/dartLangSpec.tex

Index: docs/language/dartLangSpec.tex
diff --git a/docs/language/dartLangSpec.tex b/docs/language/dartLangSpec.tex
index 9a6ad52bbfa8c2f749b61e5e606465962dabe99d..c09d4d3900b0d520d6aa3f6cfe05aaf71023718c 100644
--- a/docs/language/dartLangSpec.tex
+++ b/docs/language/dartLangSpec.tex
@@ -163,7 +163,7 @@ Type tests also examine the types in a program explicitly. Nevertheless, in most
 }
 
 \LMHash{}
-In checked mode, assignments are dynamically checked, and certain violations of the type system raise exceptions at run time.
+In checked mode, assignments are dynamically checked, and certain violations of the type system throw exceptions at run time.
 
 \commentary{
 The coexistence between optional typing and reification is based on the following:
@@ -324,12 +324,11 @@ a program that interfaces between the engine and the surrounding computing envir
 {\em Dynamic type errors} are type errors reported in checked mode.
 
 \LMHash{}
-{\em Run-time errors} are exceptions raised during execution. Whenever we say that an exception $ex$ is {\em raised} or {\em thrown}, we mean that a throw expression  (\ref{throw}) of the form: \code{\THROW{} $ex$;} was implicitly evaluated or that a rethrow statement (\ref{rethrow}) of the form \code{\RETHROW} was executed. When we say that {\em a} $C$ {\em is thrown}, where $C$ is a class, we mean that an instance of class $C$ is thrown. When we say that a stream raises an exception, we mean that an exception occurred while computing the value(s) of the stream.
+{\em Run-time errors} are exceptions thrown during execution. Whenever we say that an exception $ex$ is {\em thrown}, it acts like an expression had {\em thrown} (\ref{completion}) with $ex$ as exception object and with a stack trace corresponding to the current system state. When we say that {\em a} $C$ {\em is thrown}, where $C$ is a class, we mean that an instance of class $C$ is thrown.
 
 \LMHash{}
 If an uncaught exception is thrown by a running isolate $A$, $A$ is immediately suspended.
 
-
 \section{Variables}
 \LMLabel{variables}
 
@@ -803,7 +802,7 @@ Examples of external functions might be foreign functions (defined in C, or Java
 }
 
 \LMHash{}
-An external function is connected to its body by an implementation specific mechanism. Attempting to invoke an external function that has not been connected to its body will raise a \code{NoSuchMethodError} or some subclass thereof.
+An external function is connected to its body by an implementation specific mechanism. Attempting to invoke an external function that has not been connected to its body will throw a \code{NoSuchMethodError} or some subclass thereof.
 
 \LMHash{}
 The actual syntax is given in sections \ref{classes} and \ref{librariesAndScripts} below.
@@ -1214,7 +1213,8 @@ Iff no constructor is specified for a class $C$, it implicitly has a default con
 \LMLabel{generativeConstructors}
 
 \LMHash{}
-A {\em generative constructor} consists of a constructor name, a constructor parameter list, and either a redirect clause or an  initializer list and an optional body.
+A {\em generative constructor} is executed to initialize a freshly allocated object.
+It consists of a constructor name, a constructor parameter list, and either a redirect clause or an  initializer list and an optional body.
 
 \begin{grammar}
 {\bf constructorSignature:}
@@ -1286,6 +1286,16 @@ A generative constructor may be {\em redirecting}, in which case its only action
     .
 \end{grammar}
 
+A redirecting generative constructor is executed to initialize an object $o$ as
+follows:
+
+Let $C$ be the class containing the redirecting generative constructor.
+Let $k$ the target generative constructor specified by either \THIS{} (the constructor named $C$) or $\THIS{}.id$ (the constructor named $C.id$).
+Evaluate \code{arguments} to an argument list.
+Then bind the argument list to the formal parameters of $k$ and
+execute $k$ on the fresh object $o$.
+
+
 % Need to specify exactly how executing a redirecting constructor works
 
 
@@ -1326,7 +1336,7 @@ Let $k$ be a generative constructor.  Then $k$ may include at most one  superini
 Each final instance variable $f$ declared in the immediately enclosing class must have an initializer in $k$'s initializer list unless it has already been initialized by one of the following means:
  \begin{itemize}
  \item Initialization at the declaration of $f$.
- \item Initialization by  means of an initializing formal of $k$.
+ \item Initialization by means of an initializing formal of $k$.
  \end{itemize}
 
 or a static warning occurs. It is a compile-time error if $k$'s initializer list contains an initializer for a variable that is not an instance variable declared in the immediately surrounding class.
@@ -1339,43 +1349,67 @@ or a static warning occurs. It is a compile-time error if $k$'s initializer list
  It is a compile-time error if a  generative constructor of class \code{Object} includes a superinitializer.
 
 \LMHash{}
-Execution of a generative constructor $k$ is always done with respect to a set of bindings for its formal parameters and with  \THIS{} bound to a fresh instance $i$ and the type parameters of the immediately enclosing class bound to a set of actual type arguments $V_1, \ldots , V_m$.
+Execution of a generative constructor $k$ to initialize a fresh instance $i$
+is always done with respect to a set of bindings for its formal parameters
+and the type parameters of the immediately enclosing class bound to a set of actual type arguments $V_1, \ldots , V_m$.
 
 \commentary{These bindings are usually determined by the instance creation expression that invoked the constructor (directly or indirectly). However, they may also be determined by a reflective call,.
 }
 
+
 \LMHash{}
 If $k$ is redirecting then its redirect clause has the form
 
 \THIS{}$.g(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$
 
-where $g$ identifies another  generative constructor of the immediately surrounding class. Then execution of $k$ proceeds by evaluating the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$, and then executing $g$ with respect to the bindings resulting from the evaluation of $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ and with  \THIS{} bound to $i$ and the type parameters of the immediately enclosing class bound to $V_1, \ldots , V_m$.
+where $g$ identifies another  generative constructor of the immediately surrounding class. Then execution of $k$ to initialize $i$ proceeds by evaluating the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$, and then executing $g$ to initialize $i$ with respect to the bindings resulting from the evaluation of $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ and with  \THIS{} bound to $i$ and the type parameters of the immediately enclosing class bound to $V_1, \ldots , V_m$.
 
 \LMHash{}
 Otherwise, execution  proceeds as follows:
 
 \LMHash{}
-%First, a fresh instance (\ref{generativeConstructors}) $i$ of the immediately enclosing class is allocated.  Next, the instance variable declarations of the immediately enclosing class are visited in the order they appear in the program text. For each such declaration $d$, if $d$ has the form  \code{$finalConstVarOrType$ $v$ = $e$; } then the instance variable $v$ of $i$ is bound to the value of $e$ (which is necessarily a compile-time constant).
+%First, a fresh instance (\ref{generativeConstructors}) $i$ of the immediately enclosing class is allocated.
+
+The instance variable declarations of the immediately enclosing class are visited in the order they appear in the program text.
+For each such declaration $d$, if $d$ has the form \code{$finalConstVarOrType$ $v$ = $e$; }
+then $e$ is evaluated to an object $o$
+and the instance variable $v$ of $i$ is bound to $o$.
+
 %Next, a
 Any initializing formals declared in $k$'s parameter list are executed in the order they appear in the program text.
 % In fact, this order is unobservable; this could be done any time prior to running the body, since
 % these only effect \THIS{}.
-Then, $k$'s  initializers are executed in the order they appear in the program.
+Then, $k$'s initializers are executed to initialize $i$
+in the order they appear in the program.
+
+\rationale {We could observe the order by side effecting external routines called. So we need to specify the order.}
 
-\rationale {We could observe the order by side  effecting external routines called. So we need to specify the order.}
+Then if any instance variable of $i$ declared by the immediately enclosing class
+is not yet bound to a value,
+it is a dynamic error if such a variable is a \FINAL{} variable,
+otherwise all such variables are initialized with the \NULL{} value.
+
+After this, unless the enclosing class is \code{Object}, the super constructor call implicitly or explicitly specified in $k$'s initializers, is now executed to further initialize $i$, as specified below.
+
+\commentary{
+The super constructor call can be written anywhere in the initializers of $k$, but the actual call always happens after all initializers have been processed.
+It is not equivalent to moving the super call to the end of the initializers
+because the argument expressions may have visible side effects
+which must happen in the order the expressions occur in the program text.
+}
 
 \LMHash{}
-After all the initializers  have completed, the body of $k$ is executed  in a scope where \THIS{} is bound to $i$. Execution of the body begins with execution of the body of the superconstructor  with \THIS{} bound to $i$, the type parameters of the immediately enclosing class bound to a set of actual type arguments $V_1, \ldots , V_m$ and the formal parameters bindings determined by the argument list of the superinitializer of $k$.
+After all superclass constructors have completed, the body of $k$ is executed in a scope where \THIS{} is bound to $i$.
 
 \rationale{
 This process ensures that no uninitialized final field is ever seen by code. Note that \THIS{} is not in scope on the right hand side of an initializer (see \ref{this}) so no instance method can execute during initialization: an instance method cannot be directly invoked, nor can  \THIS{} be passed into any other code being invoked in the initializer.
 }
 
 \LMHash{}
-Execution of an initializer of the form \code{\THIS{}.$v$ = $e$} proceeds as follows:
+Execution of an initializer of the form \code{\THIS{}.$v$ = $e$} to initialize an object $i$ proceeds as follows:
 
 \LMHash{}
-First, the expression $e$ is evaluated to an object $o$. Then, the instance variable $v$ of the object denoted by \THIS{} is bound to $o$, unless $v$ is a final variable that has already been initialized, in which case a runtime error occurs. In checked mode, it is a dynamic type error if $o$ is not \NULL{} and the interface of the class of $o$ is not a subtype of the actual type of the field $v$.
+First, the expression $e$ is evaluated to an object $o$. Then, the instance variable $v$ of $i$ is bound to $o$, unless $v$ is a final variable that has already been initialized, in which case a runtime error occurs. In checked mode, it is a dynamic type error if $o$ is not \NULL{} and the interface of the class of $o$ is not a subtype of the actual type of the field $v$.
 
 \LMHash{}
 An initializer of the form \code{$v$ = $e$} is equivalent to an initializer of the form  \code{\THIS{}.$v$ = $e$}.
@@ -1391,12 +1425,13 @@ proceeds as follows:
 
 \LMHash{}
 First, the argument list $(a_1, \ldots, a_n, x_{n+1}: a_{n+1}, \ldots, x_{n+k}: a_{n+k})$ is evaluated.
+This evaluated argument list is remembered until after the entire initializer list has been evaluated, at which point the constructor is executed as follows:
 
 \LMHash{}
 Let $C$ be the class in which the superinitializer appears and let $S$ be the superclass of $C$.  If $S$ is generic (\ref{generics}), let $U_1, , \ldots, U_m$ be the actual type arguments passed to $S$ in the superclass clause of $C$.
 
 \LMHash{}
-Then, the initializer list of the constructor $S$ (respectively $S.id$) is executed with respect to the bindings that resulted from the evaluation of the argument list,  with \THIS{} bound to the current binding of \THIS{}, and  the type parameters (if any) of class $S$ bound to the current bindings of $U_1, , \ldots, U_m$.
+The generative constructor $S$ (respectively $S.id$) of $S$ is executed to initialize $i$ with respect to the bindings that resulted from the evaluation of the argument list, and the type parameters (if any) of class $S$ bound to the current bindings of $U_1, , \ldots, U_m$.
 
 \LMHash{}
 It is a compile-time error if class $S$ does not declare a generative constructor named $S$ (respectively $S.id$).
@@ -1429,7 +1464,6 @@ In checked mode, it is a dynamic type error if a factory returns a non-null obje
 
 \rationale{Factories address classic weaknesses associated with constructors in other languages.
 Factories can produce instances that are not freshly allocated: they can come from a cache. Likewise, factories can return instances of different classes.
-
 }
 
 \paragraph{Redirecting Factory Constructors}
@@ -2337,7 +2371,18 @@ The constant expression given in an annotation  is type checked and evaluated in
 \LMLabel{expressions}
 
 \LMHash{}
-An {\em expression} is a fragment of Dart code that can be evaluated at run time to yield a {\em value}, which is always an object. Every expression has an associated static type (\ref{staticTypes}). Every value has an associated dynamic type (\ref{dynamicTypeSystem}).
+\LMLabel{evaluation}
+An {\em expression} is a fragment of Dart code that can be evaluated at run time.
+Evaluating an expression either {\em produces a value} (an object), or it {\em throws} an exception object and an associated stack trace.
+In the former case, we also say that the expression {\em evaluates to a value}.
+
+Every expression has an associated static type (\ref{staticTypes}).
+Every value has an associated dynamic type (\ref{dynamicTypeSystem}).
+
+If evaluation of an expression is defined in terms of evaluation of another expression,
+and the evaluation of the other expression throws an exception and a stack trace,
+if nothing else is stated, the evaluation of the first expression stops
+at that point and throws the same exception object and stack trace.
 
 
 \begin{grammar}
@@ -2458,13 +2503,13 @@ A constant expression is one of the following:
 % designed so constants do not depend on check diode being on or not.
 
 \LMHash{}
-It is a compile-time error if an expression is required to be a constant expression but its evaluation  would raise an exception.
+It is a compile-time error if an expression is required to be a constant expression but its evaluation would throw an exception.
 
 % so, checked mode? analyzers? editor/development compilers?
 \commentary{
 Note that there is no requirement that every constant expression evaluate correctly. Only when a constant expression is required (e.g., to initialize a constant variable, or as a default value of a formal parameter, or as metadata) do we insist that a constant expression actually be evaluated successfully at compile time.
 
-The above is not dependent on program control-flow. The mere presence of a required compile time constant whose evaluation would fail within a program is an error.  This also holds recursively: since compound constants are composed out of constants, if any subpart of a constant  would raise an exception when evaluated, that is an error.
+The above is not dependent on program control-flow. The mere presence of a required compile time constant whose evaluation would fail within a program is an error.  This also holds recursively: since compound constants are composed out of constants, if any subpart of a constant would throw an exception when evaluated, that is an error.
 
 On the other hand, since implementations are free to compile code late, some compile-time errors may manifest quite late.
 }
@@ -2541,7 +2586,7 @@ As an example, consider:
 \LMLabel{null}
 
 \LMHash{}
-The reserved word \NULL{} denotes the {\em null object}.
+The reserved word \NULL{} evaluates to the {\em null object}.
 %\Q{Any methods, such as \code{isNull}?}
 
 \begin{grammar}
@@ -2552,7 +2597,7 @@ The reserved word \NULL{} denotes the {\em null object}.
 
 \LMHash{}
 The null object is the sole instance of the built-in class \code{Null}. Attempting to instantiate \code{Null} causes a run-time error. It is a compile-time error for a class to attempt to extend, mix in or implement \code{Null}.
-Invoking a method on \NULL{}  yields a \code{NoSuchMethodError} unless the method is explicitly implemented by class \code{Null}.
+The \code{Null} class declares no methods except those also declared by \code{Object}.
 
 \LMHash{}
 The static type of \NULL{} is $\bot$.
@@ -2591,7 +2636,17 @@ A {\em numeric literal} is either a decimal or hexadecimal integer of arbitrary
  \end{grammar}
 
 \LMHash{}
-If a numeric literal begins with the prefix `0x' or `0X', it denotes the hexadecimal integer represented by the part of the literal following `0x' (respectively `0X'). Otherwise, if the numeric literal contains only decimal digits, it denotes a decimal integer.  Otherwise, the numeric literal contains either a decimal point or an exponent part and it denotes a 64 bit double precision floating point number as specified by the IEEE 754 standard.
+If a numeric literal begins with the prefix `0x' or `0X',
+it denotes the hexadecimal integer numeral
+represented by the part of the literal following `0x' (respectively `0X').
+Otherwise, if the numeric literal contains only decimal digits,
+it denotes a decimal integer numeral.
+In either case the literal evaluates to an instance of the class \code{int}
+with the integer value represented by that numeral.
+Otherwise, the numeric literal contains either a decimal point or an exponent part
+and it evaluates to a an instance of the `double` class
+representing a 64 bit double precision floating point number
+as specified by the IEEE 754 standard.
 
 \LMHash{}
 In principle, the range of integers supported by a Dart implementations is unlimited. In practice, it is limited by available memory. Implementations may also be limited by other considerations.
@@ -2604,17 +2659,18 @@ For example, implementations may choose to limit the range to facilitate efficie
 It is a compile-time error for a class to attempt to extend, mix in or implement \code{int}. It is a compile-time error for a class to attempt to extend, mix in or implement \code{double}. It is a compile-time error for any type other than the types \code{int} and \code{double} to attempt to extend, mix in or implement \code{num}.
 
 \LMHash{}
-An {\em integer literal} is either a hexadecimal integer literal or a  decimal integer literal. Invoking the getter \code{runtimeType} on an integer literal returns the \code{Type} object that is the value of the expression \code{int}. The static type of an integer literal is \code{int}.
+An {\em integer literal} is either a hexadecimal integer literal or a  decimal integer literal.
+The static type of an integer literal is \code{int}.
 
 \LMHash{}
-A {\em literal double} is a numeric literal that is not an integer literal. Invoking the getter \code{runtimeType} on a literal double returns the \code{Type} object that is the value of the expression \code{double}.
-The static type of a literal double is \code{double}.
+A {\em literal double} is a numeric literal that is not an integer literal. The static type of a literal double is \code{double}.
 
 \subsection{Booleans}
 \LMLabel{booleans}
 
 \LMHash{}
-The reserved words \TRUE{} and \FALSE{} denote objects that represent the boolean values true and false respectively. They are the {\em boolean literals}.
+The reserved words \TRUE{} and \FALSE{} evaluate to objects {\em true} and {\em false} that represent the boolean values true and false respectively.
+They are the {\em boolean literals}.
 
 \begin{grammar}
 {\bf booleanLiteral:}\TRUE{};
@@ -2623,14 +2679,12 @@ The reserved words \TRUE{} and \FALSE{} denote objects that represent the boolea
 \end{grammar}
 
 \LMHash{}
-Both  \TRUE{} and \FALSE{} implement the built-in class \code{bool}.  It is a compile-time error for a class to attempt to extend, mix in or implement\code{ bool}.
-
-\commentary{
-It follows that the two boolean literals are the only two instances of \code{bool}.
-}
+Both {\em true} and {\em false} are instances of the built-in class \code{bool},
+and there are no other objects that implement \code{bool}.
+It is a compile-time error for a class to attempt to extend, mix in or implement\code{ bool}.
 
 \LMHash{}
-Invoking the getter \code{runtimeType} on a boolean literal returns the \code{Type} object that is the value of the expression \code{bool}. The static type of a boolean literal is \code{bool}.
+Invoking the getter \code{runtimeType} on a boolean value returns the \code{Type} object that is the value of the expression \code{bool}. The static type of a boolean literal is \code{bool}.
 
 \subsubsection{Boolean Conversion}
 \LMLabel{booleanConversion}
@@ -2831,7 +2885,8 @@ It is a compile-time error if a non-raw string literal contains a character sequ
  \end{grammar}
 
 \LMHash{}
-All string literals implement the built-in class \code{String}. It is a compile-time error for a class to attempt to extend, mix in or implement \code{String}. Invoking the getter \code{runtimeType} on a string literal returns the \code{Type} object that is the value of the expression \code{String}. The static type of a string literal is \code{String}.
+All string literals evaluates to instances of the built-in class \code{String}. It is a compile-time error for a class to attempt to extend, mix in or implement \code{String}.
+The static type of a string literal is \code{String}.
 
 \subsubsection{String Interpolation}
 \LMLabel{stringInterpolation}
@@ -2856,7 +2911,16 @@ An unescaped \$ character in a string signifies the beginning of an interpolated
 \end{itemize}
 
 \LMHash{}
-The form \code{\$id} is equivalent to the form \code{\$\{id\}}.  An interpolated string \code{`$s_1$\$\{$e$\}$s_2$'}  is equivalent to the concatenation of the  strings \code{`$s_1$'},  \code{$e$.toString()} and  \code{$`s_2$'}. Likewise an interpolated string \code{``$s_1$\$\{e\}$s_2$''} is equivalent to the concatenation of the strings \code{``$s_1$''}, \code{$e$.toString()} and  \code{``$s_2$''}.
+The form \code{\$id} is equivalent to the form \code{\$\{id\}}.
+An interpolated string, $s$, with content `\code{$s_0$\$\{$e_1$\}$s_1\ldots{}s_{n-1}\$\{e_n\}s_{n}$}' (where any of $s_0 \ldots{} s_n$ can be empty)
+is evaluated by evaluating each expression $e_i$ ($1 \le i \le n$) in to a string $r_i$ in the order they occur in the source text, as follows:
+\begin{itemize}
+\item{} Evaluate $e_i$ to an object $o_i$.
+\item{} Invoke the \code{toString} method on $o_i$ with no arguments, and let
+  $r_i$ be the returned value.
+\item{} If $r_i$ is not an instance of the built-in type \code{String}, throw an \code{Error}.
+\end{itemize}
+Finally, the result of the evaluation of $s$ is the concatenation of the strings $s_0$, $r_1$, \ldots{}, $r_n$, and $s_n$.
 
 \subsection{Symbols}
 \LMLabel{symbols}
@@ -2920,7 +2984,7 @@ Let $list_1 =$ \CONST{} $<V>[e_{11} \ldots e_{1n}]$ and $list_2 =$  \CONST{} $<U
 A run-time list literal $<E>[e_1 \ldots e_n]$  is evaluated as follows:
 \begin{itemize}
 \item
-First, the expressions $e_1 \ldots e_n$ are evaluated in order they appear in the program, yielding objects $o_1 \ldots o_n$.
+First, the expressions $e_1 \ldots e_n$ are evaluated in order they appear in the program, producing objects $o_1 \ldots o_n$.
 \item A fresh instance  (\ref{generativeConstructors}) $a$, of size $n$,  whose class implements the built-in class $List<E>$ is allocated.
 \item
 The operator \code{[]=} is invoked on $a$ with  first  argument $i$ and second argument
@@ -2996,12 +3060,13 @@ Let $map_1 =$ \CONST{}$ <K, V>\{k_{11}:e_{11} \ldots k_{1n} :e_{1n}\}$ and  $map
 A runtime map literal $<K, V>\{k_1:e_1\ldots k_n :e_n\}$  is evaluated as follows:
 \begin{itemize}
 \item
-First, the expression $k_i$ is evaluated yielding object $u_i$, the $e_i$ is vaulted yielding object $o_i$, for $i \in 1..n$ in left to right order, yielding objects $u_1, o_1\ldots u_n, o_n$.
-\item  A fresh instance (\ref{generativeConstructors}) $m$ whose class implements the built-in class
-
- $Map<K, V>$ is allocated.
+For each $i \in 1..n$ in numeric order,
+first the expression $k_i$ is evaluated producing object $u_i$,
+and then $e_i$ is evaluated producing object $o_i$.
+This produces all the objects $u_1, o_1\ldots u_n, o_n$.
+\item  A fresh instance (\ref{generativeConstructors}) $m$ whose class implements the built-in class $Map<K, V>$ is allocated.
 \item
-The operator \code{[]=} is invoked on $m$ with  first  argument $u_i$ and second argument $o_i,  i \in 1.. n$.
+The operator \code{[]=} is invoked on $m$ with  first  argument $u_i$ and second argument $o_i$ for each $i \in 1.. n$.
 \item
 The result of the evaluation is $m$.
 \end{itemize}
@@ -3031,7 +3096,7 @@ The static type of a map literal of the form  \CONST{}$ <K, V>\{k_1:e_1\ldots k_
 \LMLabel{throw}
 
 \LMHash{}
-The {\em throw expression}  is used to raise an exception.
+The {\em throw expression}  is used to throw an exception.
 
  \begin{grammar}
 {\bf throwExpression:}
@@ -3045,45 +3110,28 @@ The {\em throw expression}  is used to raise an exception.
  \end{grammar}
 
 \LMHash{}
- The {\em current exception} is the last exception raised and not subsequently caught at a given moment during runtime.
-
-\LMHash{}
- Evaluation of a throw expression of the form  \code{\THROW{} $e$;} proceeds as follows:
+Evaluation of a throw expression of the form  \code{\THROW{} $e$;} proceeds as follows:
 
 \LMHash{}
-The expression $e$ is evaluated yielding a value $v$.
+The expression $e$ is evaluated producing a value $v$.
 
 \commentary{
 There is no requirement that the expression $e$ evaluate to a special kind of exception or error object.
 }
 
 \LMHash{}
-If $e$ evaluates to \NULL{} (\ref{null}), then a \code{NullThrownError} is thrown. Otherwise the current exception is set to $v$ and the current return value (\ref{return}) becomes undefined.
-
-\rationale{The current exception and the current return value must never be simultaneously defined, as they represent mutually exclusive options for exiting the current function.
-}
-
-\LMHash{}
-Let $f$ be the immediately enclosing function.
+If $v$ is the null value (\ref{null}), then a \code{NullThrownError} is thrown. Otherwise let $t$ be a stack trace corresponding to the current execution state, and the \THROW{} statement {\em throws} (\ref{completion}) with $v$ as exception object and $t$ as stack trace.
 
 \LMHash{}
-If $f$ is synchronous (\ref{functions}), control is transferred to the nearest dynamically enclosing exception handler.
+If $v$ is an instance of class \code{Error} or a subclass thereof,
+and it is the first time that \code{Error} object is thrown,
+the stack trace $t$ is stored on $v$ so that it will be returned by the $v$'s \code{stackTrace} getter
 
 \commentary{
-If $f$ is marked \SYNC* then a dynamically enclosing exception handler encloses the call to \code{moveNext()} that initiated the evaluation of the throw expression.
-}
-
-\LMHash{}
-If $f$ is asynchronous  then if there is a dynamically enclosing exception handler $h$  (\ref{try}) introduced by the current activation, control is transferred to $h$, otherwise $f$  terminates.
-
-\rationale{
-The rules for where a thrown exception will be handled must necessarily differ between the synchronous and asynchronous cases. Asynchronous functions cannot transfer control to an exception handler defined outside themselves.  Asynchronous generators post exceptions to their stream. Other asynchronous functions report exceptions via their future.
+If the same \code{Error} object is thrown more than once, its \code{stackTrace} getter will return the stack trace from the {\em first} time it was thrown.
 }
 
 \LMHash{}
-If the object being thrown is an instance of class \code{Error} or a subclass thereof, its \code{stackTrace} getter will return the stack trace current at the point where the object was first thrown.
-
-\LMHash{}
 The static type of a throw expression is $\bot$.
 
 
@@ -3345,7 +3393,7 @@ Then, if $q$ is a non-factory constructor of an abstract class then an \code{Abs
 
 \LMHash{}
 If $T$  is malformed or if $T$ is a type variable a dynamic error occurs. In checked mode, if $T$ or any of its superclasses is malbounded a dynamic error occurs.
- Otherwise, if $q$ is not defined or not accessible, a \code{NoSuchMethodError} is thrown.  If $q$ has  less than $n$ positional parameters or more than $n$ required parameters, or if $q$ lacks any of the keyword parameters $\{ x_{n+1}, \ldots, x_{n+k}\}$ a \code{NoSuchMethodError} is thrown.
+Otherwise, if $q$ is not defined or not accessible, a \code{NoSuchMethodError} is thrown.  If $q$ has fewer than $n$ positional parameters or more than $n$ required parameters, or if $q$ lacks any of the keyword parameters $\{ x_{n+1}, \ldots, x_{n+k}\}$ a \code{NoSuchMethodError} is thrown.
 
 \LMHash{}
 Otherwise, if $q$ is a generative constructor (\ref{generativeConstructors}), then:
@@ -3353,14 +3401,10 @@ Otherwise, if $q$ is a generative constructor (\ref{generativeConstructors}), th
 \commentary{Note that it this point we are assured that the number of actual type arguments match the number of formal type parameters.}
 
 \LMHash{}
-A fresh instance (\ref{generativeConstructors}), $i$,  of class $R$ is allocated. For each instance variable $f$ of $i$,  if the variable declaration of $f$ has an initializer expression $e_f$, then $e_f$ is evaluated, with the type parameters (if any) of $R$ bound to the actual type arguments $V_1, \ldots, V_l$, to an object $o_f$ and $f$ is bound to $o_f$. Otherwise $f$ is bound to \NULL{}.
-
-\commentary{
-Observe that \THIS{} is not in scope in $e_f$. Hence, the initialization cannot depend on other properties of the object being instantiated.
-}
+A fresh instance (\ref{generativeConstructors}), $i$, of class $R$ is allocated.
+Then $q$ is executed to initialize $i$ with its formal parameters bound to the evaluated argument list and, if $R$ is a generic class, with its type parameters bound to $V_1 \ldots V_m$.
 
-\LMHash{}
-Next,  $q$ is executed  with \THIS{} bound to $i$,  the type parameters (if any) of $R$ bound to the actual type arguments $V_1, \ldots, V_l$ and the formal parameter bindings that resulted from the evaluation of the argument list. The result of the evaluation of $e$ is $i$.
+If execution of $q$ completes normally, $e$ evaluates to $i$.
 
 \LMHash{}
 Otherwise, $q$ is a factory constructor (\ref{factories}). Then:
@@ -3368,11 +3412,16 @@ Otherwise, $q$ is a factory constructor (\ref{factories}). Then:
 \LMHash{}
 If $q$ is a redirecting factory constructor of the form $T(p_1, \ldots, p_{n+k}) = c;$ or of the form  $T.id(p_1, \ldots, p_{n+k}) = c;$ then the result of the evaluation of $e$ is equivalent to evaluating the expression
 
-$[V_1,  \ldots, V_m/T_1,  \ldots, T_m]($\code{\NEW{} $c(a_1, \ldots, a_n, x_{n+1}: a_{n+1}, \ldots, x_{n+k}: a_{n+k}))$}.  If evaluation of $q$ causes $q$ to be re-evaluated cyclically, a runtime error occurs.
+$[V_1,  \ldots, V_m/T_1,  \ldots, T_m]($\code{\NEW{} $c(a_1, \ldots, a_n, x_{n+1}: a_{n+1}, \ldots, x_{n+k}: a_{n+k}))$}.  If evaluation of $q$ causes $q$ to be re-evaluated cyclically, with only factory constructor redirections in-between, a runtime error occurs.
+% Used to not have the "in-between" clause, which would disallow a factory constructor redirecting to another constructor which conditionally calls the original factory constructor again with different arguments.
 
 
 \LMHash{}
-Otherwise, the body of $q$ is executed with respect to the bindings that resulted from the evaluation of the argument list and the type parameters (if any) of $q$ bound to the actual type arguments $V_1, \ldots, V_l$ resulting in an object $i$. The result of the evaluation of $e$ is $i$.
+Otherwise, the body of $q$ is executed with respect to the bindings that resulted from the evaluation of the argument list and the type parameters (if any) of $q$ bound to the actual type arguments $V_1, \ldots, V_l$.
+If this execution {\em returns a value} (\ref{completion}),
+let $i$ be the returned value.
+If the execution {\em completes normally} or {\em returns with no value}, let $i$ be \code{null}.
+The result of the evaluation of $e$ is $i$.
 
 \LMHash{}
 It is a static warning if $q$ is a constructor of an abstract class and $q$ is not a factory constructor.
@@ -3536,37 +3585,24 @@ As discussed in section \ref{errorsAndWarnings}, the handling of a suspended iso
 Function invocation occurs in the following cases: when a function expression  (\ref{functionExpressions}) is invoked (\ref{functionExpressionInvocation}), when a method (\ref{methodInvocation}), getter (\ref{topLevelGetterInvocation}, \ref{propertyExtraction}) or setter (\ref{assignment}) is invoked or when a constructor is invoked (either via instance creation (\ref{instanceCreation}), constructor redirection (\ref{redirectingConstructors}) or super initialization). The various kinds of function invocation differ as to how the function to be invoked, $f$,  is determined, as well as whether \THIS{} (\ref{this}) is bound. Once $f$ has been determined, the formal parameters of $f$ are bound to corresponding actual arguments. When the body of $f$ is executed it will be executed with the aforementioned bindings.
 
 \LMHash{}
-If $f$ is marked \ASYNC{} (\ref{functions}), then a fresh instance (\ref{generativeConstructors}) $o$ implementing the built-in class \code{Future} is associated with the invocation and immediately returned to the caller. The body of $f$ is scheduled for execution at some future time. The future $o$ will complete when $f$ terminates. The value used to complete $o$ is the current return value (\ref{return}), if it is defined, and the current exception (\ref{throw}) otherwise.
-
-\LMHash{}
-If $f$ is marked \ASYNC* (\ref{functions}), then a fresh instance $s$ implementing the built-in class \code{Stream} is associated with the invocation and immediately returned. When $s$ is listened to, execution of the body of $f$ will begin.  When $f$ terminates:
-\begin{itemize}
-\item If the current return value is defined then, if $s$ has been canceled then its cancellation future is completed with \NULL{} (\ref{null}).
-\item If the current exception $x$ is defined:
-  \begin{itemize}
-  \item $x$ is added to $s$.
-  \item If $s$ has been canceled then its cancellation future is completed with $x$ as an error.
-  \end{itemize}
-\item $s$ is closed.
-\end{itemize}
-
-\rationale{
-When an asynchronous generator's stream has been canceled, cleanup will occur in the \FINALLY{} clauses (\ref{try}) inside the generator. We choose to direct any exceptions that occur at this time to the cancellation future rather than have them be lost.
-}
-
-\LMHash{}
-If $f$ is asynchronous then, when $f$ terminates, any open stream subscriptions associated with any asynchronous for loops  (\ref{asynchronousFor-in}) or yield-each statements  (\ref{yieldEach}) executing within $f$ are canceled, in the order of their nesting, innermost first.
+If $f$ is synchronous and is not a generator (\ref{functions}) then execution of the body of $f$ begins immediately.
+If that execution {\em returns} a value, $v$, (\ref{completion}), the invocation evaluates to $v$.
+If it {\em completes normally} or {\em returns without a value}, the invocation evaluates to \code{null} (\ref{null}).
+If it {\em throws}, the invocation throws the same exception object and stack trace.
 
-\rationale{Such streams may be left open by for loops that were escaped when an exception was thrown within them for example.
+\commentary{
+A function body can never complete by {\em breaking} or {\em continuing}
+because any \BREAK{} or \CONTINUE{} statement must occur inside a statement
+which will handle the \BREAK{} or \CONTINUE{},
+either by declaring the same label, if the \BREAK{} or \CONTINUE{} has a label,
+or merely by being a loop or \SWITCH{} statement.
+This means that a function body can only either {\em complete normally}, {\em throw}, or {\em return} a value. Completing normally is treated the same as returning \code{null}, so a function call expression can always propagate the behavior of the called function's body.
 }
 
-%\LMHash{}
-%When a stream is canceled, the implementation must wait for the cancelation future returned by \cd{cancell()} to complete before proceeding.
 
 \LMHash{}
 If $f$ is marked \SYNC* (\ref{functions}), then a fresh instance $i$ implementing the built-in class \code{Iterable} is associated with the invocation and immediately returned.
 
-
 \commentary{
 A Dart implementation will need to provide a specific implementation of \code{Iterable} that will be returned by \SYNC* methods. A typical strategy would be to produce an instance of a subclass of class \code{IterableBase} defined in \code{dart:core}. The only method that needs to be added by the Dart implementation in that case is \code{iterator}.
 }
@@ -3579,7 +3615,11 @@ The contract explicitly mentions a number of situations where certain iterables
 }
 
 \LMHash{}
-When iteration over the iterable is started, by getting an iterator $j$ from the iterable and calling \code{moveNext()}, execution of the body of $f$ will begin. When $f$ terminates, $j$ is positioned after its last element, so that its current value is \NULL{} and the current call to \code{moveNext()} on $j$ returns false, as will all further calls.
+When iteration over the iterable is started, by getting an iterator $j$ from the iterable and calling \code{moveNext()}, execution of the body of $f$ will begin. When execution of the body of $f$ completes (\ref{completion},
+\begin{itemize}
+\item If it {\em returns} or {\em completes normally}, $j$ is positioned after its last element, so that its current value is \code{null} and the current call to \code{moveNext()} on $j$ returns false, as must all further calls.
+\item If it {\em throws} exception $e$ and stack trace $t$ then the current value of $j$ is \code{null} and the current call to \code{moveNext()} throws $e$ and $t$ as well. Further calls to \code{moveNext()} must return false.
+\end{itemize}
 
 Each iterator starts a separate computation. If the \SYNC* function is impure, the sequence of values yielded by each iterator may differ.
 
@@ -3598,21 +3638,31 @@ Two executions of an iterator interact only via state outside the function.
 }
 % The alternative would be to cache the results of an iterator in the iterable, and check the cache at each \YIELD{}.  This would have strange issues as well. The yielded value might differ from the expression in the yield. And it is a potential memory leak as the cache is kept alive by any iterator.
 
-
 \LMHash{}
-If $f$ is synchronous and is not a generator (\ref{functions}) then execution of the body of $f$ begins immediately.  When $f$ terminates the current return value is returned to the caller.
-
+If $f$ is marked \ASYNC{} (\ref{functions}), then a fresh instance (\ref{generativeConstructors}) $o$ implementing the built-in class \code{Future} is associated with the invocation and immediately returned to the caller. The body of $f$ is scheduled for execution at some future time. The future $o$ will be completed when execution of the body of $f$ completes (\ref{completion}). If it {\em returns} a value, $o$ is completed with that value, if it {\em completes normally} or {\em returns with no value}, $o$ is completed with the value \code{null}, and if it completes by {\em throwing} an exception $e$ and stack trace $t$, $o$ is completed with the error $e$ and stack trace $t$.
 
 \LMHash{}
-Execution of $f$ terminates when the first of the following occurs:
+If $f$ is marked \ASYNC* (\ref{functions}), then a fresh instance $s$ implementing the built-in class \code{Stream} is associated with the invocation and immediately returned. When $s$ is listened to, execution of the body of $f$ will begin.
+When execution of the body of $f$ completes:
 \begin{itemize}
-\item An exception is thrown and not caught within the current function activation.
-\item A return statement (\ref{return}) immediately nested in the body of $f$ is executed and not intercepted in a \FINALLY{} (\ref{try}) clause.
-\item The last statement of the body completes execution.
+\item If it {\em completes normally} or {\em returns with no value}, then if $s$ has been canceled then its cancellation future is completed with \code{null} (\ref{null}).
+\item If it {\em throws} with exception $e$ and stack trace $t$:
+  \begin{itemize}
+  \item If $s$ has been canceled then its cancellation future is completed with error $e$ and stack trace $t$.
+  \item otherwise the error $e$ and stack trace $t$ are emitted by $s$.
+  \end{itemize}
+\item $s$ is closed.
 \end{itemize}
+\commentary{
+The body of an asynchronous generator function cannot {\em break}, {\em continue} or {\em return a value}. The first two are only allowed in contexts that will handle the break or continue, and return statements with an expression are not allowed in generator functions.
+}
 
+\rationale{
+When an asynchronous generator's stream has been canceled, cleanup will occur in the \FINALLY{} clauses (\ref{try}) inside the generator. We choose to direct any exceptions that occur at this time to the cancellation future rather than have them be lost.
+}
 
-
+%\LMHash{}
+%When a stream is canceled, the implementation must wait for the cancelation future returned by \cd{cancell()} to complete before proceeding.
 
 \subsubsection{ Actual Argument List Evaluation}
 \LMLabel{actualArguments}
@@ -3647,7 +3697,7 @@ $(a_1, \ldots, a_m, q_1: a_{m+1}, \ldots, q_l: a_{m+l})$
 proceeds as follows:
 
 \LMHash{}
-The arguments $a_1, \ldots, a_{m+l}$ are evaluated in the order they appear in the program, yielding objects $o_1, \ldots, o_{m+l}$.
+The arguments $a_1, \ldots, a_{m+l}$ are evaluated in the order they appear in the program, producing objects $o_1, \ldots, o_{m+l}$.
 
 \commentary{Simply stated, an argument list consisting of $m$ positional arguments and $l$ named arguments is evaluated from left to right.
 }
@@ -3840,7 +3890,7 @@ $o.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$
 proceeds as follows:
 
 \LMHash{}
-First, the expression $o$ is evaluated to a value $v_o$. Next, the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated yielding actual argument objects $o_1, \ldots , o_{n+k}$. Let $f$ be the result of looking up (\ref{methodLookup}) method $m$  in $v_o$ with respect to the current library $L$.
+First, the expression $o$ is evaluated to a value $v_o$. Next, the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated producing actual argument objects $o_1, \ldots , o_{n+k}$. Let $f$ be the result of looking up (\ref{methodLookup}) method $m$  in $v_o$ with respect to the current library $L$.
 
 \LMHash{}
 Let $p_1 \ldots p_h$ be the required parameters of $f$,  let $p_1 \ldots p_m$ be the positional parameters of $f$ and let $p_{h+1}, \ldots, p_{h+l}$ be the optional parameters declared by $f$.
@@ -3949,7 +3999,7 @@ $\SUPER{}.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
 Evaluation of $i$ proceeds as follows:
 
 \LMHash{}
-First, the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated  yielding actual argument objects $o_1, \ldots , o_{n+k}$. Let $g$ be the method currently executing, and let $C$ be the class in which $g$ was looked up (\ref{methodLookup}). Let $S_{dynamic}$ be the superclass of $C$, and let $f$ be the result of looking up method (\ref{methodLookup})  $m$ in $S_{dynamic}$  with respect to the current library $L$.
+First, the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated producing actual argument objects $o_1, \ldots , o_{n+k}$. Let $g$ be the method currently executing, and let $C$ be the class in which $g$ was looked up (\ref{methodLookup}). Let $S_{dynamic}$ be the superclass of $C$, and let $f$ be the result of looking up method (\ref{methodLookup})  $m$ in $S_{dynamic}$  with respect to the current library $L$.
 Let $p_1 \ldots p_h$ be the required parameters of $f$,  let $p_1 \ldots p_m$ be the positional parameters of $f$ and let $p_{h+1}, \ldots, p_{h+l}$ be the optional parameters declared by $f$.
 
 \LMHash{}
@@ -4719,10 +4769,10 @@ The logical boolean expressions combine boolean objects using the boolean conjun
 A {\em logical boolean expression} is either an equality expression (\ref{equality}), or an invocation of a logical boolean operator on an expression $e_1$ with argument $e_2$.
 
 \LMHash{}
-Evaluation of a logical boolean expression $b$ of the form $e_1 || e_2$ causes the evaluation of $e_1$ which is then  subjected to boolean conversion, yielding an object $o_1$; if $o_1$ is \TRUE, the result of evaluating $b$ is \TRUE, otherwise $e_2$ is evaluated to an object $o_2$, which is then subjected to boolean conversion (\ref{booleanConversion}) producing an object $r$, which is the value of $b$.
+Evaluation of a logical boolean expression $b$ of the form $e_1 || e_2$ causes the evaluation of $e_1$ which is then  subjected to boolean conversion, producing an object $o_1$; if $o_1$ is \TRUE, the result of evaluating $b$ is \TRUE, otherwise $e_2$ is evaluated to an object $o_2$, which is then subjected to boolean conversion (\ref{booleanConversion}) producing an object $r$, which is the value of $b$.
 
 \LMHash{}
-Evaluation of a logical boolean expression $b$ of the form $e_1 \&\& e_2$ causes the evaluation of $e_1$ which is then subjected to boolean conversion, yielding an object $o_1$; if $o_1$ is not  \TRUE, the result of evaluating $b$ is \FALSE, otherwise $e_2$ is evaluated to an object $o_2$, which is then subjected to boolean conversion producing an object $r$, which is the value of $b$.
+Evaluation of a logical boolean expression $b$ of the form $e_1 \&\& e_2$ causes the evaluation of $e_1$ which is then subjected to boolean conversion, producing an object $o_1$; if $o_1$ is not  \TRUE, the result of evaluating $b$ is \FALSE, otherwise $e_2$ is evaluated to an object $o_2$, which is then subjected to boolean conversion producing an object $r$, which is the value of $b$.
 
 \LMHash{}
 A logical boolean expression $b$ of the form $e_1 \&\& e_2$ shows that a variable $v$ has type
@@ -5009,18 +5059,24 @@ An {\em await expression} allows code to yield control until an asynchronous ope
 
 \LMHash{}
 Evaluation of an await expression $a$ of the form \AWAIT{} $e$ proceeds as follows:
-First, the expression $e$ is evaluated. Next:
+First, the expression $e$ is evaluated to an object $o$. Next:
 
 \LMHash{}
-If $e$ raises an exception $x$, then an instance $f$ of class \code{Future} is allocated and later completed with $x$. Otherwise, if $e$ evaluates to an object $o$ that is not an instance of \code{Future}, then let $f$ be the result of calling \code{Future.value()} with $o$ as its argument; otherwise let $f$ be the result of evaluating $e$.
+% NOTICE: Removed the requirement that an error thrown by $e$ is caught in a
+% future. There is no reason $var x = e; await x;$ and $await e$ should behave
+% differently, and no implementation actually implemented it.
+If $o$ is not an instance of \code{Future}, then let $f$ be the result of creating a new object using the constructor \code{Future.value()} with $o$ as its argument; otherwise let $f$ be $o$.
 
 \LMHash{}
-Next,  execution of the function $m$ immediately enclosing $a$ is suspended until after $f$ completes. The stream associated with the innermost enclosing asynchronous for loop (\ref{asynchronousFor-in}), if any, is paused. At some time after $f$ is completed, control returns to the current invocation. The stream associated with the innermost enclosing asynchronous for loop  (\ref{asynchronousFor-in}), if any, is resumed. If $f$ has completed with an exception $x$, $a$ raises $x$. If $f$ completes with a value $v$, $a$ evaluates to $v$.
+Next, the stream associated with the innermost enclosing asynchronous for loop (\ref{asynchronousFor-in}), if any, is paused. The current invocation of the function body immediately enclosing $a$ is suspended until after $f$ completes. At some time after $f$ is completed, control returns to the current invocation. If $f$ has completed with an error $x$ and stack trace $t$, $a$ {\em throws} $x$ and $t$. If $f$ completes with a value $v$, $a$ evaluates to $v$.
 
 %Otherwise, the value of $a$ is the value of $e$. If evaluation of $e$ raises an exception $x$, $a$ raises $x$.
 
 \commentary{
 It is a compile-time error if  the function  immediately enclosing  $a$  is not declared asynchronous.  However, this error is simply a syntax error, because in the context of a normal function, \AWAIT{} has no special meaning.
+% TODO(lrn): Update this, it's not actually correct,
+% the expression "await(expr)" is valid non-async syntax *and* a valid
+% async await expression.
 }
 
 \rationale{
@@ -5425,6 +5481,29 @@ The static type of a cast expression  \code{$e$ \AS{} $T$}  is $T$.
 
 \section{Statements}
 \LMLabel{statements}
+A {\em statement} is a fragment of Dart code that can be executed at runtime. Statements, unlike expressions, do not evaluate to a value, but are instead executed for their effect on the program state.
+Some statements or expression can affect control flow, in particular \BREAK{}, \CONTINUE{}, \RETURN{}, \RETHROW{} and \THROW{}.
+
+\LMLabel{completion}
+Execution of a statement can {\em complete} in one of five ways: either it {\em completes normally}, it {\em breaks} or it {\em continues} (either to a label or without a label), it {\em returns} (with or without a value), or it {\em throws} an exception object and an associated stack trace.
+
+In the description of statement execution, the default is that the execution
+{\em completes normally} unless otherwise stated.
+
+If the execution of a statement, $s$, is defined in terms of executing
+another statement,
+like the body of a loop or the branches of an \IF{} statement,
+and the execution of that other statement doesn't complete normally,
+then, unless otherwise stated, the execution of $s$ stops
+at that point and completes in the same way.
+
+If the execution of a statement is defined in terms of evaluating an expression,
+like the condition expression of an \IF{} statement or the value of a \RETURN{},
+and the evaluation of that expression throws,
+then, unless otherwise stated, the execution of the statement stops
+at that point and throws the same exception object and stack trace.
+
+\LMHash{}
 
  \begin{grammar}
 {\bf statements:}
@@ -5460,7 +5539,7 @@ The static type of a cast expression  \code{$e$ \AS{} $T$}  is $T$.
  \LMLabel{blocks}
 
 \LMHash{}
- A {\em block statement} supports sequencing of code.
+A {\em block statement} supports sequencing of code.
 
 \LMHash{}
 Execution of a block statement $\{s_1, \ldots,  s_n\}$ proceeds as follows:
@@ -5471,10 +5550,8 @@ For $i \in 1 .. n, s_i$ is executed.
 \LMHash{}
 A block statement introduces a new scope, which is nested in the lexically enclosing scope in which the block statement appears.
 
-
-
- \subsection{Expression Statements}
- \LMLabel{expressionStatements}
+\subsection{Expression Statements}
+\LMLabel{expressionStatements}
 
 \LMHash{}
 An {\em expression statement} consists of an expression other than a non-constant map literal (\ref{maps}) that has no explicit type arguments.
@@ -5601,15 +5678,14 @@ The {\em if statement} allows for conditional execution of statements.
 
 \begin{grammar}
 {\bf ifStatement:}
-      \IF{} `(' expression `)' statement ( \ELSE{} statement)? % we could allow top level expression
+      \IF{} `(' expression `)' statement ( \ELSE{} statement)?
     .
- \end{grammar}
+\end{grammar}
 
 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.
-
+ 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
@@ -5691,12 +5767,18 @@ First the variable declaration statement \VAR{} $v = e_0$ is executed. Then:
 \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}.
 \item
-The expression $[v^\prime/v]c$ is evaluated and subjected to boolean conversion (\ref{booleans}). If the result is \FALSE{}, the for loop completes. Otherwise, execution continues at step
+The expression $[v^\prime/v]c$ is evaluated and subjected to boolean conversion (\ref{booleans}). If the result is \FALSE{}, the for loop completes normally. Otherwise, execution continues at step
 \ref{beginIteration}.
 \item
 \label{beginIteration}
 The statement $[v^\prime/v]\{s\}$ is executed.
-\item
+
+If this execution {\em completes normally}, {\em continues} without a label,
+or {\em continues} with a label that prefixes this \FOR{} statement (\ref{labels}),

[eernst, 2016/10/19 13:37:05]

Following the newest plan (around noon, Oct 19), this would not have the {\em..}
around completion related words, but it would have (\ref{completion}) after the
completion related phrase. We could put it 3 times, but maybe this will suffice
(because we have `continues` so close to `with.. a label` everywhere):

`If this execution completes normally, continues without a label, or continues
with a label (\label{labels}) that prefixes this \FOR{} statement
(\ref{completion})`

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Done.

+then execution of the statement is treated as if it had completed normally.
+If it completes in any other way,
+execution of the for loop stops and completes in the same way.
+
 \label{allocateFreshVar}
 Let $v^{\prime\prime}$ be a fresh variable.  $v^{\prime\prime}$ is bound to the value of $v^\prime$.
 \item
@@ -5740,8 +5822,6 @@ var n0 = $e$.iterator;
 \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$.
 
-
-
 \subsubsection{Asynchronous For-in}
 \LMLabel{asynchronousFor-in}
 
@@ -5749,22 +5829,65 @@ where \code{n0} is an identifier that does not occur anywhere in the program, ex
 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 of the form  \code{\AWAIT{} \FOR{} (finalConstVarOrType? id \IN{} $e$) $s$} proceeds as follows:
+Execution of a for-in statement, $f$, of the form \code{\AWAIT{} \FOR{} (finalConstVarOrType? 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}.
 
 \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}. Otherwise, the expression \code{\AWAIT{} $v_f$}  (\ref{awaitExpressions}) is evaluated, where $v_f$ is a fresh variable whose value is a fresh instance (\ref{generativeConstructors}) $f$ implementing the built-in class \code{Future}.
+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.
+This allows other asynchronous events to execute while this loop is waiting for stream events.
+
+Pausing an asynchronous for loop means pausing the associated stream subscription.
+A stream subscription is paused by calling its \code{pause} method.
+\commentary{
+The \code{pause} call can throw, although that should never happen for a correctly implemented stream.
+}
+If the subscription is already paused, the \code{pause} call may be omitted.
 
 \LMHash{}
-The stream $o$ is listened to,  and on each data event in $o$ the statement $s$ is executed with \code{id} bound to the value of the current element of the stream. If $s$ raises an exception, or if $o$ raises an exception, then $f$ is completed with that exception. Otherwise, when all events in the stream $o$ have been processed, $f$ is completed with \NULL{}  (\ref{null}).
+For each {\em data event} from $u$,
+the statement $s$ is executed with \code{id} bound to the value of the current data event.
 
 \LMHash{}
-Let $u$ be the stream associated with the immediately enclosing asynchronous for loop or generator function (\ref{functions}), if any. If another event $e_u$ of $u$ occurs before execution of $s$ is complete, handling of $e_u$ must wait until $s$ is complete.
+If another event $e_u$ of $u$ occurs before execution of $s$ is complete, handling of $e_u$ must wait until $s$ is complete.
 
-\rationale{
-The future $f$ and the corresponding \AWAIT{} expression ensure that execution suspends as an asynchronous for loop begins and resumes after the \FOR{} statement when it ends. They also ensure that the stream of any enclosing asynchronous \FOR{} loop is paused for the duration of this loop.
+\LMHash{}
+If execution of $s$ {\em continues} with no label, or with a label that prefixes the asynchronous for statement (\ref{labels}), then the execution of $s$ is treated as if it had completed normally.
+
+If execution of $s$ does not completing normally, the subscription $u$ is canceled by evaluating \code{\AWAIT{} v.cancel()} where $v$ is a fresh variable referencing the stream subscription $u$.
+If that evaluation throws,
+execution of $f$ throws the same exception and stack trace.
+Otherwise execution of $f$ completes in the same way as the execution of $s$.
+% Notice: The previous specification was unclear about what happened when
+% a subscripton is canceled. This text is explicit, and existing
+% implementations may not properly await the cancel call.
+
+Otherwise the execution of $f$ is suspended again, waiting for the next stream subscription event, and $u$ is resumed if it has been paused.
+If $u$ has been paused more than once, the \code{resume} method is called
+until $u$ is no longer paused.
+\commentary{
+The \code{resume} call can throw, in which case the asynchronous for
+loop also throws. That should never happen for a correctly implemented stream.
 }
 
 \LMHash{}
+On the first {\em error event} from $u$,

[eernst, 2016/10/19 13:37:05]

We shouldn't specify 'first': Saying that something must happen in a given
specification may have as a "lemma" (a necessary consequence) that this must be
the first error event, but if we wish to make this explicit it would be
commentary. The normative text shouldn't mention necessary consequences (it's
redundant).

Also, an "error event from $u$" seems imprecise, how does such an event arise,
or how is it detected?

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Error events are a defined term for streams. They arise by the source putting an
error event into the stream, they are detected by the stream subscription
calling the onError handler.

This is no more (or less) controversial, or less defined, than using "data
event" above.

The current specification was written in imprecise terms. The precise terms
would be that you pass callback functions in the listen call (which is then also
made explicit) and you act when those callback functions are called. 

+with error object $e$ and stack trace $st$,
+the subscription $u$ is canceled by evaluating \code{\AWAIT{} v.cancel()}
+where $v$ is a fresh variable referencing the stream subscription $u$.
+If that evaluation throws,
+execution of $f$ throws the same exception object and stack trace.
+Otherwise execution of $f$ throws with $e$ as exception object and $st$ as stack trace.
+
+\LMHash{}
+When $u$ is done, execution of $f$ completes normally.
+
+\LMHash{}
 It is a compile-time error if an asynchronous for-in statement appears inside a synchronous function (\ref{functions}). It is a compile-time error if a traditional for loop  (\ref{forLoop}) is prefixed by the \AWAIT{}  keyword.
 
 \rationale{An asynchronous loop would make no sense within a synchronous function, for the same reasons that an await expression makes no sense in a synchronous function.}
@@ -5783,10 +5906,15 @@ The while statement supports conditional iteration, where the condition is evalu
  \end{grammar}
 
 \LMHash{}
- Execution of a while statement of the form \code{\WHILE{} ($e$) $s$;} proceeds as follows:
+Execution of a while statement of the form \code{\WHILE{} ($e$) $s$;} proceeds as follows:
 
 \LMHash{}
-The expression $e$ 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\}$ is executed and then the while statement is re-executed recursively. If $r$ is \FALSE{}, execution of the while statement is complete.
+The expression $e$ is evaluated to an object $o$. Then, $o$ is subjected to boolean conversion (\ref{booleanConversion}), producing an object $r$.
+

[eernst, 2016/10/19 13:37:07]

Please insert \LMHash{} or delete the empty line.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Why? Do we need \LMHash between all paragraphs?

+If $r$ is \TRUE{}, then the statement $\{s\}$ is executed.
+If that execution {\em completes normally} or it {\em continues} with no label or with a label that prefixes the \WHILE{} statement (\ref{labels}), then the while statement is re-executed.

[eernst, 2016/10/19 13:37:06]

Should cover the situation where $s$ completes with a break.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Done.

+
+If $r$ is \FALSE{}, then execution of the while statement completes normally.
 
 \LMHash{}
 It is a static type warning if the static type of $e$ may not be assigned to \code{bool}.
@@ -5809,7 +5937,12 @@ The do statement supports conditional iteration, where the condition is evaluate
 Execution of a do statement of the form \code{\DO{} $s$ \WHILE{} ($e$);} proceeds as follows:
 
 \LMHash{}
-The statement $\{s\}$ is executed. Then, the expression $e$ is evaluated to an object $o$. Then, $o$ is  subjected to boolean conversion (\ref{booleanConversion}), producing an object $r$. If $r$ is \FALSE{}, execution of the do statement is complete. If $r$ is \TRUE{}, then the do statement is re-executed recursively.
+The statement $\{s\}$ is executed.
+If that execution {\em continues} with no label, or with a label that prefixes the do statement (\ref{labels}), then the execution of $s$ is treated as if it had completed normally.
+
+\LMHash{}
+Then, the expression $e$ is evaluated to an object $o$. Then, $o$ is subjected to boolean conversion (\ref{booleanConversion}), producing an object $r$. If $r$ is \FALSE{}, execution of the do statement completes normally.
+If $r$ is \TRUE{}, then the do statement is re-executed.
 
 \LMHash{}
 It is a static type warning if the static type of $e$ may not be assigned to \code{bool}.
@@ -5820,7 +5953,7 @@ It is a static type warning if the static type of $e$ may not be assigned to \co
 \LMHash{}
 The {\em switch statement} supports dispatching control among a large number of cases.
 
- \begin{grammar}
+\begin{grammar}
 {\bf switchStatement:}
       \SWITCH{} `(' expression `)' `\{' switchCase* defaultCase? `\}'% could do top level here and in cases
     .
@@ -5909,13 +6042,10 @@ The statement \code{\VAR{} id = $e$;} is evaluated, where \code{id} is a variabl
 \commentary{Note that if there are no case clauses ($n = 0$), the type of $e$ does not matter.}
 
 \LMHash{}
-Next, the case clause \CASE{} $e_{1}: s_{1}$ is executed if it exists. If \CASE{} $e_{1}: s_{1}$ does not exist, then if there is a  \DEFAULT{} clause it is executed by executing $s_{n+1}$.
-
-\LMHash{}
-A case clause introduces a new scope, nested in the lexically surrounding scope. The scope of a case clause ends immediately after the case clause's statement list.
+Next, the case clause \CASE{} $e_{1}: s_{1}$ is matched against {\code id} if such a case clause exists. If \CASE{} $e_{1}: s_{1}$ does not exist, then if there is a \DEFAULT{} clause, its statements, if any, are executed (\ref{case-execute}).

[eernst, 2016/10/19 13:37:07]

We did introduce $s_{n+1}$ a few lines earlier, so the issue is not whether
\DEFAULT{} has any statements, it's whether there is a \DEFAULT{} clause at all.
I'd prefer this:

`.. if there is a \DEFAULT{} clause, its statements $s_{n+1}$ are executed`.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

Done.

 
 \LMHash{}
-Execution of a \CASE{} clause \CASE{} $e_{k}: s_{k}$ of a  switch statement
+Matching of a \CASE{} clause \CASE{} $e_{k}: s_{k}$ of a switch statement

[eernst, 2016/10/19 13:37:06]

Why did the scope sentence go away? Surely we don't want to break all the code
that puts declarations into a `case`?

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Because I now add braces around the statements before executing them.

 
 \begin{dartCode}
 \SWITCH{} ($e$) \{
@@ -5926,16 +6056,15 @@ Execution of a \CASE{} clause \CASE{} $e_{k}: s_{k}$ of a  switch statement
 \}
 \end{dartCode}
 
-proceeds as follows:
+against a value {\code id} proceeds as follows:

[eernst, 2016/10/19 13:37:07]

`{\code id}` --> `$id$`.

I actually think the following text reads better if we use the opposite
ordering: Put 'Matching of a value $id$ against a \CASE{} clause \CASE{} $e_k:
s_k$ of a switch statement' before the code environment, and then just 'proceeds
as follows:' here.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

Done.

 
 \LMHash{}
-The expression \code{$e_k$ == id} is evaluated to an object $o$ which is then subjected to boolean conversion yielding a value $v$.
-If $v$ is not  \TRUE{} the following case,  \CASE{} $e_{k+1}: s_{k+1}$ is executed if it exists. If  \CASE{} $e_{k+1}: s_{k+1}$ does not exist, then the \DEFAULT{} clause is executed by executing $s_{n+1}$.
-If $v$ is \TRUE{},   let $h$ be the smallest number such that $h \ge k$ and $s_h$ is non-empty. If no such $h$ exists, let $h = n + 1$. The  sequence of statements $s_h$ is then executed.
-If execution reaches the point after $s_h$  then  a runtime error occurs, unless $h = n+1$.
+The expression \code{$e_k$ == id} is evaluated to an object $o$ which is then subjected to boolean conversion producing a value $v$.

[eernst, 2016/10/19 13:37:06]

'id' --> '$id$'.

In this CL we had things like 'An {\em expression} is a fragment of Dart code
that can be evaluated at run time to yield a {\em value}', and 'yield' is used
in at least dozens of cases in this way in the spec.

With 'produce' I could only find two examples where the thing 'produced' is the
result of computations: That's when constructors 'produce' an object. In that
case it is already an exception because that's not expression evaluation, it is
"procedure invocation" following the primitive allocation which is associated
with `new`.

So please keep `yielding` here.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

I prefer not to use "yield" since that means something specific in Dart.

Boolean conversion is a function invocation, but it's probably better seen as an
expression evaluation. I think I'll rewrite 'boolean conversion producing" into
"boolean conversion evaluating to"

+If $v$ is not \TRUE{} the following case, \CASE{} $e_{k+1}: s_{k+1}$ is matched against {\code id} if such a case clause exists. If \CASE{} $e_{k+1}: s_{k+1}$ does not exist, then the \DEFAULT{} clause's statements are executed (\ref{case-execute}).

[eernst, 2016/10/19 13:37:07]

'If $v$ is not \TRUE{}, $id$ is matched against the following case, \CASE{}
$e_{k+1}: s_{k+1}$, if it exists; otherwise the default statements $s_{n+1}$ are
executed.'

I'm not sure why there should be a reference \ref{case-execute}, because the
default case has no matching, it's only about execution of ordinary statements.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

\ref{case-execute} is about executing the *statements* of a case or default
clause. It's not case-matching.
It is needed because execution of case statements need to know about the
surrounding switch case so it can properly jump on a continue-to-label.

I think the simplest way to specify this is to handle the continue at the end of
the execution of the case-statements. The alternative is to let the continue
bubble up and complete the switch case, and then add an extra clause saying that
if the switch case continues to a label declared by the switch case, the switch
statement is re-executed from the execution of the related statements. This
leaving and reentering the switch statement is too confusing, so I'm making this
iterative on the case statement block execution.

+If $v$ is \TRUE{}, let $h$ be the smallest number such that $h \ge k$ and $s_h$ is non-empty. If no such $h$ exists, let $h = n + 1$. The statements $s_h$ are then executed (\ref{case-execute}).
 
 \LMHash{}
-Execution of a \CASE{} clause \CASE{} $e_{k}: s_{k}$ of a  switch statement
+Matching of a \CASE{} clause \CASE{} $e_{k}: s_{k}$ of a switch statement
 
 \begin{dartCode}
 \SWITCH{} ($e$) \{
@@ -5945,19 +6074,14 @@ Execution of a \CASE{} clause \CASE{} $e_{k}: s_{k}$ of a  switch statement
 \}
 \end{dartCode}
 
-proceeds as follows:
+against the value of a variable {\code id} proceeds as follows:
 
 \LMHash{}
-The expression \code{$e_k$ == id} is evaluated to an object $o$ which is then subjected to boolean conversion yielding a value $v$.
-If $v$ is not  \TRUE{} the following case,  \CASE{} $e_{k+1}: s_{k+1}$ is executed if it exists.
-If $v$ is \TRUE{},   let $h$ be the smallest integer such that $h \ge k$ and $s_h$ is non-empty. The  sequence of statements $s_h$ is  executed if it exists.
-If execution reaches the point after $s_h$  then  a runtime error occurs, unless $h = n$.
+The expression \code{$e_k$ == id} is evaluated to an object $o$ which is then subjected to boolean conversion producing a value $v$.

[eernst, 2016/10/19 13:37:07]

Keep `yielding`.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

evalautes to

+If $v$ is not \code{true} the following case, \CASE{} $e_{k+1}: s_{k+1}$ is matched against {\code id} if it exists.

[eernst, 2016/10/19 13:37:07]

We have no existing occurrences of `\code{true}`, and the spec has the following
at the beginning of \subsection{Booleans}:

`The reserved words \TRUE{} and \FALSE{} denote objects that represent the
boolean values true and false respectively.`

So we already use the plain words true and false (no special formatting) for the
value yielded by an evaluation of \TRUE{} and \FALSE{}. So this could be as
follows:

'If $v$ is not true, $id$ is matched against the following case \CASE{}
$e_{k+1}: s_{k+1}$; otherwise, the switch statement completes normally.'

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

I see varying uses of true and \TRUE{}, but \code{true} is right out.
I think I'll use \TRUE{} here for temporary consistency, and then we can look at
it later and see if "true" or "\TRUE{}" is better

+If $v$ is \code{true}, let $h$ be the smallest integer such that $h \ge k$ and $s_h$ is non-empty. If no such $h$ exists, let $h$ be $n$. The sequence of statements $s_h$ is executed (\ref{case-execute}).

[eernst, 2016/10/19 13:37:06]

'\code{true}' --> 'true', drop the \ref.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:43]

\TRUE{}, keeping the ref with a slight rewording.

 
 
-\commentary{
-In other words, there is no implicit fall-through between non-empty cases. The last case in a switch (default or otherwise) can `fall-through' to the end of the statement.
-}
-
 \LMHash{}
 It is a static warning if the type of $e$ may not be assigned to the type of $e_k$. It is a static warning if the last statement of the statement sequence $s_k$ is not a \BREAK{}, \CONTINUE{}, \RETURN{} or \THROW{} statement.
 
@@ -5989,13 +6113,62 @@ The sophistication of the analysis of fall-through is another issue. For now, we
 In other words, a warning will be issued if a switch statement over an enum is not exhaustive.
 }
 
+\LMHash{}
+\subsubsection{ Switch case statements}

[eernst, 2016/10/19 13:37:06]

Argh, we don't have to have that weird space ('{ S') in _new_ material!

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Thanks. :)

+\LMLabel{case-execute}
+Execution of the statements $s_h$ of a switch statement

[eernst, 2016/10/19 13:37:05]

Please add empty line and `\LMHash{}` in front of normative paragraph.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

Done.

+
+\begin{dartCode}
+\SWITCH{} ($e$) \{
+   $label_{11} \ldots label_{1j_1}$ \CASE{} $e_1: s_1$
+   $\ldots$
+   $label_{n1} \ldots label_{nj_n}$ \CASE{} $e_n: s_n$
+\}
+\end{dartCode}
+
+or a switch statement
+
+\begin{dartCode}
+\SWITCH{} ($e$) \{
+   $label_{11} \ldots label_{1j_1}$ \CASE{} $e_1: s_1$
+   $\ldots$
+   $label_{n1} \ldots label_{nj_n}$ \CASE{} $e_n: s_n$
+   $label_{(n+1)1} \ldots label_{(n+1)j_{n+1}}$ \DEFAULT{}: $s_{n+1}$
+\}
+\end{dartCode}
+
+proceeds as follows:
+
+\LMHash{}
+Execute $\{s_h\}$.
+If this execution completes normally,
+and if $s_h$ is not the statements of the last case of the switch
+($h = n$ if there is no \DEFAULT{} clause,
+$h = n+1$ if there is a \DEFAULT{} clause),
+then the execution of the switch case throws an error.
+Otherwise $s_h$ are the last statements of the switch case,
+and execution of the switch case completes normally.
+
+\commentary{
+In other words, there is no implicit fall-through between non-empty cases. The last case in a switch (default or otherwise) can `fall-through' to the end of the statement.
+}
+
+If execution of $\{s_h\}$ {\em breaks} with no label, or with a label that prefixes the switch statement, then the execution of the switch statement completes normally.
+
+If execution of $\{s_h\}$ {\em continues} with a label, and the label is $label_{ij}$, where $1 \le i \le n+1$ if the \SWITCH{} statement has a \DEFAULT{}, or $1 \le i \le n$ if there is no \DEFAULT{}, and where $1 \le j \le j_{i}$, then
+execution of the switch statement continues with the case labeled by that label.

[eernst, 2016/10/19 13:37:06]

This again shows that 'execution continues' is too smart to work really well,
because we will (1) need to very carefully avoid saying 'execution continues' in
the normal sense; and I'm not convinced that it is enough to use the magic `{\em
continues}` for the completion mode.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Removed entire line, it's purely explanatory, the following lines says exactly
what happens.

+let $h$ be the smallest number such that $h \ge i$ and $s_h$ is non-empty. If no such $h$ exists, and let $h = n + 1$ if the \SWITCH{} statement has a \DEFAULT{}, otherwise let $h = n$.
+The statements $s_h$ are then executed (\ref{case-execute}).
+
+If execution of $\{s_h\}$ completes in any other way, execution of the \SWITCH{} statement completes in the same way.
+

[eernst, 2016/10/19 13:37:06]

It's hard to tell which is better, but we should consider the alternatives:
Either we'd specify that the execution runs `s_h; throw <something>`, or we'd
spell out how to get the same effect without the code.

In order to maintain compositionality we should of course never execute
manipulated code ;-)

but the description given here illustrates how much more index manipulation it
takes to use this alternative.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

This extra text and index manipulation is only necessary due to 'continue
label". It's not really affected by the implicit throw.

 
 \subsection{ Rethrow}
 \LMLabel{rethrow}
 
 
 \LMHash{}
-The {\em rethrow statement}  is used to re-raise an exception.
+The {\em rethrow statement}  is used to re-throw an exception and its associated stack trace.
 
  \begin{grammar}
 {\bf rethrowStatement:}
@@ -6014,25 +6187,12 @@ A \RETHROW{} statement always appears inside a \CATCH{} clause, and any \CATCH{}
 }
 
 \LMHash{}
-The current exception (\ref{throw}) is set to $p_1$, the current return value (\ref{return}) becomes undefined, and the active stack trace (\ref{try}) is set to $p_2$.
-
-\LMHash{}
-If $f$ is marked \ASYNC{} or \ASYNC* (\ref{functions}) and there is a dynamically enclosing exception handler (\ref{try}) $h$ introduced by the current activation, control is transferred to $h$, otherwise $f$  terminates.
-
-\rationale{
-In the case of an asynchronous function, the dynamically enclosing exception handler is only relevant within the function. If an exception is not caught within the function, the exception value is channelled through a future or stream rather than propagating via exception handlers.
-}
-
-\LMHash{}
-Otherwise, control is transferred to the  innermost enclosing exception handler.
-
-\commentary{The change in control may result in multiple functions terminating if these functions do not catch the exception via a \CATCH{} or \FINALLY{} clause, both of which introduce a dynamically enclosing exception handler.}
+The \RETHROW{} statement {\em throws} (\ref{completion}) with $p_1$ as the exception object and $p_2$ as the stack trace.
 
 \LMHash{}
 It is a compile-time error if a  \code{\RETHROW{}} statement is not enclosed within an \ON-\CATCH{} clause.
 
 
-
 \subsection{ Try}
 \LMLabel{try}
 
@@ -6058,10 +6218,10 @@ The try statement supports the definition of exception handling code in a struct
  \end{grammar}
 
 \LMHash{}
- A try statement consists of a block statement, followed by at least one of:
- \begin{enumerate}
- \item
-A set of \ON{}-\CATCH{} clauses, each of which specifies  (either explicitly or implicitly) the type of exception object to be handled, one or two exception parameters and a block statement.
+A try statement consists of a block statement, followed by at least one of:
+\begin{enumerate}
+\item
+A set of \ON{}-\CATCH{} clauses, each of which specifies (either explicitly or implicitly) the type of exception object to be handled, two exception parameters and a block statement.

[eernst, 2016/10/19 13:37:06]

We still need to textually allow the omission of the stack trace parameter, just
like the grammar rule says, right?

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

Yes, and the grammar above does. There is "catch without stack variable
equivalent to one with" section below.

 \item
 A \FINALLY{} clause, which consists of a block statement.
 \end{enumerate}
@@ -6071,122 +6231,83 @@ The syntax is designed to be upward compatible with existing Javascript programs
 }
 
 \LMHash{}
-An \ON{}-\CATCH{} clause of the form   \code{\ON{} $T$ \CATCH{} ($p_1, p_2$) $s$}  {\em matches} an object $o$  if the type of $o$ is a subtype of $T$.  If $T$ is a malformed or deferred type  (\ref{staticTypes}), then performing a match causes a run time error.
-
-\commentary {
-It is of course a static warning if $T$ is a deferred or malformed type.
-}
-
-\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}.
-
+A try statement of the form \code{\TRY{} $s_1$ $on-catch_1 \ldots on-catch_n$;} is equivalent to the statement \code{\TRY{} $s_1$ $on-catch_1 \ldots on-catch_n$ \FINALLY{} $\{\}$}.
 
 \LMHash{}
 An \ON{}-\CATCH{} clause of the form  \code{\ON{} $T$ \CATCH{} ($p_1$) $s$} is equivalent to an \ON{}-\CATCH{} clause  \code{\ON{} $T$ \CATCH{} ($p_1, p_2$) $s$} where $p_2$ is an identifier that does not occur anywhere else in the program.

[eernst, 2016/10/19 13:37:07]

We have 12 occurrences of `fresh variable` and only two (until now) of
identifier-or-variable that `does not occur`, so we might as well use `fresh
variable` everywhere in new material.

We should then make sure that it is defined once and for all, possibly in
\section{Overview}.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Agree

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

Agree

 
I don't think it fits in Overview, so I put it in Notation.

 
-
 \LMHash{}
-An \ON{}-\CATCH{} clause of the form  \code{\CATCH{} ($p$) $s$} is equivalent to an \ON{}-\CATCH{} clause  \code{\ON{} \DYNAMIC{} \CATCH{} ($p$) $s$}. 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$}.
-
-
-%If an explicit type is associated with of $p_2$, it is a static warning if that type is not \code{Object} or \DYNAMIC{}.
+An \ON{}-\CATCH{} clause of the form  \code{\ON{} $T$ $s$} is equivalent to an \ON{}-\CATCH{} clause  \code{\ON{} $T$ \CATCH{} ($p_1, p_2$) $s$} where $p_1$ and $p_2$ are identifiers that do not occur anywhere else in the program.

[eernst, 2016/10/19 13:37:06]

`fresh variable`

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

Done.

 
 \LMHash{}
-The {\em active stack trace} is an object whose \code{toString()} method produces a string that is a record of exactly those function activations within the current isolate that had not completed execution at the point where the current exception (\ref{throw}) was thrown.
-%\begin{enumerate}
-%\item Started execution after the currently executing function.
-%\item Had not completed execution at the point where the exception caught by the currently executing  \ON{}-\CATCH{} clause was initially thrown.
-%\commentary{The active stack trace contains the frames between the exception handling code and the original point when an exception is thrown, not where it was rethrown.}
-%\end{enumerate}
-
- \commentary{
-This implies that no synthetic function activations may be added to the trace, nor may any source level activations be omitted.
-This means, for example, that any inlining of functions done as an optimization must not be visible in the trace. Similarly, any synthetic routines used by the implementation must not appear in the trace.
-
-Nothing is said about how any native function calls may be represented in the trace.
- }
-
-\commentary{
-Note that we say nothing about the identity of the stack trace, or what notion of equality is defined for stack traces.
-}
-
-% Sadly, the info below cannot be computed efficiently. It would need to be computed at the throw point, since at latte points it might be destroyed. Native code in calling frames executes relative to the stack pointer, which therefore needs to be reset as each frame is unwound.  This means that the
-% OS kernel can dispose of this stack memory - it is not reliably preserved. And such code must execute if only to test if the exception should be caught or sent onward.
-
-% For each such function activation, the active stack trace includes the name of the function, the bindings of all its formal parameters, local variables and \THIS{}, and the position at which the function was executing.
+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 an identifier that does not occur anywhere else in the program.

[eernst, 2016/10/19 13:37:06]

`fresh variable`

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Done.

 
- % Is this controversial? We were thinking of viewing the trace as a List<Invocation>,
- % but that won't capture the receiver or the locals. More generally, we need a standard interface that describes these traces, so one can type the stack trace variable in the catch.
-
- \commentary{The term position should not be interpreted as a line number, but rather as a precise position - the exact character index of the  expression that raised  the exception. }
-
- % A position can be represented via a Token. If we make that part of the core reflection facility, we can state this here.
-
-\LMHash{}
-A try statement \TRY{} $s_1$ $on-catch_1 \ldots  on-catch_n$ \FINALLY{} $s_f$  defines an exception handler $h$ that executes as follows:
+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{}
-The \ON{}-\CATCH{} clauses are examined in order, starting with $catch_1$, until either an \ON{}-\CATCH{} clause that matches the current exception (\ref{throw}) is found, or the list of \ON{}-\CATCH{} clauses has been exhausted. If an \ON{}-\CATCH{} clause $on-catch_k$ is found, then $p_{k1}$ is bound to the current exception,  $p_{k2}$, if declared,  is bound to the active stack trace, and then $catch_k$ is executed. If no \ON{}-\CATCH{} clause is found, the \FINALLY{} clause is executed. Then, execution resumes at the end of the try statement.
+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{}
-A finally clause \FINALLY{} $s$ defines an exception handler $h$ that executes as follows:
+Execution of a \TRY{} statement $s$ on 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{}
-Let $r$ be the current return value (\ref{return}). Then the current return value becomes undefined. Any open streams associated with any asynchronous for loops (\ref{asynchronousFor-in}) and yield-each (\ref{yieldEach}) statements executing within the dynamic scope of $h$ are canceled, in the order of their nesting, innermost first.
+First $b$ is executed.
+If execution of $b$ {\em 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}).

[eernst, 2016/10/19 13:37:07]

Just 'throws'.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Done.

 
-\rationale{
-Streams left open by for loops that were escaped for whatever reason would be canceled at function termination, but it is best to cancel them as soon as possible.
-}
+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.
 
-\LMHash{}
-Then the \FINALLY{} clause is executed. Let $m$ be the immediately enclosing function. If $r$ is defined then the current return value is set to $r$ and then:
-\begin{itemize}
-\item
- if there is a dynamically enclosing error handler $g$ defined by a \FINALLY{} clause in $m$, control is transferred to $g$.
- \item
-Otherwise $m$ terminates.
-\end{itemize}
-
-Otherwise, execution resumes at the end of the try statement.
+If execution of $f$ does not complete normally,
+execution of the \TRY{} statement completes in the same way.
+Otherwise if execution of $b$ threw, the \TRY{} statement completes in the same way as the matching against the \ON{}-\CATCH{} clauses.

[eernst, 2016/10/19 13:37:05]

`threw (\ref{completion})`

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Done.

+Otherwise the \TRY{} statement completes in the same way as the execution of $b$.
 
+\subsubsection{\ON{}-\CATCH{} clauses}

[eernst, 2016/10/19 13:37:05]

`\LMLabel{..}`, empty line.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

Why add a label if it isn't referenced?

 \LMHash{}
-Execution of an \ON{}-\CATCH{} clause \code{\ON{} $T$ \CATCH{} ($p_1$, $p_2$)} $s$ of a try statement $t$ proceeds as follows: The statement $s$ is executed in the dynamic scope of the exception handler defined by the finally clause of $t$. Then, the current exception and active stack trace both become undefined.
+Matching an exception object $e$ and stack trace $t$ against a (potentially empty) sequence of \ON{}-\CATCH{} clauses on 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}

[eernst, 2016/10/19 13:37:06]

+`proceeds as follows:`, and no colon after `form` above.

 
 \LMHash{}
-Execution of a \FINALLY{} clause \FINALLY{} $s$ of a try statement proceeds as follows:
+If there are no \ON{}-\CATCH{} clauses ($n = 0$), matching completes by {\em throwing} the exception object $e$ and stack trace $t$.

[eernst, 2016/10/19 13:37:06]

`completes by throwing (\ref{completion})`

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Throws.

 
+Otherwise the exception is matched against the first clause.
 \LMHash{}

[eernst, 2016/10/19 13:37:05]

Move `LMHash` up in front of the paragraph, and add one just before the next
one.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Done.

-Let $x$ be the current exception and let $t$ be the active stack trace. Then the current exception and the active stack trace both become undefined. The statement $s$ is executed. Then, if $x$ is defined,  it is rethrown as if by a rethrow statement (\ref{rethrow}) enclosed in a \CATCH{} clause of the form \code{\CATCH{} ($v_x$, $v_t$)} where $v_x$ and $v_t$ are fresh variables bound to $x$ and $t$ respectively.
 
+If $T_1$ is a malformed or deferred type (\ref{staticTypes}), then performing a match causes a run time error.
+\commentary {
+It is of course a static warning if $T_i$, $1 \le i \le n$ is a deferred or malformed type.

[eernst, 2016/10/19 13:37:06]

Delete 'of course' and move this sentence up a few lines to a context where the
`try` statement is discussed as a whole.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

Done.

+}
 
 \LMHash{}
-Execution of a try statement of the form \code{\TRY{} $s_1$ $on-catch_1 \ldots on-catch_n$ \FINALLY{} $s_f$;}  proceeds as follows:
-
-\LMHash{}
-The statement $s_1$ is executed in the dynamic scope of the exception handler defined by the try statement. Then, the \FINALLY{} clause is executed.
-
-\commentary{
-Whether any of the \ON{}-\CATCH{} clauses is executed depends on whether a matching exception has been raised by $s_1$ (see the specification of the throw statement).
-
-If $s_1$ has raised an exception, it will transfer control to the try statement's handler, which will examine the catch clauses in order for a match as specified above. If no matches are found, the handler will execute the \FINALLY{} clause.
-
-If a matching \ON{}-\CATCH{} was found, it will execute first, and then the \FINALLY{} clause will be executed.
-
-If an exception is thrown during execution of an \ON{}-\CATCH{} clause, this will transfer control to the handler for the \FINALLY{} clause, causing the \FINALLY{} clause to execute in this case as well.
-
-If no exception was raised, the \FINALLY{} clause is also executed. Execution of the \FINALLY{} clause could also raise an exception, which will cause transfer of control to the next enclosing handler.
-}
+Otherwise, if the type of $e$ is a subtype of $T_1$, then the first clause matches, and then $e_1$ is bound to the exception object $e$ and $t_1$ is bound to the stack trace $t$, and $s_1$ is executed in this scope.
+The matching completes in the same way as this execution.
 
 \LMHash{}
-A try statement of the form \code{\TRY{} $s_1$ $on-catch_1 \ldots on-catch_n$;} is equivalent to the statement \code{\TRY{} $s_1$ $on-catch_1 \ldots on-catch_n$ \FINALLY{} $\{\}$}.
+Otherwise, if the first clause did not match $e$, $e$ and $t$ are recursively matched against the remaining \ON{}-\CATCH{} clauses:
+\begin{dartCode}
+\ON{} $T_2$ \CATCH{} ($e_2$, $t_2$) \{ $s_2$ \}
+\ldots
+\ON{} $T_n$ \CATCH{} ($e_n$, $t_n$) \{ $s_n$ \}
+\end{dartCode}
 

[eernst, 2016/10/19 13:37:06]

Wow, that's a substantial improvement!

Was the semantics of canceling stream subscriptions of enclosing await-for
statements preserved by adding the same thing to them based on the completion
mode of its body?

Also, is it an improvement that the spec says nothing about stack traces any
more? Or is there something elsewhere? I couldn't find it based on a few naive
searches.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Yes - that cancelling of the subscription of an await-for is now specified with
the await for, independently of how the body completes.

Not sure what about stack traces you are referring to. The spec now does say
something about stack traces - they are introduced at throws and propagated with
the exception.

 
 \subsection{ Return}
 \LMLabel{return}
 
 \LMHash{}
-The {\em return statement} returns a result to the caller of a synchronous function,  completes the future associated with an asynchronous function or terminates the stream or iterable associated with a generator (\ref{functions}).
+The {\em return statement} returns a result to the caller of a synchronous function, completes the future associated with an asynchronous function or terminates the stream or iterable associated with a generator (\ref{functions}).
 
 
  \begin{grammar}
@@ -6195,31 +6316,12 @@ The {\em return statement} returns a result to the caller of a synchronous funct
     .
  \end{grammar}
 
- \commentary{
- Due to \FINALLY{} clauses, the precise behavior of \RETURN{} is a little more involved. Whether the value a return statement is supposed to return is actually returned depends on the behavior of any \FINALLY{} clauses in effect when executing the return. A \FINALLY{} clause may choose to return another value, or throw an exception, or even redirect control flow leading to other returns or throws. All a return statement really does is set a value that is intended to be returned when the function terminates.
- }
-
-\LMHash{}
-The {\em current return value} is a unique value specific to a given function activation. It is undefined unless explicitly set in this specification.
-
 \LMHash{}
 Executing a return statement \code{\RETURN{} $e$;} proceeds as follows:
 
 \LMHash{}
-First the expression $e$ is evaluated, producing an object $o$. Next:
-\begin{itemize}
-\item
-The current return value is set to $o$ and the current exception (\ref{throw}) and active stack trace (\ref{try}) become undefined.
-\item
-Let $c$ be the \FINALLY{} clause of the innermost enclosing try-finally statement (\ref{try}), if any. If $c$ is defined, let $h$ be the handler induced by $c$. If $h$ is defined, control is transferred to $h$.
-\item
-Otherwise execution of the current method terminates.
-\end{itemize}
-
-\commentary{
-In the simplest case, the immediately enclosing function is an ordinary, synchronous non-generator, and upon function termination, the current return value is given to the caller.  The other possibility is that the function is marked \ASYNC{}, in which case the current return value is used to complete the future associated with the function invocation. Both these scenarios are specified in section \ref{functionInvocation}.
-The enclosing function cannot be marked as generator (i.e, \ASYNC* or \SYNC*), since generators are not allowed to contain a statement of the form \code{\RETURN{} $e$;} as discussed below.
-}
+First the expression $e$ is evaluated, producing an object $o$.
+Then the return statement completes by \em{returning} the value $o$ (\ref{completion}).

[eernst, 2016/10/19 13:37:06]

The `\em{..}` construct makes a zero-argument command like `\em` leak into the
enclosing text (so lots of stuff will now be \em'd.

As usual, I'd suggest: `completes by returning..`.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

Just: returns the value $o$

 
 \LMHash{}
 Let $T$ be the static type of $e$ and let $f$ be the immediately enclosing function.
@@ -6228,13 +6330,6 @@ Let $T$ be the static type of $e$ and let $f$ be the immediately enclosing funct
 It is a static type warning if the body of $f$ is marked \ASYNC{} and the type \code{Future$<$flatten(T)$>$} (\ref{functionExpressions}) may not be assigned to the declared return type of $f$.    Otherwise, it is a static type warning if $T$ may not be assigned to the declared return type of $f$.
 
 \LMHash{}

[eernst, 2016/10/19 13:37:07]

Why did the ASYNC / wrong-return-type error paragraph go away? Is that because
\section{functionInvocation} says what needs to be said for this?

A quick check did not reveal that this has happened, shouldn't it be added
around line 3600?

[Lasse Reichstein Nielsen, 2016/10/31 16:54:43]

Good point. Must have gotten lost somewhere.
I think I'll just reintroduce it here, and then if it needs to be moved, we can
do it later.
I think it's a good thing if the stack trace corresponds to the return
statement, so it probably should be thrown here.

-Let $S$ be the runtime type of $o$. In checked mode:
-\begin{itemize}
-\item  If the body of $f$ is marked \ASYNC{} (\ref{functions}) it is a dynamic type error if $o$ is not \NULL{} (\ref{null}) and \code{Future$<$flatten(S)$>$} is not a subtype of the actual return type  (\ref{actualTypeOfADeclaration}) of $f$.
-\item Otherwise, it is a dynamic type error if $o$ is not \NULL{} and the runtime type of $o$ is not a subtype of the actual return type of $f$.
-\end{itemize}
-
-\LMHash{}
 It is a compile-time error if a return statement of the form \code{\RETURN{} $e$;} appears in a generative constructor (\ref{generativeConstructors}).
 
 \rationale{
@@ -6263,40 +6358,13 @@ Hence, a static warning will not be issued if $f$ has no declared return type, s
 \rationale{ An asynchronous non-generator always returns a future of some sort. If no expression is given, the future will be completed with \NULL{} and this motivates the requirement above.} \commentary{Leaving the return type of a function marked \ASYNC{}  blank will be interpreted as \DYNAMIC{} as always, and cause no type error. Using \code{Future} or \code{Future$<$Object$>$} is acceptable as well, but any other type will cause a warning, since \NULL{} has no subtypes.}
 
 \LMHash{}
-A return statement with no expression, \code{\RETURN;} is executed as follows:
+Executing a return statement with no expression, \code{\RETURN;} {\em returns} with no value (\ref{completion}).

[eernst, 2016/10/19 13:37:07]

I'd still prefer `returns with the value null (\ref{completion}).`, to make it
work as implemented and as-expected-in-the-future in order to make it
well-defined what happens if the value returned from a `void` function gets used
(because the type checker couldn't see it coming).

[Lasse Reichstein Nielsen, 2016/10/31 16:54:43]

This is well-defined. If a function invocation's execution of the function body
returns without a value, the function invocation expression evaluates to null.
There is no change to the semantics, and the static type shouldn't be affected
by anything.

 
-\LMHash{}
-If the immediately enclosing function $f$ is a generator, then:
-\begin{itemize}
-\item
-The current return value is set to \NULL{}.
-\item
-Let $c$ be the \FINALLY{} clause of the innermost enclosing try-finally statement, if any. If $c$ is defined,  let $h$ be the handler induced by $c$. If $h$ is defined, control is transferred to $h$.
-\item
-Otherwise, execution of the current method terminates.
-\end{itemize}
-
-\LMHash{}
-Otherwise the return statement is executed by executing the statement  \code{\RETURN{} \NULL{};} if it occurs inside a method, getter, setter or factory; otherwise, the return statement necessarily occurs inside a generative constructor, in which case it is executed by executing  \code{\RETURN{} \THIS{};}.
-
-\commentary{Despite the fact that \code{\RETURN{};} is executed as if by a \code{\RETURN{} $e$;}, it is important to understand that it is not a static warning to include a statement of the form \code{\RETURN{};}
-%in a \VOID{} function; neither is it illegal
-in a generative constructor. The rules relate only to the specific syntactic form \code{\RETURN{} $e$;}.
-}
-
-
-\rationale{
-The motivation for formulating \code{\RETURN{};} in this way stems from the basic requirement that all function invocations indeed return a value. Function invocations are expressions, and we cannot rely on a mandatory typechecker to always prohibit use of \VOID{} functions in expressions. Hence, a return statement must always return a value, even if no expression is specified.
-
-The question then becomes, what value should a return statement return when no return expression is given. In a generative constructor, it is obviously the object being constructed (\THIS{}). A void function is not expected to participate in an expression, which is why it is marked \VOID{} in the first place. Hence, this situation is a mistake which should be detected as soon as possible. The static rules help here, but if the code is executed, using \NULL{} leads to fast failure, which is desirable in this case. The same rationale applies for function bodies that do not contain a return statement at all.
-}
 
 \LMHash{}
 It is a static warning if a  function contains both one or more explicit return statements of the form \code{\RETURN;} and one or more return statements of the form \code{\RETURN{} $e$;}.
 
 
-
-
 \subsection{ Labels}
 \LMLabel{labels}
 
@@ -6314,7 +6382,12 @@ A {\em label} is an identifier followed by a colon. A {\em labeled statement} is
  \end{grammar}
 
 \LMHash{}
- The semantics of a labeled statement $L: s$ are identical to those of the statement $s$. The namespace of labels is distinct from the one used for types, functions and variables.
+Execution a labeled statement $s$, $label: s_l$, consists of executing $s_l$.
+If execution of $s_l$ {\em breaks} with the label $label$,
+then execution of $s$ completes normally,
+otherwise execution of $s$ completes in the same ways as the execution of $s_l$.
+
+The namespace of labels is distinct from the one used for types, functions and variables.

[eernst, 2016/10/19 13:37:07]

Prepend `LMHash{}` to new paragraph.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

It's not new - it's just separated from its original paragraph.
But done.

 
 \LMHash{}
 The scope of a label that labels a statement $s$ is $s$. The scope of a label that labels a case clause of a switch statement $s$ is $s$.
@@ -6336,11 +6409,12 @@ The {\em break statement} consists of the reserved word \BREAK{} and an optional
  \end{grammar}
 
 \LMHash{}
-Let $s_b$ be a \BREAK{} statement. If $s_b$ is of the form  \code{\BREAK{} $L$;}, then let $s_E$ be the innermost labeled statement with label $L$ enclosing $s_b$. If $s_b$ is of the form \code{\BREAK{};},  then let $s_E$ be the innermost  \DO{} (\ref{do}), \FOR{} (\ref{for}), \SWITCH{} (\ref{switch}) or \WHILE{} (\ref{while}) statement enclosing  $s_b$. It is a compile-time error if no such statement $s_E$ exists within the innermost function in which  $s_b$ occurs.  Furthermore, let $s_1, \ldots, s_n$ be those \TRY{} statements that are both enclosed in $s_E$ and that enclose  $s_b$, and that have a \FINALLY{} clause. Lastly, let $f_j$ be the \FINALLY{} clause of $s_j, 1 \le j \le n$.   Executing  $s_b$ first executes $f_1, \ldots,  f_n$ in innermost-clause-first  order and then terminates $s_E$.
+Let $s_b$ be a \BREAK{} statement. If $s_b$ is of the form  \code{\BREAK{} $L$;}, then let $s_E$ be the innermost labeled statement with label $L$ enclosing $s_b$. If $s_b$ is of the form \code{\BREAK{};},  then let $s_E$ be the innermost  \DO{} (\ref{do}), \FOR{} (\ref{for}), \SWITCH{} (\ref{switch}) or \WHILE{} (\ref{while}) statement enclosing  $s_b$. It is a compile-time error if no such statement $s_E$ exists within the innermost function in which  $s_b$ occurs.
 
 \LMHash{}
-If $s_E$ is an asynchronous for loop (\ref{asynchronousFor-in}), its associated stream subscription is canceled. Furthermore, let $a_k$ be the set of asynchronous for loops  and yield-each statements (\ref{yieldEach}) enclosing $s_b$ that are enclosed in $s_E , 1 \le k \le m$, where $a_k$ is enclosed in $a_{k+1}$.   The stream subscriptions associated with $a_j$ are canceled, $1 \le j \le m$, innermost first, so that $a_j$ is canceled before $a_{j+1}$.
+Execution of a \BREAK{} statement \code{\BREAK{} label;} completes by {\em breaking} with the label \code{label} (\ref{completion}).

[eernst, 2016/10/19 13:37:07]

`{\em breaking}` --> `breaking`.

We have the same issue here is before with `id`: It ought to be $label$, unless
that is too unreadable. If it looks bad then we can use `\mbox{\em label}`,
which will work in a math context and produce reasonable kerning.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Done.

Changed the label to $L$.

 
+Execution of a \BREAK{} statement \code{\BREAK{};} completes by {\em breaking} without a label (\ref{completion}).

[eernst, 2016/10/19 13:37:06]

`{\em breaking}` --> `breaking`.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

Done.

 
 
 \subsection{ Continue}
@@ -6356,25 +6430,23 @@ The {\em continue statement} consists of the reserved word \CONTINUE{} and an op
  \end{grammar}
 
 \LMHash{}
- Let $s_c$ be a \CONTINUE{} statement. If $s_c$ is of the form  \code{\CONTINUE{} $L$;}, then let $s_E$ be the innermost labeled \DO{} (\ref{do}), \FOR{} (\ref{for}) or \WHILE{} (\ref{while}) statement or case clause with label $L$ enclosing $s_c$. If $s_c$ is of the form \code{\CONTINUE{};}  then let $s_E$ be the innermost  \DO{} (\ref{do}), \FOR{} (\ref{for}) or \WHILE{} (\ref{while}) statement enclosing  $s_c$. It is a compile-time error if no such statement or case clause $s_E$ exists within the innermost function in which  $s_c$ occurs.  Furthermore, let $s_1, \ldots, s_n$ be those \TRY{} statements that are both enclosed in $s_E$ and that enclose  $s_c$, and that have a \FINALLY{} clause. Lastly, let $f_j$ be the \FINALLY{} clause of $s_j, 1 \le j \le n$.   Executing  $s_c$ first executes $f_1, \ldots,  f_n$ in innermost-clause-first  order. Then, if $s_E$ is a case clause, control is transferred to the case clause. Otherwise, $s_E$ is necessarily a loop and execution resumes after the last statement in the loop body.
+Let $s_c$ be a \CONTINUE{} statement. If $s_c$ is of the form  \code{\CONTINUE{} $L$;}, then let $s_E$ be the innermost labeled \DO{} (\ref{do}), \FOR{} (\ref{for}) or \WHILE{} (\ref{while}) statement or case clause with label $L$ enclosing $s_c$. If $s_c$ is of the form \code{\CONTINUE{};}  then let $s_E$ be the innermost  \DO{} (\ref{do}), \FOR{} (\ref{for}) or \WHILE{} (\ref{while}) statement enclosing  $s_c$. It is a compile-time error if no such statement or case clause $s_E$ exists within the innermost function in which  $s_c$ occurs.
 
- \commentary{
- In a while loop, that would be the boolean expression before the body. In a do loop, it would be the boolean expression after the body. In a for loop, it would be the increment clause.  In other words, execution continues to the next iteration of the loop.
- }
+Execution of a \CONTINUE{} statement \code{\CONTINUE{} label;} completes by {\em continuing} with the label \code{label} (\ref{completion}).

[eernst, 2016/10/19 13:37:06]

`continuing`

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

Done.

 
-\LMHash{}
- If $s_E$ is an asynchronous for loop (\ref{asynchronousFor-in}), let $a_k$ be the set of asynchronous for loops and yield-each statements (\ref{yieldEach}) enclosing $s_c$ that are enclosed in $s_E , 1 \le k \le m$, where $a_k$ is enclosed in $a_{k+1}$.   The stream subscriptions associated with $a_j$ are canceled, $1 \le j \le m$, innermost first, so that $a_j$ is canceled before $a_{j+1}$.
+Execution of a \CONTINUE{} statement \code{\CONTINUE{};} completes by {\em continuing} without a label (\ref{completion}).

[eernst, 2016/10/19 13:37:06]

`continuing`

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

Done.

 
- \subsection{ Yield and Yield-Each}
- \LMLabel{yieldAndYieldEach}
 
- \subsubsection{ Yield}
- \LMLabel{yield}
+\subsection{ Yield and Yield-Each}
+\LMLabel{yieldAndYieldEach}
+
+\subsubsection{ Yield}
+\LMLabel{yield}
 
 \LMHash{}
- The {\em yield statement} adds an element to the result of a generator function (\ref{functions}).
+The {\em yield statement} adds an element to the result of a generator function (\ref{functions}).
 
- \begin{grammar}
+\begin{grammar}
 {\bf yieldStatement:}
    \YIELD{} expression `{\escapegrammar ;}'
       .
@@ -6384,20 +6456,20 @@ The {\em continue statement} consists of the reserved word \CONTINUE{} and an op
 Execution of a statement $s$ of the form \code{\YIELD{} $e$;}  proceeds as follows:
 
 \LMHash{}
-First, the expression $e$ is evaluated to an object $o$. If the enclosing function $m$ is marked \ASYNC* (\ref{functions}) and the stream $u$ associated with $m$ has been paused,  then execution of $m$ is suspended until $u$ is resumed or canceled.
+First, the expression $e$ is evaluated to an object $o$. If the enclosing function $m$ is marked \ASYNC* (\ref{functions}) and the stream $u$ associated with $m$ has been paused, then the nearest enclosing asynchronous for loop (\ref{asynchronousFor-in}), if any, is paused and execution of $m$ is suspended until $u$ is resumed or canceled.
 
 \LMHash{}
 Next, $o$ is added to the iterable or stream associated with the immediately enclosing function.
 
 \LMHash{}
-If the enclosing function $m$ is marked \ASYNC* and the stream $u$ associated with $m$ has been canceled, then let $c$ be the \FINALLY{} clause (\ref{try}) of the innermost enclosing try-finally statement, if any. If $c$ is defined, let $h$ be the handler induced by $c$. If $h$ is defined, control is transferred to $h$. If $h$ is undefined, the immediately enclosing function terminates.
+If the enclosing function $m$ is marked \ASYNC* and the stream $u$ associated with $m$ has been canceled, then the \YIELD{} statement completes by {\em returning} \code{null} (\ref{completion}), otherwise it completes normally.

[eernst, 2016/10/19 13:37:07]

`returning`

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

Done.

 
 \rationale{
 The stream associated with an asynchronous generator could be canceled by any code with a reference to that stream at any point where the generator was passivated.  Such a cancellation constitutes an irretrievable error for the generator. At this point, the only plausible action for the generator is to clean up after itself via its \FINALLY{} clauses.
 }
 
 \LMHash{}
-Otherwise, if the enclosing function $m$ is marked \ASYNC* (\ref{functions}) then the enclosing function may suspend.
+Otherwise, if the enclosing function $m$ is marked \ASYNC* (\ref{functions}) then the enclosing function may suspend, in which case the nearest enclosing asynchronous for loop (\ref{asynchronousFor-in}), if any, is paused first.
 
 \rationale {
 If a \YIELD{} occurred inside an infinite loop and the enclosing function never suspended, there might not be an opportunity for consumers of the  enclosing stream to run and access the data in the stream.  The stream might then accumulate an unbounded number of elements. Such a situation is untenable. Therefore, we allow the enclosing function to be suspended when a new value is added to its associated stream. However, it is not essential (and in fact, can be quite costly) to suspend the function on every \YIELD{}. The implementation is free to decide how often to suspend the enclosing function. The only requirement is that consumers are not blocked indefinitely.
@@ -6450,7 +6522,7 @@ If the immediately enclosing function $m$ is marked \SYNC* (\ref{functions}), th
 \item It is a dynamic error if the class of $o$ does not implement \code{Iterable}.  Otherwise
 \item The method \cd{iterator} is invoked upon $o$ returning an object $i$.
 \item \label{moveNext} The \cd{moveNext} method of $i$ is invoked on it with no arguments. If \cd{moveNext} returns \FALSE{} execution of $s$ is complete. Otherwise
-\item The getter \cd{current} is invoked on $i$. If the invocation raises an exception $ex$, execution of $s$ throws $ex$. Otherwise, the result $x$ of the getter invocation is added to the iterable associated with $m$.
+\item The getter \cd{current} is invoked on $i$. If the invocation {\em throws} an exception $ex$, execution of $s$ completes in the same way. Otherwise, the result $x$ of the getter invocation is added to the iterable associated with $m$.

[eernst, 2016/10/19 13:37:05]

If I understand this right then `the invocation throws an exception $ex$
(\ref{completion})` should work.

[Lasse Reichstein Nielsen, 2016/10/31 16:54:44]

Reworded since the invocation is an expression, so it's \ref{evaluation}.

 Execution of the function $m$ immediately enclosing $s$ is suspended until the nullary method \code{moveNext()} is invoked upon the iterator used to initiate the current invocation of $m$, at which point execution of $s$ continues at \ref{moveNext}.
 \item
 The current call to \code{moveNext()} returns \TRUE.
@@ -6460,16 +6532,19 @@ The current call to \code{moveNext()} returns \TRUE.
 If $m$ is marked \ASYNC* (\ref{functions}), then:
 \begin{itemize}
 \item  It is a dynamic error if the class of $o$ does not implement \code{Stream}. Otherwise
-\item For each element $x$ of $o$:
+\item The nearest enclosing asynchronous for loop (\ref{asynchronousFor-in}), if any, is paused.
+\item The $o$ stream is listened to, creating a subscription $s$, and for each event $x$, or error $e$ with stack trace $t$, of $s$:
 \begin{itemize}
 \item
-If the stream $u$ associated with $m$ has been paused,  then execution of $m$ is suspended until $u$ is resumed or canceled.
- \item
-If the stream $u$ associated with $m$ has been canceled, then let $c$ be the \FINALLY{} clause (\ref{try}) of the innermost enclosing try-finally statement, if any. If $c$ is defined,  let $h$ be the handler induced by $c$. If $h$ is defined, control is transferred to $h$. If $h$ is undefined, the immediately enclosing function terminates.
+If the stream $u$ associated with $m$ has been paused, then execution of $m$ is suspended until $u$ is resumed or canceled.
+\item
+If the stream $u$ associated with $m$ has been canceled,
+then $s$ is canceled by evaluating \code{\AWAIT{} v.cancel()} where $v$ is a fresh variable referencing the stream subscription $s$.
+Then, if the cancel completed normally, the stream execution of $s$ {\em returns} with no value (\ref{completion}).

[eernst, 2016/10/19 13:37:06]

`returns`

[Lasse Reichstein Nielsen, 2016/10/31 16:54:43]

Done.

 \item
-Otherwise,  $x$ is added to the stream associated with $m$ in the order it appears in $o$.  The function $m$ may suspend.
+Otherwise, $x$, or $e$ with $t$, are added to the stream associated with $m$ in the order they appears in $o$.  The function $m$ may suspend.
 \end{itemize}
-\item If the stream $o$ is done, execution of $s$ is complete.
+\item If the stream $o$ is done, execution of $s$ completes normally.
 \end{itemize}
 
 
@@ -6497,7 +6572,7 @@ The assert statement has no effect in production mode. In checked mode, executio
 
 \LMHash{}
 The expression $e$ is evaluated to an object $o$. If the class of $o$ is a subtype of \code{Function} then let $r$ be the result of invoking $o$ with no arguments. Otherwise, let $r$ be $o$.
-It is a dynamic type error if $o$ is not of type \code{bool} or of type \code{Function}, or if $r$ is not of type \code{bool}.  If $r$ is \FALSE{}, we say that the assertion failed. If $r$ is \TRUE{}, we say that the assertion succeeded. If the assertion succeeded, execution of the assert statement is complete. If the assertion failed, an \code{AssertionError} is thrown.
+It is a dynamic type error if $o$ is not of type \code{bool} or of type \code{Function}, or if $r$ is not of type \code{bool}.  If $r$ is \FALSE{}, we say that the assertion failed. If $r$ is \TRUE{}, we say that the assertion succeeded. If the assertion succeeded, execution of the assert statement is complete. If the assertion failed, the execution {\em throws} an \code{AssertionError} with a stack trace corresponding to the \ASSERT{} statement.

[eernst, 2016/10/19 13:37:07]

`the execution throws .. to the current execution state at the \ASSERT{}
statement (\ref{completion}).`

[Lasse Reichstein Nielsen, 2016/10/31 16:54:45]

Done.

 
 %\Q{Might be cleaner to define it as \code{if (!$e$) \{\THROW{} \NEW{} AssertionError();\}} (in checked mode only).
 %What about an error message as part of the assert?}