Allow `rethrow` to end a switch case. Allow braces around switch cases.

docs/language/dartLangSpec.tex

 \documentclass{article}
 \usepackage{epsfig}
 \usepackage{color}
 \usepackage{dart}
 \usepackage{bnf}
 \usepackage{hyperref}
 \usepackage{lmodern}
 \newcommand{\code}[1]{{\sf #1}}
 \title{Dart Programming Language  Specification  \\
 {4th edition draft}\\
@@ skipping 5952 matching lines @@
 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$.
 
 
 \commentary{
 In other words, there is no implicit fall-through between non-empty cases. The last case in a switch (default or otherwise) can `fall-through' to the end of the statement.
 }
 
 \LMHash{}
-It is a static warning if the type of $e$ may not be assigned to the type of $e_k$. It is a static warning if the last statement of the statement sequence $s_k$ is not a \BREAK{}, \CONTINUE{}, \RETURN{} or \THROW{} statement.
+It is a static warning if the type of $e$ may not be assigned to the type of $e_k$.
+Let $s$ be the last statement of the statement sequence $s_k$.
+If $s$ is a non-empty block statement, let $s$ instead be the last statment of the block statement.
+It is a static warning $s$ is not a \BREAK{}, \CONTINUE{}, \REHTROW{} or \RETURN{} statement or an expression statment where the expression is a \THROW{} expression.

[eernst, 2016/10/24 12:38:02]

I'm not sure it's sufficiently helpful to mention the non-empty block statement,
that just makes all the other cases stick out even more.

What we want here is a flow graph; in that flow graph, we may have a node N that
represents the end of the `case`, and we would then focus on the immediate
predecessors N_1..N_m of N, looking recursively into composite statements. The
composite statement might be an `if`, it might be a nested `switch` statement,
etc., and we would then recursively consider the "then" and `else` branches of
that `if` respectively the cases of that `switch`. And then we need to take into
account the possibility that the nested statements may or may not leave the
right thing (with \BREAK{} and \CONTINUE{}, it might look safe unless they will
break/continue with one of those nested constructs).

I wonder if we should start introducing a notion of local flow analysis in order
to be able to say these things in a way that makes sense?

One approach that we could use would be to define for every statement whether it
is statically known to 'never complete normally'. \BREAK{}, \CONTINUE{},
\RETURN{}, \RETHROW{} have this property, and composite statements could
propagate it.

A similar concept would be needed for expressions which may be known to 'never
complete with a value', and \THROW{} expressions would have this property.

This would also allow us to handle things like
```
switch (e) {
case 1: // Not OK: `case 3` lets the nested `switch` complete normally.
  switch (e2) {
  case 2: // OK
    x = e3 ? throw 3 : throw 4;
  case 3: // OK: fall-through
    x = 4;
  }
case 5:
  x = 6;
}
```

So I guess the obvious choices are the following: do we want to enhance
completion to define 'will never complete normally/with-a-value', and then use
that concept here, or do we want to solve this problem later?

[Bob Nystrom, 2016/10/24 16:48:00]

Yeah, I'm not crazy about how blocks are handled here either. It addresses this
case:

switch (e) {
  case 1: {
    return;
  }
}

But doesn't extend to even (admittedly contrived):

switch (e) {
  case 1: {
    {
      return;
    }
  }
}

I think we may want to consider having a concept of "definitely exits" and do
some flow analysis like Erik suggests to define that for each of the statement
and expression forms. I think this would dovetail nicely with a user-defined
bottom. It would be neat if you defined:

bottom exit() { /* abort process... */ }

Then:

switch (e) {
  case 1:
    exit();
}

And it would know this is OK.

[Lasse Reichstein Nielsen, 2016/10/24 18:38:25]

I don't want to solve the general problem right now.

That's a larger problem and needs to be addressed in more places in the
specification, and something we need to think about.

This CL addresses two shortcomings of the current spec - it missed the rethrow
statement for no good reason, and it doesn't handle the common case of wrapping
the statements of a case in a block.
It's not dealing with the recursive case of wrapping a block in a block because
that's just a baby step towards a real analysis, and we should either do it
right or not at all. 

Users coming from languages like C++ will wrap the statements in a block because
they think it's necessary if you make declarations inside the case. It's not
necessary in Dart, but I don't think it should be wrong either, and currently it
is (gives a warning).

We could argue the you shouldn't add a block, and then we shouldn't special case
it and instead just allow it to be a warning. That's a different option, I just
think this is better, yet still simple.


For bottom, it would be a Dart 2 feature - Dart 1 can't trust return types
anyway.

 
 \rationale{
 The behavior of switch cases intentionally differs from the C tradition.  Implicit fall through is a known cause of programming errors and therefore disallowed.  Why not simply break the flow implicitly at the end of every case, rather than requiring explicit code to do so?  This would indeed be cleaner.  It would also be cleaner to insist that each case have a single (possibly compound) statement.  We have chosen not to do so in order to facilitate porting of switch statements from other languages.  Implicitly breaking the control flow at the end of a case would silently alter the meaning of ported code that relied on fall-through, potentially forcing the programmer to deal with subtle bugs. Our design ensures that the difference is immediately brought to the coder's attention.  The programmer will be notified at compile-time if they forget to end a case with a statement that terminates the straight-line control flow. We could make this warning a compile-time error, but refrain from doing so because do not wish to force the programmer to deal with this issue immediately while porting code.  If developers ignore the warning and run their code, a run time error will prevent the program from misbehaving in hard-to-debug ways (at least with respect to this issue).
 
 The sophistication of the analysis of fall-through is another issue. For now, we have opted for a very straightforward syntactic requirement. There are obviously situations where code does not fall through, and yet does not conform to these simple rules, e.g.:
 }
 
 \begin{dartCode}
 \SWITCH{} (x) \{
   \CASE{} 1: \TRY{} \{ $\ldots$ \RETURN{};\} \FINALLY{} \{ $\ldots$ \RETURN{};\}
@@ skipping 1928 matching lines @@
 
 The invariant that each normative paragraph is associated with a line
 containing the text \LMHash{} should be maintained.  Extra occurrences
 of \LMHash{} can be added if needed, e.g., in order to make
 individual \item{}s in itemized lists addressable.  Each \LM.. command
 must occur on a separate line.  \LMHash{} must occur immediately
 before the associated paragraph, and \LMLabel must occur immediately
 after the associated \section{}, \subsection{} etc.
 
 ----------------------------------------------------------------------