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 4b2c5148241d41febb06341bc0767c2e7050a4b4..0bf5577c54ea6063e80a9d955abb959a67a2d4df 100644
--- a/docs/language/dartLangSpec.tex
+++ b/docs/language/dartLangSpec.tex
@@ -1,4 +1,4 @@
-\documentclass{article}
+4\documentclass{article}

[floitsch, 2016/10/10 18:58:15]

typo?

[Lasse Reichstein Nielsen, 2016/10/11 07:52:43]

That, or advanced LaTeX magic - who knows?
(LaTeX knows, fixed).

[eernst, 2016/10/17 16:44:57]

Make it 5.

 \usepackage{epsfig}
 \usepackage{color}
 \usepackage{dart}
@@ -1212,7 +1212,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.

[eernst, 2016/10/17 16:44:56]

Even though it is tempting to add explanatory text like the above, I think that
the intended information is already given at the beginning of
`\subsection{Constructors}` ('[constructors are] used .. to produce objects'),
so I'd recommend that we avoid adding it here, in normative text, and simply
stick to the syntax description, as before.

Other mechanisms like instance methods, getters, setters, and functions are also
introduced by their syntax, and the semantics is specified in detail (usually by
words along the lines of '..the body is executed..') when we get to the point
where the necessary preconditions have been established.

So, in general, "semantic summaries" like this are used quite rarely in
normative text. We could add a bit of semantic summary material to all the
constructs involving execution. but that would make the spec longer and more
redundant.

If we still decide that we want to have these semantic summaries then I think we
should make it explicit that the semantics of the generative constructor
includes allocation, otherwise the words 'freshly allocated' will raise the
question "OK, so how do we allocate it in the first place?".

Also, I find the words 'is executed to initialize' too ambiguous, I'd prefer
something like 'The effect of executing a {\em generative constructor} is to
allocate and initialize a new object', and even then I'd prefer to have the
introduction of the syntax at first, such that we have the generative
constructor "on the table", and then we can say what it does.

PS: Further down the text I can see that the allocation operation has been kept
(deliberately?) hidden, so we may need to search for the right place to put it.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:32]

I want to say something here because it introduces a new mode of execution
(execution to initialize a new object). This is similar to the text written
about statements and expressions describing that they can be executed and
evaluated respectively. A generative constructor can be "executed to
initialize".

That said, it's not saying much, so let's just drop it.


As discussed, the allocation happens below. that's fine with me - the `new`
operator allocates the object, the constructors initialize the new object.

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

Done.

+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:}
@@ -1284,6 +1285,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

[eernst, 2016/10/17 16:44:56]

I think the new text in lines 1288-1297 is redundant: The semantics of an
execution of a redirecting generative constructor is specified later in
`\section{Generative Constructors}` (search for 'If $k$ is redirecting..' line
1360), along with text before and after that point specifying elements that are
shared among multiple kinds of constructors.

We should instead delete the comment in line 1298, which is probably a TODO from
before the text around 'If $k$ is redirecting' was written.

Alternatively, if we wish to include this kind of semantic summary then we could
add a \commentary{} about it. But I think we should be careful about introducing
that kind of redundancy, because it incurs the danger of making the spec
significantly longer.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

I have removed these lines.

 
 
@@ -1324,7 +1335,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.
@@ -1337,43 +1348,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$

[eernst, 2016/10/17 16:44:57]

I think we need to preserve the information about the binding of `\THIS{}`.

I can see that the phrase 'to initialize a fresh instance $i$' plays a different
role here and below: It is a fixed phrase used in connection with the execution
of generative constructors.

The benefit is that this allows for the description to hold a given constructor
and the instance currently-in-construction on the table, such that there can be
a location in the spec where the two of them are brought together, and then we
can describe the execution of several constructors with the same instance (which
is otherwise underspecified, just like the allocation itself).

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

I don't think that's necessary here. The `this` is only in scope inside the
body, and `this` is bound to $i$ there (line 1401).

...
Allocation is specified in the `new` expression section. It's not part of the
generative constructor semantics (so we can execute the super-constructor
without allocating more objects), instead the generative constructor
*initializes* the new object.

If we ever make `new` optional, we probably have to add an initial allocation
step to calling the constructor, separate from its initialization semantics.

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

[eernst, 2016/10/17 16:44:56]

The binding of value parameters are specified elsewhere, but the type parameters
seem to be unspecified. Where is the location where we can say that the type
parameters are taken from the instance creation expression (or from some
arguments to a reflective instance creation operation)?

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

The constructor $k$ is invoked on a type $T$. The $T$ may be a parameterized
class type with type parameters. 

I guess I should add "of the type $T$" above after "generative constructor $k$".

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

Done.

 
 \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,.
 }
 
+

[eernst, 2016/10/17 16:44:57]

No need for two empty lines: No new sections here.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

Acknowledged.

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

Done.

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

[eernst, 2016/10/17 16:44:56]

So here's the answer to the question "where does it get allocated in the first
place?", but the '%' explains why we can't find it by searching the generated
PDF.

If we never mention it then we won't get in trouble with multiple unwanted
occurrences of the allocation. Otherwise, making it part of the execution of a
generative constructor makes it pop up below: 'the super constructor call .. is
now executed', i.e., we'll perform allocation many times, each time of the
enclosing class of that constructor. Or we need to say "by the way, _those_
constructor executions do not involve allocation of a fresh instance, they'll
continue to work on the one we created in the "original" constructor execution".

In order to clean up this issue, we could choose to make the allocation a
completely separate action, with no connection to the execution of a generative
constructor.

It could be a side effect of the evaluation of a `new` expression. In that case
there is no conflict between "executing a constructor with and without
allocation". We still don't really know what it means to allocate a fresh
instance of a given class because, as is the traditional C++ point of view,
which makes sense here, too: the 'fresh instance' is just a memory area, it's
not yet an instance of any class. So we would then need to talk about the size
of instances of a class, at least as "something that is defined" even if we
don't want to specify how to compute the exact size.

I believe that new instances are _only_ allocated during evaluation of `new`
expressions and as part of reflective constructor invocation. Given that
reflection is described only briefly in the specification, we should be OK as
long as we just mention the allocation with `new`.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

It *is* a side-effect of evaluating a `new` expression (line 3380).

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

[eernst, 2016/10/17 16:44:57]

OK, so this is now uncommented, and that's an improvement because it used to be
omitted (I couldn't find any other location about it, at least).

I guess the 'compile-time constant' stuff was very old..

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

The initialization of fields were also done in the `new` operator, although not
in a way that actually worked.

+
 %Next, a

[eernst, 2016/10/17 16:44:55]

We might as well delete this line.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

We could delete all the comments.
A few might me relevant, but they are still in the git history.

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

Done.

 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.

[eernst, 2016/10/17 16:44:56]

This sounds like we'll evaluate the initializing expressions in the declaration
first, then the ones in the initializer lists, and possibly initializing `final`
fields twice, or just ignoring one of the values.

The tools do not agree: `dart2js` says 'Field 'x' is initialized more than
once.' and stops with a compile-time error. The vm is happy about the program,
runs the declaration initializer once and the one in the initializer list twice,
and then says 'Class 'C' has no instance setter 'x=''. ;-)


So we should make a decision and specify it here. I created an issue for that
discussion.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

This only refers to the initializers in the initializer list.
The ones for class fields are not initializers of $k$ and
Initializing formals are not initializers, so the initializer list is the only
thing left.
Maybe it should be made more clear. Reworded.

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

[eernst, 2016/10/17 16:44:56]

We should strive to specify each property only once, and otherwise refer to the
place where it is already specified:

'Then, for each instance variable $v$ of $i$ declared by the immediately
enclosing class which is not yet bound to a value, it is a dynamic error if $v$
is \FINAL{}.

\commentary{For the remaining (non-\FINAL{}) variables, the initial value is
\NULL{} (\ref{variables}).}'

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

I don't see the rewrite as better than what's already there.

That commentary would make it sound like the variables are already initialized
with `null`, which they aren't. 

The way I have written it, all class fields are initialized at least once, and
final fields exactly once.
I treat "binding the variable to a value" as an imperative step. Before doing
that binding, the variable has no binding. This distinguishes a variable with no
binding from one with `null` as value. Moving the `null` value to a commentary
basically leaves some fields unbound.

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

[eernst, 2016/10/17 16:44:57]

This is the place where it really helps to mention $i$!

I believe the most direct form, using the existing specification of the
superinitializer would be something like this:

'Then, unless the enclosing class is \code{Object}, the explicitly specified or
implicitly added superinitializer (\ref{initializerLists}) is executed to
further initialize $i$.'

We will get the binding of `\THIS{}` recursively by just saying that we execute
that superinitializer, but we do not specify the implicitly passed type
parameters. This is one of the locations where that should be specified (for
instance, declarations like `class D<X, Y> extends C<int, Y, List<X>> ..`
illustrate that there is something to say).

+
+\commentary{
+The super constructor call can be written anywhere in the initalizers 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

[eernst, 2016/10/17 16:44:57]

Seems more clear to use 'initializer list', because it's obvious how to
understand the end of a list (otherwise, we might append it to each initializer
;-).

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

Acknowledged.

+because the argument expressions may have visible side effects
+which must happen in the order the expressions occour in the program text.

[floitsch, 2016/10/10 18:58:15]

occur

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

Acknowledged.

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

[eernst, 2016/10/17 16:44:56]

I believe we should say 'After the superinitializer has completed' in order to
avoid introducing the notion of 'superclass constructors' in normative text. It
follows from the wording above that the execution of one superinitializer
includes recursive invocation of the rest, up to `Object`.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

Good point.

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

[eernst, 2016/10/17 16:44:56]

It's probably simpler if we avoid introducing yet another concept ("executing an
initializer to initialize an object"), but we could say: 'During the execution
of a generative constructor to initialize an instance $i$, execution of an
initializer ..'.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

ACK

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

Done.

 
 \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$}.
@@ -1389,12 +1424,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:

[eernst, 2016/10/17 16:44:58]

I'd prefer avoiding to introduce 'remember' as a normative concept. We could say
that the argument list 'is evaluated, yielding a set of bindings $B$.'

The specification uses phrases like 'bindings that resulted from the evaluation
of the argument list' many times, but that is of course ill-defined because it
takes both an actual argument list and a formal parameter list to provide the
information that goes into a set of bindings (if we ignore the formal parameter
list then we cannot bind an actual argument value to the proper name which is
required for the body to be able to use that argument).

But let's fix that in a separate CL, and then use the "usual" imprecise phrase
here.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

I believe "binding" refers to the result of applying actual arguments to a
formal parameter list. Here we only evaluate the actual arguments, we do not
bind them yet (which is important, since the binding may contain initializing
formals, and must happen after field initializers).
Exactly.
I don't think it applies here, but I'll check if it would be no more wrong than
other occurrences.

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

Actually, I don't think the binding of formal variables includes the handling of
initializing formals anyway. That's handled explicitly by this section based on
the existing binding of formal variables.
So, let's just say that we create a binding here and use it later.

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

[eernst, 2016/10/17 16:44:58]

'..with respect to the bindings $B$, and the type parameters..'

This falsely specifies that we use the same type arguments for the constructor
$S$/$S.id$ as we did for the current constructor. In reality, we need to
transform the type arguments as implied by the `extends` clause (for instance,
with `classC<E> extends B<List<E>> ..` and `class B<F> ..`, we need to transform
`E --> U` to `F --> List<U>`).

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

No, the U_1 .. U_m *are* the type parameters of the *superclas* as specified in
the superclass/extends clause of the class declaration. That's what line 1430
says.

At this point we remember the supertype (superclass plus type parameters), the
construtor name and the constructor arguments.

At a later point we execute that constructor of that type with those arguments
to initialize $i$.

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

It's still suspicious that we talk about the "Actual type arguments" ( a dynamic
property) of the superclass clause (a syntactic entity).
I'm not going to fix that in this CL, but it's probably worth looking into.

 
 \LMHash{}
 It is a compile-time error if class $S$ does not declare a generative constructor named $S$ (respectively $S.id$).
@@ -1427,7 +1463,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}
@@ -2338,6 +2373,15 @@ The constant expression given in an annotation  is type checked and evaluated in
 \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}).
 
+Expressions can also {\em throw} an exception object and an associated stack trace.

[Kevin Millikin (Google), 2016/10/13 08:38:28]

I suggest a more radical rewrite of this section.  It should say up front that
there are two possibilities, and then provide specific details of the two.  It
should be clear that the two possibilities are mutually exclusive (say "or else"
instead of "or").  The two possibilities should use parallel language wherever
possible.

As it is, the detail "Every expression has an associated static type" is lumped
in with yielding a value, but that detail is true of expressions that throw
exceptions as well so it should appear where both outcomes are discussed.

The terminology "yield a value" is unfortunate.  I think we need to go with
something more like "produce a value".  Though note that elsewhere we simply use
"evaluates to" so we could simply have that expressions evaluate to a value or
else throw an exception.

The emphasis is inconsistent --- why emphasize 'value' but not 'exception'?  Why
emphasize 'throw' but not 'yield'?

[Lasse Reichstein Nielsen, 2016/10/17 10:08:22]

Rewritten completely. Changed "yield" to "produce" everywhere(?) it refers to
evaluation of an expression.

The emphasis is inconsistent.
I don't want to emphasize a long sentence part like "throws an exeception object
and an associated stack trace", so I now just emphasize "throws".
On the other hand, just emphasizing "produces" seems weird without "a value".

Maybe it's just because I'm used to using "throws" intransitively, but not
"produces". Better ideas appreciated.

+
+Evaluation of an expression will always either {\em yield a value} or it will {\em throw an exception} along with an associated stack trace.
+
+If evaluation of an expression is defined in terms of evaluation of another
+expression, and the evaluation of the other expression throws an exception,
+if nothing else is stated, the evaluation of the first expression stops
+at that point and throws the same exception.

[eernst, 2016/10/17 16:44:58]

Aha, here is the congruence rule! (I was waiting for that when I saw '$e$ is
evaluated to an object $o$' in line 1411).

However, I'd prefer to introduce completion immediately, in order to keep
closely related concepts together at their introduction. Maybe the following
could be used:

'An {\em expression} is a fragment of Dart code that can be evaluated at run
time. The evaluation may {\em complete with a value}, which is always an object,
or it may {\em complete with an exception}, which amounts to {\em throwing an
object and a stack trace}.

Every expression has an associated static type (\ref{staticTypes}). Every value
has an associated dynamic type (\ref{dynamicTypeSystem}).

We need to introduce a general rule to specify propagation of exceptions in
expression evaluation: Whenever the evaluation of an expression $e$ is specified
to include evaluation of a set of subexpressions $e_1\ldots{}e_k$ in that order,
if the subexpression $e_i$ is evaluated and completes with an exception throwing
the object $o$ and the stack trace $s$, $e$ itself completes by throwing $o$ and
$s$, without evaluating the remaining subexpressions $e_{i+1}\ldots{}e_k$, if
any.'

We don't even need to say 'if nothing else is stated' here, because `try` is a
statement, not an expression.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

Acknowledged.

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

We won't use "complete" for expressions.
I have tried making the emphasis more consistent.

I also don't want to talk about evaluating multiple expressions in any order.
That's exactly the kind of non-compositionality that causes problems (it fails
to recognize that evaluation might do other things between evaluating
expressions that can also throw).
It might not be the case currently, but I would prefer to not depend on that. 

I have removed the "unless otherwise stated" for now, that's easy to add if it
becomes necessary.

+

[eernst, 2016/10/17 16:44:57]

Typo: Spurious empty line.

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

Done.

 
 \begin{grammar}
 
@@ -3044,10 +3088,7 @@ 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$.
@@ -3057,32 +3098,16 @@ There is no requirement that the expression $e$ evaluate to a special kind of ex
 }
 
 \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 $e$ evaluates to \NULL{} (\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 aborts by {\em throwing} with $e$ as exception object and $t$ as stack trace.

[eernst, 2016/10/17 16:44:56]

We might as well have a newline per sentence here. For the second sentence, the
following would follow the terminology I suggested earlier more closely:

'Otherwise, the \THROW{} statement completes with an exception, throwing the
value $v$ and a stack trace that corresponds to the current execution state.'

I removed the `\em` on throwing because that word has been introduced earlier
(and 'throwing' is something that happens both at `throw` and later at
propagation, so it's not unnatural to tie it up to the general introduction of
expression evaluation, where it is needed anyway).

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

Added newlines, removed emphasis. Changed ref to {evaluation} since this is an
expression, not a statement.

 
 \LMHash{}
-If $f$ is synchronous (\ref{functions}), control is transferred to the nearest dynamically enclosing exception handler.
+If $e$ is an instance of class \code{Error} or a subclass thereof, its \code{stackTrace} getter will return the stack trace captured at the point where the object was first thrown.
 
 \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.
+If the same \code{Error} object is thrown more than once, its \code{stackTrace} getter will return the stack trace captured the {\em first} time it was thrown.
 }

[eernst, 2016/10/17 16:44:56]

I think this text should remain normative (interpreting it as a new version of
the sentence previously in line 3083).

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

The previous paragraph (which has since been rewritten) corresponds to line
3083, this is commentary explaining what that paragraph means.

 
 \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.
-}
-
-\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$.
 
 
@@ -3344,7 +3369,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  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.
 
 \LMHash{}
 Otherwise, if $q$ is a generative constructor (\ref{generativeConstructors}), then:
@@ -3352,14 +3377,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.}

[eernst, 2016/10/17 16:44:56]

Could fix typo: 'at this point'.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

Done.

 
 \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{}.
+A fresh instance (\ref{generativeConstructors}), $i$, of class $R$ is allocated.

[eernst, 2016/10/17 16:44:57]

Aha, so we should definitely simply delete the commented-out sentence in line
1370! Then we _do_ have that approach where `new` does the allocation, and
constructors have nothing to do with that.

It's _really_ nice to have the initializer stuff in the right place now!

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

The allocation was always done here. Previously the field initialization was
also done here, badly.

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

[eernst, 2016/10/17 16:44:57]

The binding stuff is still a mess, but this is probably safer:

'.. with the formal parameter bindings that resulted from the evaluation of the
argument list ..'.

If we make sure that formal parameter binding operations always refer to
'bindings' then it's easier to find & fix this issue later on.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

Again I don't think that applies because the actual binding happens later, after
initializing fields, and it will handle initializing formals.
Or maybe I'm wrong. I'll check :)

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

I'm wrong. Reworded to be consistent with other similar sections: "with respect
to the bindings that resulted from the evaluation of  ...."

 
-\commentary{
-Observe that \THIS{} is not in scope in $e_f$. Hence, the initialization cannot depend on other properties of the object being instantiated.
-}
-
-\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$.

[eernst, 2016/10/17 16:44:56]

This is a very special situation, because we cannot say that $q$ completes
normally 'with the value $o$'. This means that the congruence rule in the
comment on line 2383 does not apply directly (because there is no constructor
invocation _expression_). So I'd suggest that we make it explicit here:

'If execution of $q$ completes normally then the evaluation of $e$ completes
normally with the value $i$; if it completes with an exception then the
evaluation of $e$ completes with the same exception.'

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

That's mixing expressions and statements. A statement can "complete normally"
and an expression can "evaluate to a value". You can't complete normally with a
value.

If execution of the constructor as an initializer completes normally (like a
statement), then the `new` expression evaluates to $i$.
If the constructor throws, so does the expression.

Function calls are expressions which contains statements, and for a generative
constructor, I actually treat the invocation as a statement, not an expression.
Maybe that should be made explicit/

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

No explicitly propagates exception from execution to evaluation, since
\ref{evaluation} doesn't handle that implicitly - it only handles
sub-expressions, not sub-executions (generative constructor invocation is
actually neither, but I treat it as a function invocation, and function
invocations are underspecified too)

 
 \LMHash{}
 Otherwise, $q$ is a factory constructor (\ref{factories}). Then:
@@ -3367,11 +3388,15 @@ 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.

[eernst, 2016/10/17 16:44:56]

Reword to work for the general case, not just this situation where it motivates
an update ('We cannot make every cyclic execution an error because ..').

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

Not sure what you are asking for.

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

[eernst, 2016/10/17 16:44:57]

We definitely need to have a comma here: '..argument list, and..'.

Actually: '..argument list, and with the type parameters..' would work better,
because then we have 'with respect to .. bindings' and 'with type parameters ..
bound'.

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

Done.

+If this execution {\em returns} or {\em completes normally} (\ref{completion}),
+let $i$ be the value {\em returned} by this execution, or \NULL{} if the execution returns without a value or it completes normally.
+The result of the evaluation of $e$ is $i$.

[eernst, 2016/10/17 16:44:55]

Isn't a factory constructor a function that returns a value? Certainly,
\ref{factories} uses phrases like 'the return type of a factory' and 'a factory
returns'.

Then why not just stick to 'If this execution completes with the returned value
$o$ then the evaluation of $e$ completes normally with the value $o$; if it
completes with an exception, evaluation of $e$ completes with the same
exception'.

The reason for including both types of completion is the same as previously: We
hit a generative constructor, so the general propagation rule for expressions
doesn't apply (a similar rule for statements wouldn't apply, either).

(To 'complete with returned value' is introduced below.)

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

A non-redirecting factory constructor is basically a function.
Still, we are invoking it with `new`, not using function call, so we need to
duplicate the function-call semantics here as well (I think).
Yes, it's similar to a function, but it is not a function, and it's not written
as "equivalent to the function declaration .... and calling that function".
Because we also have to handle the cases where it completes normally (at least
if I remove the implicit "return;" statement added to functions) and where it
returns without a value, which both means the same as `return null;`.
It doesn't come for free since we are not calling a function, we are executing a
body directly.
Actually not. This is a non-redirecting factory constructor, so we won't hit any
generative constructor. We are executing a body, which is a block statement, so
we have to handle statement completion in general, including completing normally
and returning with no value.

 
 \LMHash{}
 It is a static warning if $q$ is a constructor of an abstract class and $q$ is not a factory constructor.
@@ -3535,16 +3560,16 @@ 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.
+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 execution of $f$ completes (\ref{completion}). If $f$ completes by {\em returning} a value, that value used to complete $o$, if it {\em completes normally} or by {\em returning} with no value, $o$ is completed with \NULL{}, and if it completes by {\em throwing} an exception $e$ and stack trace $t$, $o$ is completed with $e$ and stack trace $t$ as an error.

[eernst, 2016/10/17 16:44:55]

I'd suggest that we avoid the concept of completing without a value.
Implementations (`dart2js` and `dart`) agree that `void f() { return; }` and
`void g() {}` both return `null` dynamically, and we discussed returning
whatever-you-want in a `void` function, so we are well-situated to simply
declare that there is a return value in all cases.

So we could do this:


'.. If the execution of the body of $f$ completes normally with the value $v$
then the future $o$ completes to $v$; if it completes with an exception then the
future $o$ will complete to the same exception.'

I searched a bit for the terminology used with future completion, and 'complete
to' seems to exhibit a reasonably clear difference to 'complete with' that we've
used for expressions and now functions.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

I considered doing that, but Kevin actually liked having the distinction, so I
decided to keep it.
I don't mind having the distinction between returning with and without a value -
it's one more case to handle at the end of a function body, but that's not bad
(since it can be lumped with the "completes normally" case).
Mixing expressions and statements. "Complete normally" applies to statements,
"with a value" is for expressions. Unless we introduce a new generalizing
concept of "completes normally with a value" which combines "returns value",
"returns without value" and "completes normally".

I'm not sure that's worth it, we only return from functions in so many places.

 
 \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:
+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$ completes:
 \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:
+\item If $f$ {\em completes normally}, then if $s$ has been canceled then its cancellation future is completed with \NULL{} (\ref{null}).

[eernst, 2016/10/17 16:44:57]

I think we should reserve `{\em ..}` for introductory occurrences of terms (or
non-normative text where ordinary textual emphasis may be useful). In this case,
'completes normally' is not introduced.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

Are you sure it's not worth emphasizing that this is a term of art defined
elsewhere, and not just prose?
I *think* it's easier to read correctly with the emphasis, but since I wrote it,
I'm not an objective observer.

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

Done.

+\item If $f$ {\em throws} exception $e$ and stack trace $t$:

[eernst, 2016/10/17 16:44:56]

Keeping the usual phrases for this, we would have 'If $f$ completes with an
exception throwing the object $o$ and stack trace $t$:'

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

I don't think "completes with an exception" is defined.

I have reworded it, so throwing is one of the five ways of completing.
It would be either:
 If $f$ completes by throwing an exception object $o$ and stack trace $t$.
or 
 If $f$ throws an exception object $o$ and stack trace $t$.

   \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.
+  \item $e$ and $t$ are added to $s$ as an error.
+  \item If $s$ has been canceled then its cancellation future is completed with $e$ and $t$ as an error.

[eernst, 2016/10/17 16:44:55]

$e$ would now be $o$, twice.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

I think I'll keep using $e$ for the error.

   \end{itemize}
 \item $s$ is closed.
 \end{itemize}
@@ -3553,12 +3578,6 @@ If $f$ is marked \ASYNC* (\ref{functions}), then a fresh instance $s$ implementi
 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.
-
-\rationale{Such streams may be left open by for loops that were escaped when an exception was thrown within them for example.
-}
-
 %\LMHash{}
 %When a stream is canceled, the implementation must wait for the cancelation future returned by \cd{cancell()} to complete before proceeding.
 
@@ -3578,7 +3597,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 $f$ completes (\ref{completion},
+\begin{itemize}
+\item If $f$ {\em completes normally}, $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.

[eernst, 2016/10/17 16:44:58]

'If $f$ completes normally with the value $v$, $v$ is ignored and $j$ is
positioned after..'.

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

Not using that phrasing.

+\item If $f$ {\em throws} exception $e$ and stack trace $t$ then the current value is \NULL{} and the current call to \code{moveNext()} throws $e$ and $t$ as well. Further calls must return false.

[eernst, 2016/10/17 16:44:55]

'If $f$ completes with an exception then a call to \code{moveNext()} must
complete with the same exception, and the current value must be \NULL{}. Further
calls to \code{moveNext()} must return false.'

I guesstimated that the further calls would be to `moveNext()`, but since that
wasn't immediately obvious I think we should make it explicit.

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

Done.

+\end{itemize}
 
 Each iterator starts a separate computation. If the \SYNC* function is impure, the sequence of values yielded by each iterator may differ.
 
@@ -3599,19 +3622,20 @@ Two executions of an iterator interact only via state outside the function.
 
 
 \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.
-
-
-\LMHash{}
-Execution of $f$ terminates when the first of the following occurs:
-\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.
-\end{itemize}
-
-
+If $f$ is synchronous and is not a generator (\ref{functions}) then execution of the body of $f$ begins immediately.
+When $f$ completes (\ref{completion}) by returning a value, that value is returned to the caller.
+If $f$ completes by returning without a value or by completing normally, \NULL{} is returned to the callse.
+If $f$ completes by {\em throwing}, the invoking call expression throws the same exception object and stack trace.

[eernst, 2016/10/17 16:44:57]

Following the same style we would have something like this (I replaced 'when' by
'if' because it may not terminate at all):

'If the execution of the body of $f$ completes (\ref{completion}) normally with
a value $v$ then the function invocation completes normally with the value $v$.
If the execution of the body of $f$ ends because the last statement has
completed normally, the function invocation completes normally with the value
\NULL{}.
If the execution of the body of $f$ completes with an exception throwing the
object $o$ and stack trace $s$, the function invocation completes with the same
exception $(o, s)$.'

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

The "last statement" shouldn't need to be mentioned. If the body completes
normally, it is because the last statement (if any) has completed normally, but
that's not really important. You don't need to worry about which statement is
last.

 
+\commentary{
+A function body can never {\em abort} by {\em breaking} or {\em continuing}
+because any \BREAK{} or \CONTINUE{} statement must occuring inside 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 abort by {\em throwing}, so an
+expression can represent the behavior of a function body.

[eernst, 2016/10/17 16:44:56]

I know this is commentary, but I think there are too many `\em`s, and there are
also a couple of other issues. Here's a possible revision:

'A function invocation can never abort at \BREAK{} or \CONTINUE{} because it is
a compile-time error for these statements to occur anywhere else than inside an
enclosing statement $S$ that handles them.
This is either because $S$ is a labelled statement with the same label, or
because the given \BREAK{} or \CONTINUE{} does not have an associated label, and
$S$ is a \SWITCH{} statement or a loop.

This means that the only possible ways for the execution of the body of a
function to end is (1) completing normally with a value, and (2) completing with
an exception. This is a set of completion modes that expressions support, so it
can be directly transferred to the function invocation.'

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

ACK. I'm actually considering moving this to the \ref{statements} section - 
maybe it's possible to define function body execution in a general way, so I
won't have to handle the
complete-normally/return-with-value/return-without-value -> invocation evaluates
to value/null for each type of invocation.
  

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

REmoved \em's. Reworded.

+}
 
 \subsubsection{ Actual Argument List Evaluation}
 \LMLabel{actualArguments}
@@ -5011,15 +5035,21 @@ Evaluation of an await expression $a$ of the form \AWAIT{} $e$ proceeds as follo
 First, the expression $e$ is evaluated. 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 $e$ evaluates to an object $o$ that 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 the result of evaluating $e$.

[eernst, 2016/10/17 16:44:56]

I'd prefer if we keep all completion situations explicit, because we need to
make it very easy to discover the locations where the exception propagation
applies. Here's a possible way to do that:

'If the evaluation of $e$ completes normally with a value $o$ which is not an
instance of \code{Future} then ..[same]..; otherwise let $f$ be $o$.'

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

I have trouble parsing that. I read it as:

 if (e evaluates to a value o that is not Future) { 
   let f = new Future.value(o) 
 } else { 
   let f = o
 }

but o is not in scope in the else branch.

Kept (almost) as written.

 
 \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. Execution of the function $m$ 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 exception $x$ and stack trace $t$, $a$ {\em throws} $x$ and $t$. If $f$ completes with a value $v$, $a$ evaluates to $v$.

[eernst, 2016/10/17 16:44:56]

OK, we discussed a while back how to interleave these suspend/pause events. I'll
leave it to others to have strong opinions about it and just note that it is
being done here. 

However, it would be useful to make sure that the change is documented in a
dart-lang-evolution issue -- which may or may not be the case already, but I
couldn't immediately spot it.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

It's not, good point.
It should be possible to describe this idea behind behavior in more readable
terms, without all the details needing to there.

 
 %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{
@@ -5424,6 +5454,29 @@ The static type of a cast expression  \code{$e$ \AS{} $T$}  is $T$.
 
 \section{Statements}
 \LMLabel{statements}

[eernst, 2016/10/17 16:44:56]

Missing empty line, then missing `\LMHash{}` for the next paragraph.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

But why?
I.e., hat are the rules for using LMHash - why must there be an empty line
before (and why is LMLabel not introducing a hash automatically)?

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

[eernst, 2016/10/17 16:44:57]

It's a smart phrase, 'Statements, unlike expressions, do not..' but it still
seems twisted. Maybe a small change to 'Unlike expressions, statements do not..'
would make it more smooth to read.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

Acknowledged.

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

The more I think about it, the less I agree.
We are talking about statements, so starting the sentence with "expressions" is
less direct.

+Some statements can affect control flow, in particular \BREAK{}, \CONTINUE{}, \RETURN{} and \THROW{} statements.

[eernst, 2016/10/17 16:44:57]

Function invocations do affect the control flow as well, even though they'll
(often) return to "nearly the same spot". Logical operators with short-cut
semantics affect the control flow as well, as do loops etc.

So we definitely need to admit that the listed statements aren't the only ones.
But maybe they are the only ones that work like a structural variant of regular
GOTO statements? Maybe they are special in that they affect the control flow by
jumping to something which is _not inside_ the construct itself.

We could then say 'Some statements can affect control flow in a way that isn't
confined to the statement itself, in particular..', which still lets `?:`,
`switch` etc. do their thing without forcing us to mention them here.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

Good point.
I'm exactly talking about the things that affect control flow when control comes
*out* of the statement/expression.

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

I have reworded considerably, this sentence is now gone.

+
+\LMLabel{completion}

[eernst, 2016/10/17 16:44:57]

It breaks the rules to have an \LMLabel{} which is anywhere else than
immediately after a sectioning command. That's because it produces a label that
refers to the "current number", which is otherwise the number of the section as
shown in the \tableofcontents and used in all the occurrences of
`(\ref{whatever})`. So in this case it would just cause `\ref{completion}` to
work exactly like \ref{statements}.

So we need to introduce a new section/subsection/.. in order to have something
to refer to. This would make sense anyway, because completion occurs all over
the place.

That subsection would then refer to the (beginning) of the sections
\ref{statements} and \ref{expressions} etc., wherever we have something about
completion, after giving a brief introduction to the underlying ideas.

This location would then just have the normal \LMHash{} for each normative
paragraph.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

Is it a problem to have two labels for the same section?
I know that the \ref will print the same section number, but I like being able
to be more precise in the reference. If I ever move this to a subsection, it
will still make sense, and I won't have to separate the \ref{statement} into
those that refer to one and those that refer to the other.
Currently, I think this section is too short to be a sub-section by itself, but
I'm not absolutely convinced. If I add more text about function bodies, then I
think it should be a subsection.

+Execution of a statement can {\em complete} in two ways: either it {\em completes normally} or it {\em aborts}. It can {\em abort} in one of four ways: Either it {\em breaks} or it {\em continues} (either to a label or without a label), it {\em returns}, either with a value or without one, or it {\em throws} an exception object and an associated stack trace.

[eernst, 2016/10/17 16:44:57]

It is tempting to use these short-hands, but I still think it would be useful to
strictly make completion explicit. We could do it like this:

'Execution of a statement can {\em complete} in several ways, also known as {\em
completion modes}:
\begin{itemize}
\item It can {\em complete normally}.
\item It {\em complete with a \BREAK{}} or {\em with a \CONTINUE{}}, optionally
{\em to a label}.
\item It can {\em complete with a returned value}.
\item It can {\em complete with an exception}, which amounts to {\em throwing an
object and a stack trace}.
\end{itemize}

In all cases except normal completion, we say that the statement {\em completed
by aborting} or that it {\em aborted}.

\commentary{
Note that aborted execution does not imply that anything went wrong, it just
means that execution continues somewhere else than the next statement.
}'

As usual, I've put the emphasis on making 'complete' explicit, and I've reserved
two levels of detail for the exception: The exception as two named entities
(both an object thrown and a stack trace captured) and the two parts as a whole
(when we don't need to talk about the parts).

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

This has been rewritten already.
Also, as discussed, making the completion explicit doesn't necessarily require
writing "completion". The new text just uses "throws" instead of "completes by
throwing", but it's still defined the same way.

+
+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 {\em aborts},
+then, unless otherwise stated, the execution of $s$ stops
+at that point and aborts 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.

[eernst, 2016/10/17 16:44:57]

I'm not so happy about introducing any 'default' mechanisms here, or about
placing examples in normative text. I think we can avoid this using the same
style as with expressions (so this is a proposal for text that replaces all of
lines 5463-5477):

'We need to introduce a general rule to specify propagation of completion modes
in statement execution:
Whenever the execution of a statement $S$ is specified to include execution of a
set of immediately enclosed statements $S_1\ldots{}S_k$,
if the statement $S_i$ is executed and aborts then $S$ aborts in the same way.
Whenever the execution of $S$ is specified to include the evaluation of an
immediately enclosed expression $e$, if this evaluation completes with an
exception then $S$ completes with the same exception. This rule does not apply
in all cases, but every exception to the rule is specified explicitly.

\commentary{
For instance, if the body of a loop completes with a \BREAK{} without a label
then that loop will complete normally, rather than propagating the breaking
completion.
}'

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

Seems reasonable, although doing the S_1 .. S_k seems overkill, and not
consistent since it doesn't say anything about multiple expressions, or the
interleaving of expressions and statements (for-statements contain multiple
expressions - although they might be the only ones).

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

Kept the existing text mostly unchanged. Getting into talking about multiple
statements or expressions at the same time leads to having to consider
interleaving and ordering, which is strictly worse than just talking about one
at a time.

I don't like the lead-in "we need to" (To channel Yoda: Do or do not, there is
no "need to").

Moved examples to end of paragraphs.

+
+\LMHash{}

[eernst, 2016/10/17 16:44:56]

We haven't otherwise used \LMHash{} markers on grammar blocks, so I'd suggest
that we keep putting \LMHash{} on natural language paragraphs, and only there.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

What is the purpose of LMHash markers?
I am thinking of it as a way to split the file into separate sections, roughly
by subject, so it's easy to see which sections have changed and which have not.
Here I consider the section before the grammar and the grammar to be quite
different in subject, so I want them seprated.

 
  \begin{grammar}
 {\bf statements:}
@@ -5459,7 +5512,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:
@@ -5470,10 +5523,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.
 

[eernst, 2016/10/17 16:44:57]

Just for consistency, let's keep 2 empty lines before sections.

[Lasse Reichstein Nielsen, 2016/10/19 14:34:30]

Acknowledged.

-
-
- \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.
@@ -5600,15 +5651,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
@@ -5695,7 +5745,13 @@ The expression $[v^\prime/v]c$ is evaluated and subjected to boolean conversion
 \item
 \label{beginIteration}
 The statement $[v^\prime/v]\{s\}$ is executed.
-\item
+
+If this execution {\em continues} without a label,
+or with a label that this \FOR{} statement is labeled with (\ref{labels}),
+then the statement is treated as if it had completed normally.

[eernst, 2016/10/17 16:44:57]

'If this execution completes with a \BREAK{}, without a label or with a label
that this \FOR{} statement is labeled with (\ref{labels}), then the \FOR{}
statement completes normally. If this execution completes with a \CONTINUE{},
without a label or with a label that this \FOR{} statement is labeled with, then
the execution of this \FOR{} statement continues at step \ref{beginIteration}.'

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

If the body continues the loop, then it's equivalent to the body completing
normally. It's incorrect to goto beginIteration here, you need to go to the
evaluation of the increment-part (the third part of the for-statement) below.
(A continue of a loop is always equivalent to breaking the body statement, so
it's equivalent to the body completing normally).

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

Reworded.

+If it aborts in any other way,
+execution of the for loop stops and aborts in the same way.

[eernst, 2016/10/17 16:44:57]

'

\commentary{
If it aborts in any other way then the \FOR{} statement aborts in the same way,
following the general propagation rule.
For instance, it could complete with a returned value or with an exception.
}'

[Lasse Reichstein Nielsen, 2016/10/19 14:34:31]

That, or remove it.

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

Removed.

+
 \label{allocateFreshVar}
 Let $v^{\prime\prime}$ be a fresh variable.  $v^{\prime\prime}$ is bound to the value of $v^\prime$.
 \item
@@ -5739,8 +5795,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}
 
@@ -5748,22 +5802,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}. 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 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 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}).
+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{}
-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.
+For each {\em data event} from $u$,
+the statement $s$ is executed with \code{id} bound to the value of the current data event.
 
-\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 another event $e_u$ of $u$ occurs before execution of $s$ is complete, handling of $e_u$ must wait until $s$ is complete.
+
+\LMHash{}
+If execution of $s$ {\em continues} with no label, or with a label that prefixes the asynchronous for statement (\ref{labels}), then the exection of $s$ is treated as if it had completed normally.
+
+If execution of $s$ {\em aborts} in any other way, 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$ aborts in the same way as the exeution 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 it aborts the asynchronous for
+loop. That should never happen for a correctly implemented stream.
 }
 
 \LMHash{}
+On the first {\em error event} from $u$,
+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.}
@@ -5782,10 +5879,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$.
+
+If $r$ is \TRUE{}, then the statement $\{s\}$ is executed.
+If that execution 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.
+
+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}.
@@ -5808,7 +5910,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 exection 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}.
@@ -5819,7 +5926,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
     .
@@ -5908,13 +6015,13 @@ 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}$.
+Next, the case clause \CASE{} $e_{1}: s_{1}$ is matched against {\code id} if it 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}).
 
 \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.
 
 \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$) \{
@@ -5925,16 +6032,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:
 
 \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$.
+If $v$ is not \TRUE{} the following case, \CASE{} $e_{k+1}: s_{k+1}$ is matched against {\code id} if it exists. If \CASE{} $e_{k+1}: s_{k+1}$ does not exist, then the \DEFAULT{} clause's statements are executed (\ref{case-execute}).
+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$) \{
@@ -5944,19 +6050,56 @@ 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:
 
 \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$.
+If $v$ is not  \TRUE{} the following case,  \CASE{} $e_{k+1}: s_{k+1}$ is matched against {\code id} 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 (\ref{case-execute}).
+
+\LMHash{}
+\subsection{ Executing the statements of a switch case}
+\LMLabel{case-execute}
+Execution of the statements $s_h$ of 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$
+\}
+\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 statments of the last case of the switch ($h = n$ if there is no \DEFAULT{} clause, $h = n+1$ if thre is a \DEFAULT{} clause), then the execution of the switch case aborts by throwing a runtime 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\}$ aborts by {\em breaking} 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\}$ aborts with a continue 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.
+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 leth $h = n$.
+The statements $s_h$ are then executed (\ref{case-execute}).
+
+If execution of $\{s_h\}$ aborts in any other way, execution of the \SWITCH{} statement aborts in the same way.
+
 \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.
 
@@ -6013,25 +6156,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 aborts by {\em throwing} with $p_1$ as the exception object and $p_2$ as the stack trace.

[Lasse Reichstein Nielsen, 2016/10/11 07:52:43]

Another option, and probably more consistent, is to introduce "rethrows" as a
way for statements to complete, and then in the catch body evaluation, if it
completes by rethrowing, throw with the exception and stack that was used to
enter the catch body. Those values will still be logically in scope at that
point.
WDYT?

 
 \LMHash{}
 It is a compile-time error if a  \code{\RETHROW{}} statement is not enclosed within an \ON-\CATCH{} clause.
 
 
-
 \subsection{ Try}
 \LMLabel{try}
 
@@ -6057,10 +6187,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, one or two exception parameters and a block statement.
 \item
 A \FINALLY{} clause, which consists of a block statement.
 \end{enumerate}
@@ -6070,115 +6200,76 @@ 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.
 
-
 \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.
 
 \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}
+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 indentifier that does not occur anywhere else in the program.
 
- \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.
-
- % 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$ aborts by throwing 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}).
 
-\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$ aborted or matching against the \ON{}-\CATCH{} clauses aborted, 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$ aborts, execution of the \TRY{} statement aborts 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.
+Otherwise the \TRY{} statement completes in the same way as the execution of $b$.
 
+\subsubsection{Matching against \ON{}-\CATCH{} clauses}
 \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}
 
 \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$.
 
+Otherwise the exception is matched against the first clause.
 \LMHash{}
-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.
-
 
-\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:
+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.
+}
 
 \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}
 
 
 \subsection{ Return}
@@ -6194,31 +6285,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} $o$.
 
 \LMHash{}
 Let $T$ be the static type of $e$ and let $f$ be the immediately enclosing function.
@@ -6227,13 +6299,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{}
-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{
@@ -6262,40 +6327,14 @@ 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:
+A return statement with no expression, \code{\RETURN;} is executed
+by {\em returning} with no value (\ref{completion}).
 
-\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}
 
@@ -6313,7 +6352,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$ aborts by {\em breaking} with the label $label$,
+then execution of $s$ completes normally,
+otherwise execution of $s$ aborts in the same ways as $sl$.
+
+The namespace of labels is distinct from the one used for types, functions and variables.
 
 \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$.
@@ -6335,11 +6379,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}).
 
+Execution of a \BREAK{} statement \code{\BREAK{};} completes by {\em breaking} without a label (\ref{completion}).
 
 
 \subsection{ Continue}
@@ -6355,25 +6400,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}).
+
+Execution of a \CONTINUE{} statement \code{\CONTINUE{};} completes by {\em continuing} without a label (\ref{completion}).
 
-\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}$.
 
- \subsection{ Yield and Yield-Each}
- \LMLabel{yieldAndYieldEach}
+\subsection{ Yield and Yield-Each}
+\LMLabel{yieldAndYieldEach}
 
- \subsubsection{ Yield}
- \LMLabel{yield}
+\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 ;}'
       .
@@ -6383,20 +6426,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} without a value (\ref{completion}), otherwise it completes normally.
 
 \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.
@@ -6449,7 +6492,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$ aborts in the same way. Otherwise, the result $x$ of the getter invocation is added to the iterable associated with $m$.
 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.
@@ -6459,16 +6502,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$ aborts by {\em returning} with no value (\ref{completion}).
 \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}
 
 
@@ -6496,7 +6542,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.
 
 %\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?}