diff --git a/docs/language/dart.sty b/docs/language/dart.sty
index 3146317..a7e9cb7 100644
--- a/docs/language/dart.sty
+++ b/docs/language/dart.sty
@@ -1,12 +1,6 @@
-\def\keyword#1{\textbf{#1}}
-\def\builtinId#1{\textbf{#1}}
 \def\code#1{\textsf{#1}}
-\def\comment#1{\textit{#1}}
-\def\capt#1{\rmfamily \caption{#1}}
-\def\lt{\ensuremath{<}}
-\def\gt{\ensuremath{>}}
-\def\<{\ensuremath{\langle}}
-\def\>{\ensuremath{\rangle}}
+\def\builtinId#1{\code{\textbf{#1}}}
+\def\keyword#1{\code{\textbf{#1}}}
 \def\metavar#1{\ensuremath{\mathit{#1}}}
 
 \def\ABSTRACT{\builtinId{abstract}}
@@ -34,7 +28,6 @@
 \def\ASYNC{\keyword{async}}
 \def\AWAIT{\keyword{await}}
 \def\BREAK{\keyword{break}}
-\def\CALL{\keyword{call}}
 \def\CASE{\keyword{case}}
 \def\CATCH{\keyword{catch}}
 \def\CLASS{\keyword{class}}
@@ -73,6 +66,18 @@
 \def\WITH{\keyword{with}}
 \def\YIELD{\keyword{yield}}
 
+% `call` has no special lexical status, so we just use \code{}.
+\def\CALL{\code{call}}
+
+% Used in regular text to indicate that #1 consists of non-terminals.
+%% TODO(eernst): Update to use grammar font when we start using that;
+%% at this point we just make it "regular text" using \mbox.
+\newcommand{\NonTerminal}[1]{\mbox{#1}}
+
+% Angle brackets used for operators in grammar context.
+\def\lt{\ensuremath{<}}
+\def\gt{\ensuremath{>}}
+
 % A quoted comma as used in the grammar: needs spacing fix.
 \newcommand{\gcomma}{\mbox{`,\hspace{-0.1em}'}}
 
@@ -88,6 +93,14 @@
 \newenvironment{rationale}[1]{{\it #1}}{}
 \newenvironment{commentary}[1]{{\sf #1}}{}
 
+\newcommand{\flatten}[1]{\ensuremath{\mbox{\it flatten}({#1})}}
+
+% Used as a mini-section marker, indicating visibly that a range of
+% text (usually just a couple of paragraphs) are concerned with one
+% specific topic in a list of similar topics (like many forms of
+% expressions of a similar nature).
+\newcommand{\Case}[1]{\textbf{Case }$\langle\hspace{0.1em}${#1}$\hspace{0.1em}\rangle$\textbf{.}}
+
 \newenvironment{dartCode}[1][!ht] {
 %  \begin{verbatim}[#1]
   \def\@programcr{\@addfield\strut}
diff --git a/docs/language/dartLangSpec.tex b/docs/language/dartLangSpec.tex
index e74b910..b37d438 100644
--- a/docs/language/dartLangSpec.tex
+++ b/docs/language/dartLangSpec.tex
@@ -27,6 +27,35 @@
 %   declaration must be taken into account during static checks.
 % - Disallow any expression statement starting with `{`, not just
 %   those that are map literals.
+% - Define a notion of lookup that is needed for super invocations, adjust
+%   specification of super invocations accordingly.
+% - Specify that it is a dynamic error to initialize a non-static variable
+%   with a value that does not have the declared type (e.g., a failed cast).
+% - Specify for constructor initializers that target variable must exist and
+%   the initializing expression must have a type which is assignable to its
+%   type.
+% - Specify for superinitializers that the target constructor must exist and
+%   the argument part must have a matching shape and pass type and value
+%   arguments satisfying the relevant constraints.
+% - Reword rules about abstract methods and inheritance to use 'class
+%   interface'.
+% - Specify that it is an error for a concrete class with no non-trivial
+%   \code{noSuchMethod} to not have a concrete declaration for some member
+%   in its interface, or to have one which is not a correct override.
+% - Use \ref{bindingActualsToFormals} in 3 locations, eliminating 2 extra
+%   copies of nearly the same text.
+% - Add figure in \ref{bindingActualsToFormals} for improved readability.
+% - Introduce a notion of lookup which is needed for superinvocations.
+% - Use new lookup concept to simplify specification of getter, setter, method
+%   lookup.
+% - Introduce several `Case< SomeTopic >` markers in order to improve
+%   readability.
+% - Reorganize several sections to specify static analysis first and then
+%   dynamic semantics; clarify many details along the way. The sections are:
+%   \ref{variables}, \ref{new}, \ref{const}, \ref{bindingActualsToFormals},
+%   \ref{unqualifiedInvocation}, \ref{functionExpressionInvocation},
+%   \ref{superInvocations}, \ref{assignment}, \ref{compoundAssignment},
+%   \ref{localVariableDeclaration}, and \ref{return}.
 %
 % 2.0
 % - Don't allow functions as assert test values.
@@ -621,10 +650,49 @@
 \end{grammar}
 
 \LMHash{}
-A variable that has not been initialized has the null object (\ref{null}) as its initial value.
+A variable declaration that contains one or more terms of the form
+\NonTerminal{initializedIdentifier}
+(\commentary{i.e., a declaration that declares two or more variables})
+is equivalent to multiple variable declarations declaring
+the same set of variable names in the same order,
+with the same initialization, type, and modifiers.
+
+\commentary{
+For example,
+\code{\VAR{} x = 1, y;}
+is equivalent to
+\code{\VAR{} x = 1; \VAR{} y;}
+and
+\code{\STATIC{} \FINAL{} String s1, s2 = "foo";}
+is equivalent to
+\code{\STATIC{} \FINAL{} String s1; \STATIC{} \FINAL{} String s2 = "foo";}.
+}
 
 \LMHash{}
-A variable declared at the top-level of a library is referred to as either a {\em library variable} or simply a top-level variable.
+In a variable declaration of one of the forms
+\code{$N$ $v$;}
+\code{$N$ $v$ = $e$;}
+where $N$ is derived from
+\NonTerminal{metadata finalConstVarOrType},
+we say that $v$ is the {\em declaring occurrence} of the identifier.
+For every identifier which is not a declaring occurrence,
+we say that it is an {\em referencing occurrence}.
+We also abbreviate that to say that an identifier is
+a {\em declaring identifier} respectively an {\em referencing identifier}.
+
+\commentary{
+In an expression of the form \code{$e$.\id} it is possible that
+$e$ has static type \DYNAMIC{} and \id{} cannot be associated with
+any declaration named \id{} at compile-time,
+but in this situation \id{} is still an referencing identifier.
+}
+
+\LMHash{}
+An {\em initialized variable} is a variable whose declaring identifier is
+immediately followed by `\code{=}' and an {\em initializing expression}.
+
+\LMHash{}
+A variable declared at the top-level of a library is referred to as either a {\em library variable} or a top-level variable.
 
 \LMHash{}
 A {\em static variable} is a variable that is not associated with a particular instance, but rather with an entire library or class.
@@ -634,49 +702,74 @@
 It is a compile-time error to preface a top-level variable declaration with the built-in identifier (\ref{identifierReference}) \STATIC{}.
 
 \LMHash{}
-Static variable declarations are initialized lazily.
-When a static variable $v$ is read, if{}f it has not yet been assigned, it is set to the result of evaluating its initializer.
-The precise rules are given in section \ref{evaluationOfImplicitVariableGetters}.
-
-\rationale{
-The lazy semantics are given because we do not want a language where one tends to define expensive initialization computations, causing long application startup times.
-This is especially crucial for Dart, which must support the coding of client applications.
-}
-
-\LMHash{}
-A {\em final variable} is a variable whose binding is fixed upon initialization; a final variable $v$ will always refer to the same object after $v$ has been initialized.
-The declaration of a final variable must include the modifier \FINAL{}.
-
-\LMHash{}
-It is a compile-time error if a final instance variable whose declaration has an initializer expression
-is also initialized by a constructor, either by an initializing formal or an initializer list entry.
-It is a compile-time error if a local variable $v$ is final and $v$ is not initialized at its point of declaration.
-It is a compile-time error to assign to a final local variable.
-
-\commentary{
-It is a compile-time error if a final instance variable
-that has been initialized by means of an initializing formal of a constructor $k$
-is also initialized in the initializer list of $k$ (\ref{initializerLists}).
-Any attempt to assign to a final non-local variable \id{} will cause a compile-time error,
-because it amounts to an invocation of a setter named \code{\id=},
-except of course when such a setter has been declared separately.
-}
-
-\LMHash{}
 A {\em constant variable} is a variable whose declaration includes the modifier \CONST{}.
-A constant variable is always implicitly final.
 A constant variable must be initialized to a compile-time constant (\ref{constants}) or a compile-time error occurs.
 
 \LMHash{}
-We say that a variable $v$ is {\em potentially mutated} in some scope $s$ if $v$ is not final or constant and an assignment to $v$ occurs in $s$.
+A {\em final variable} is a variable whose binding is fixed upon initialization;
+a final variable $v$ will always refer to the same object after $v$ has been initialized.
+A variable is final if{}f its declaration includes the modifier \FINAL{} or the modifier \CONST{}.
 
 \LMHash{}
-If a variable declaration does not explicitly specify a type, the type of the declared variable(s) is \DYNAMIC{}, the unknown type (\ref{typeDynamic}).
+A {\em mutable variable} is a variable which is not final.
+
+%% Note that the following relies on the assumption that inference has
+%% already taken place, including member signature inference. For instance,
+%% if `var x;` is an instance variable declaration that overrides `T get x;`
+%% then we treat `var x;` as if it had been `T x;`.
 
 \LMHash{}
-A variable is {\em mutable} if it is not final.
-Static and instance variable declarations always induce implicit getters.
-If the variable is mutable it also introduces an implicit setter.
+The following rules apply to all static and instance variables.
+
+\LMHash{}
+A variable declaration of one of the forms
+\code{$T$ $v$;}
+\code{$T$ $v$ = $e$;}
+\code{\CONST{} $T$ $v$ = $e$;}
+\code{\FINAL{} $T$ $v$;}
+or \code{\FINAL{} $T$ $v$ = $e$;}
+induces an implicit getter function (\ref{getters}) with signature
+\code{$T$ \GET{} $v$}
+whose invocation evaluates as described below
+(\ref{evaluationOfImplicitVariableGetters}).
+In these cases the static type of $v$ is $T$.
+
+\LMHash{}
+A variable declaration of one of the forms
+\code{\VAR{} $v$;}
+\code{\VAR{} $v$ = $e$;}
+\code{\CONST{} $v$ = $e$;}
+\code{\FINAL{} $v$;}
+or \code{\FINAL{} $v$ = $e$;}
+induces an implicit getter function with signature
+\code{\DYNAMIC{} \GET{} $v$}
+whose invocation evaluates as described below
+(\ref{evaluationOfImplicitVariableGetters}).
+%% TODO[inference]: We assume inference has taken place, i.e., inferred types
+%% are written explicitly. Does this mean that the initialized variants
+%% cannot exist (not even for `$e$` of type `dynamic`?). We probably don't
+%% want to start talking about a grammar before inference and another one
+%% after inference.
+In these cases, the static type of $v$ is \DYNAMIC{}
+(\ref{typeDynamic}).
+
+\LMHash{}
+A mutable variable declaration of the form
+\code{{} $T$ $v$;}
+or \code{$T$ $v$ = $e$;}
+induces an implicit setter function (\ref{setters}) with signature
+\code{\VOID{} \SET{} $v$=($T$ $x$)}
+whose execution sets the value of $v$ to the incoming argument $x$.
+
+\LMHash{}
+A mutable variable declaration of the form
+\code{\VAR{} $v$;}
+or \code{\VAR{} $v$ = $e$;}
+induces an implicit setter function with signature
+\code{\VOID{} \SET{} $v$=(\DYNAMIC{} $x$)}
+whose execution sets the value of $v$ to the incoming argument $x$.
+
+\LMHash{}
 The scope into which the implicit getters and setters are introduced depends on the kind of variable declaration involved.
 
 \LMHash{}
@@ -690,113 +783,78 @@
 A mutable instance variable introduces an instance setter into the immediately enclosing class.
 
 \LMHash{}
-Local variables are added to the innermost enclosing scope.
-They do not induce getters and setters.
-A local variable may only be referenced at a source code location that is after its initializer, if any, is complete, or a compile-time error occurs.
-The error may be reported either at the point where the premature reference occurs, or at the variable declaration.
+Let $v$ be an initialized variable and let $e$ be the associated initializing expression.
+It is a compile-time error if the static type of $e$ is not assignable to the declared type of $v$.
+It is a compile-time error if a final instance variable whose declaration has an initializer expression
+is also initialized by a constructor, either by an initializing formal or an initializer list entry.
+
+\commentary{
+It is a compile-time error if a final instance variable
+that has been initialized by means of an initializing formal of a constructor $k$
+is also initialized in the initializer list of $k$ (\ref{initializerLists}).
+
+A static final variable $v$ does not induce a setter,
+so unless a setter named \code{$v$=} is in scope
+it is a compile-time error to assign to $v$.
+
+Similarly, assignment to a final instance variable $v$
+is a compile-time error,
+unless a setter named \code{$v$=} is in scope,
+or the receiver has type \DYNAMIC{}.
+$v$ can be initialized in its declaration or in initializer lists,
+but initialization and assignment is not the same thing.
+When the receiver has type \DYNAMIC{}
+such an assignment is not a compile-time error,
+but if there is no setter it will cause a dynamic error.
+}
+
+\LMHash{}
+A variable that has no initializing expression has the null object (\ref{null}) as its initial value.
+Otherwise, variable initialization proceeds as follows:
+
+\LMHash{}
+Static variable declarations with an initializing expression are initialized lazily
+(\ref{evaluationOfImplicitVariableGetters}).
 
 \rationale{
-We allow the error to be reported at the declaration to allow implementations to avoid an extra processing phase.
+The lazy semantics are given because we do not want a language where one tends to define expensive initialization computations, causing long application startup times.
+This is especially crucial for Dart, which must support the coding of client applications.
 }
 
 \commentary{
-The example below illustrates the expected behavior.
-A variable $x$ is declared at the library level, and another $x$ is declared inside the function $f$.
+Initialization of an instance variable with no initializing expression
+takes place during constructor execution
+(\ref{initializerLists}).
 }
 
-\begin{dartCode}
-\VAR{} x = 0;
-
-f(y) \{
-  \VAR{} z = x; // compile-time error
-  if (y) \{
-    x = x + 1; // two compile-time errors
-    print(x); // compile-time error
-  \}
-  \VAR{} x = x++; // compile-time error
-  print(x);
-\}
-\end{dartCode}
+\LMHash{}
+Initialization of an instance variable $v$
+with an initializing expression $e$
+proceeds as follows:
+$e$ is evaluated to an object $o$
+and the variable $v$ is bound to $o$.
 
 \commentary{
-The declaration inside $f$ hides the enclosing one.
-So all references to $x$ inside $f$ refer to the inner declaration of $x$.
-However, many of these references are illegal, because they appear before the declaration.
-The assignment to $z$ is one such case.
-The assignment to $x$ in the \IF{} statement suffers from multiple problems.
-The right hand side reads $x$ before its declaration, and the left hand side assigns to $x$ before its declaration.
-Each of these are, independently, compile-time errors.
-The print statement inside the \IF{} is also illegal.
-
-The inner declaration of $x$ is itself erroneous because its right hand side attempts to read $x$ before the declaration has terminated.
-The left hand side is not, technically, a reference or an assignment but a declaration and so is legal.
-The last print statement is perfectly legal as well.
+It is specified elsewhere when this initialization occurs,
+and in which environment
+(p.\,\pageref{executionOfGenerativeConstructors},
+\ref{localVariableDeclaration},
+\ref{bindingActualsToFormals}).
 }
 
 \commentary{
-As another example \code{\VAR{} x = 3, y = x;} is legal, because \code{x} is referenced after its initializer.
-
-A particularly perverse example involves a local variable name shadowing a type.
-This is possible because Dart has a single namespace for types, functions and variables.
+If the initializing expression throws then
+access to the uninitialized variable is prevented,
+because the instance creation
+that caused this initialization to take place
+will throw.
 }
 
-\begin{dartCode}
-\CLASS{} C \{\}
-perverse() \{
-   \VAR{} v = \NEW{} C(); // compile-time error
-   C aC; // compile-time error
-   \VAR{} C = 10;
-\}
-\end{dartCode}
-
-\commentary{
-Inside \code{perverse()}, \code{C} denotes a local variable.
-The type \code{C} is hidden by the variable of the same name.
-The attempt to instantiate \code{C} causes a compile-time error because it references a local variable prior to its declaration.
-Similarly, for the declaration of \code{aC} (even though it is only a type annotation).
-}
-
-\rationale{
-As a rule, type annotations are ignored in production mode.
-However, we do not want to allow programs to compile legally in one mode and not another, and in this extremely odd situation, that consideration takes precedence.
-}
-
-% the grammar does not support local getters and setters.
-% The local var discussion does not seem to mention getters and setters based semantics.
-% It simply discusses the creation of the variable, not its access.
-% Access is either assignment or identifiers.
-% Identifiers ignore the getter story.
-
 \LMHash{}
-The following rules apply to all static and instance variables.
-
-\LMHash{}
-A variable declaration of one of the forms \code{$T$ $v$;}, \code{$T$ $v$ = $e$;} \code{\CONST{} $T$ $v$ = $e$;}, \code{\FINAL{} $T$ $v$;} or \code{\FINAL{} $T$ $v$ = $e$;} always induces an implicit getter function (\ref{getters}) with signature
-
-$T$ \GET{} $v$
-
-whose invocation evaluates as described below (\ref{evaluationOfImplicitVariableGetters}).
-
-\LMHash{}
-A variable declaration of one of the forms \code{\VAR{} $v$;}, \code{\VAR{} $v$ = $e$;}, \code{\CONST{} $v$ = $e$;}, \code{\FINAL{} $v$;} or \code{\FINAL{} $v$ = $e$;} always induces an implicit getter function with signature
-
-\GET{} $v$
-
-whose invocation evaluates as described below (\ref{evaluationOfImplicitVariableGetters}).
-
-\LMHash{}
-A non-final variable declaration of the form \code{{} $T$ $v$;} or the form \code{$T$ $v$ = $e$;} always induces an implicit setter function (\ref{setters}) with signature
-
- \VOID{} \SET{} $v=(T$ $x)$
-
-whose execution sets the value of $v$ to the incoming argument $x$.
-
-\LMHash{}
-A non-final variable declaration of the form \code{\VAR{} $v$;} or the form \code{\VAR{} $v$ = $e$;} always induces an implicit setter function with signature
-
-\SET{} $v=(x)$
-
-whose execution sets the value of $v$ to the incoming argument $x$.
+In checked mode,
+it is a dynamic type error if $o$ is not the null object (\ref{null})
+and the interface of the class of $o$ is not a subtype of the actual type of the variable $v$
+(\ref{actualTypeOfADeclaration}).
 
 
 \subsection{Evaluation of Implicit Variable Getters}
@@ -804,23 +862,50 @@
 
 \LMHash{}
 Let $d$ be the declaration of a static or instance variable $v$.
-If $d$ is an instance variable, then the invocation of the implicit getter of $v$ evaluates to the value stored in $v$.
-If $d$ is a static or library variable then the implicit getter method of $v$ executes as follows:
+If $d$ is an instance variable,
+then the invocation of the implicit getter of $v$ evaluates to
+the value stored in $v$.
+If $d$ is a static variable
+(\commentary{which can be a library variable})
+then the implicit getter method of $v$ executes as follows:
 \begin{itemize}
 \item {\bf Non-constant variable declaration with initializer}.
-If $d$ is of one of the forms \code{\VAR{} $v$ = $e$;}, \code{$T$ $v$ = $e$;}, \code{\FINAL{} $v$ = $e$;}, \code{\FINAL{} $T$ $v$ = $e$;}, \code{\STATIC{} $v$ = $e$;}, \code{\STATIC{} $T$ $v$ = $e$; }, \code{\STATIC{} \FINAL{} $v$ = $e$; } or \code{\STATIC{} \FINAL{} $T$ $v$ = $e$;} and no value has yet been stored into $v$ then the initializer expression $e$ is evaluated.
-If, during the evaluation of $e$, the getter for $v$ is invoked, a \code{CyclicInitializationError} is thrown.
-If the evaluation succeeded yielding an object $o$, let $r$ be $o$, otherwise let $r$ be the null object (\ref{null}).
-In any case, $r$ is stored into $v$.
-The result of executing the getter is $r$.
+If $d$ is of one of the forms
+\code{\VAR{} $v$ = $e$;},
+\code{$T$ $v$ = $e$;},
+\code{\FINAL{} $v$ = $e$;},
+\code{\FINAL{} $T$ $v$ = $e$;},
+\code{\STATIC{} $v$ = $e$;},
+\code{\STATIC{} $T$ $v$ = $e$; },
+\code{\STATIC{} \FINAL{} $v$ = $e$; } or
+\code{\STATIC{} \FINAL{} $T$ $v$ = $e$;}
+and no value has yet been stored into $v$
+then the initializing expression $e$ is evaluated.
+If, during the evaluation of $e$, the getter for $v$ is invoked,
+a \code{CyclicInitializationError} is thrown.
+If the evaluation of $e$ throws an exception $e$ and stack trace $s$,
+the null object (\ref{null}) is stored into $v$;
+the execution of the getter then throws $e$ and stack trace $s$.
+Otherwise, the evaluation of $e$ succeeded yielding an object $o$;
+then $o$ is stored into $v$ and
+the execution of the getter completes by returning $o$.
+Otherwise,
+(\commentary{when a value $o$ has been stored in $v$})
+execution of the getter completes by returning $o$.
 \item {\bf Constant variable declaration}.
-If $d$ is of one of the forms \code{\CONST{} $v$ = $e$;}, \code{\CONST{} $T$ $v$ = $e$;}, \code{\STATIC{} \CONST{} $v$ = $e$;} or \code{\STATIC{} \CONST{} $T$ $v$ = $e$;} the result of the getter is the value of the compile-time constant $e$.
+If $d$ is of one of the forms
+\code{\CONST{} $v$ = $e$;},
+\code{\CONST{} $T$ $v$ = $e$;},
+\code{\STATIC{} \CONST{} $v$ = $e$;} or
+\code{\STATIC{} \CONST{} $T$ $v$ = $e$;}
+the result of the getter is the value of the compile-time constant $e$.
 \commentary{
-Note that a compile-time constant cannot depend on itself, so no cyclic references can occur.
+Note that a compile-time constant cannot depend on itself,
+so no cyclic references can occur.
 }
-Otherwise
 \item {\bf Variable declaration without initializer}.
 The result of executing the getter method is the value stored in $v$.
+\commentary{This may be the initial value, that is, the null object.}
 \end{itemize}
 
 
@@ -867,27 +952,29 @@
 \begin{itemize}
 \item A block statement (\ref{blocks}) containing the statements (\ref{statements}) executed by the function, optionally marked with one of the modifiers: \ASYNC, \ASYNC* or \SYNC*.
 
-\commentary{
-Because Dart is optionally typed, we cannot guarantee that a function that does not return a value will not be used in the context of an expression.
-Therefore, every function must return a value.
-A function body that ends without doing a throw or return will cause the function to return the null object (\ref{null}), as will a \RETURN{} without an expression.
-For generator functions, the situation is more subtle.
-See further discussion in section \ref{return}.
-}
+  \commentary{
+  Because Dart is optionally typed, we cannot guarantee that a function that does not return a value will not be used in the context of an expression.
+  Therefore, every function must return a value.
+  A function body that ends without doing a throw or return will cause the function to return the null object (\ref{null}),
+  as will a \RETURN{} without an expression.
+  For generator functions, the situation is more subtle.
+  See further discussion in section \ref{return}.
+  }
 
 OR
 \item of the form \code{=> $e$} or the form \code{\ASYNC{} => $e$}, which both return the value of the expression $e$ as if by a \code{return $e$}.
-\commentary{
-The other modifiers do not apply here, because they apply only to generators, discussed below, and generators do not allow to return a value, values are added to the generated stream or iterable using \YIELD{} instead.
-}
-Let $R$ be the static type of $e$
-and let $T$ be the actual return type (\ref{actualTypeOfADeclaration})
-of the function that has this body.
-It is a compile-time error if $T$ is not \VOID{} and either
-the function is synchronous and the static type of $R$ is not assignable to $T$,
-or the function is asynchronous and \code{Future<$flatten(R)$>}
-is not assignable to $T$.
-
+  \commentary{
+  The other modifiers do not apply here, because they apply only to generators, discussed below,
+  and generators are not allowed to return a value, values are added to the generated stream or iterable using \YIELD{} instead.
+  }
+  Let $R$ be the static type of $e$
+  and let $T$ be the declared return type of the function that has this body.
+  It is a compile-time error unless one of the following conditions hold:
+  \begin{itemize}
+  \item $T$ is \VOID{}.
+  \item The function is synchronous and $R$ is assignable to $T$.
+  \item The function is asynchronous and \code{Future<\flatten{R}>} is assignable to $T$.
+  \end{itemize}
 \end{itemize}
 
 \LMHash{}
@@ -897,7 +984,8 @@
 
 \commentary{
 Whether a function is synchronous or asynchronous is orthogonal to whether it is a generator or not.
-Generator functions are a sugar for functions that produce collections in a systematic way, by lazily applying a function that {\em generates} individual elements of a collection.
+Generator functions are a sugar for functions that produce collections in a systematic way,
+by lazily applying a function that {\em generates} individual elements of a collection.
 Dart provides such a sugar in both the synchronous case, where one returns an iterable, and in the asynchronous case, where one returns a stream.
 Dart also allows both synchronous and asynchronous functions that produce a single value.
 }
@@ -906,9 +994,10 @@
 It is a compile-time error if an \ASYNC, \ASYNC* or \SYNC* modifier is attached to the body of a setter or constructor.
 
 \rationale{
-An asynchronous setter would be of little use, since setters can only be used in the context of an assignment (\ref{assignment}), and an assignment expression always evaluates to the value of the assignment's right hand side.
-If the setter actually did its work asynchronously, one might imagine that one would return a future that resolved to the assignment's right hand side after the setter did its work.
-However, this would require dynamic tests at every assignment, and so would be prohibitively expensive.
+An asynchronous setter would be of little use, since setters can only be used in the context of an assignment (\ref{assignment}),
+and an assignment expression always evaluates to the value of the assignment's right hand side.
+If the setter actually did its work asynchronously,
+one might imagine that one would return a future that resolved to the assignment's right hand side after the setter did its work.
 
 An asynchronous constructor would, by definition, never return an instance of the class it purports to construct, but instead return a future.
 Calling such a beast via \NEW{} would be very confusing.
@@ -919,6 +1008,7 @@
 No other scenario makes sense because the object returned by the factory would be of the wrong type.
 This situation is very unusual so it is not worth making an exception to the general rule for constructors in order to allow it.
 }
+
 \LMHash{}
 It is a compile-time error if the declared return type of a function marked \ASYNC{} is not a supertype of \code{Future<$T$>} for some type $T$.
 It is a compile-time error if the declared return type of a function marked \SYNC* is not a supertype of \code{Iterable<$T$>} for some type $T$.
@@ -1289,7 +1379,7 @@
 \LMHash{}
 A class has constructors, instance members and static members.
 The instance members of a class are its instance methods, getters, setters and instance variables.
-The static members of a class are its static methods, getters, setters and static variables.
+The static members of a class are its static methods, getters, setters and class variables.
 The members of a class are its static and instance members.
 
 \LMHash{}
@@ -1572,14 +1662,17 @@
 }
 
 \commentary{
-Invoking an abstract method, getter or setter results in an invocation of \code{noSuchMethod} exactly as if the declaration did not exist, unless a suitable member $a$ is available in a superclass, in which case $a$ is invoked.
-The normative specification for this appears under the definitions of lookup for methods, getters and setters.
+Invocation of an abstract method, getter, or setter cannot occur,
+because lookup (\ref{lookup}) will never yield an abstract member as its result.
+One way to think about this is that
+an abstract member declaration in a subclass
+does not override or shadow an inherited member implementation.
+It only serves to specify the signature of the given member that
+every concrete subtype must have an implementation of;
+that is, it contributes to the interface of the class,
+not to the class itself.
 }
 
-% so does an abstract method override a method in a superclass or not? Does the superclass method get inherited or not?  This generally makes the spec inconsistent, as there is no simple answer.
-% For example - if we say it does not override, then the superclass member is inherited, in which case the rules for errors break down, and also there is question of whether there are two definitions of the same name.
-% But if we do override, method lookup rules break down.  So several things need revisiting.
-
 \rationale{
 The purpose of an abstract method is to provide a declaration for purposes such as type checking and reflection.
 In classes used as mixins, it is often useful to introduce such declarations for methods that the mixin expects will be provided by the superclass the mixin is applied to.
@@ -1828,7 +1921,8 @@
 of the corresponding formal parameter in the declaration of $k$.
 It is a dynamic error if an actual argument passed to the redirectee $k'$ of a redirecting generative constructor
 is not a subtype of the actual type
-(\ref{actualTypeOfADeclaration}) of the corresponding formal parameter in the declaration of the redirectee.
+(\ref{actualTypeOfADeclaration})
+of the corresponding formal parameter in the declaration of the redirectee.
 
 
 \paragraph{Initializer Lists}
@@ -1836,12 +1930,16 @@
 
 \LMHash{}
 An initializer list begins with a colon, and consists of a comma-separated list of individual {\em initializers}.
-There are two kinds of initializers.
+
+\commentary{
+There are three kinds of initializers.
 \begin{itemize}
-\item A {\em superinitializer} identifies a {\em superconstructor} - that is, a specific constructor of the superclass.
+\item A {\em superinitializer} identifies a {\em superconstructor}\,---\,that is, a specific constructor of the superclass.
 Execution of the superinitializer causes the initializer list of the superconstructor to be executed.
 \item An {\em instance variable initializer} assigns a value to an individual instance variable.
+\item An assertion.
 \end{itemize}
+}
 
 \begin{grammar}
 {\bf initializers:}`{\escapegrammar :}' initializerListEntry (\gcomma{} initializerListEntry)*
@@ -1858,6 +1956,36 @@
 \end{grammar}
 
 \LMHash{}
+An initializer of the form \code{$v$ = $e$} is equivalent to
+an initializer of the form \code{\THIS{}.$v$ = $e$},
+both forms are called {\em instance variable initializers}.
+It is a compile-time error if the enclosing class does not declare an instance variable named $v$.
+Otherwise, let $T$ be the static type of $v$.
+It is a compile-time error unless the static type of $e$ is assignable to $T$.
+
+\LMHash{}
+Consider a {\em superinitializer} $s$ of the form
+
+\code{\SUPER{}($a_1, \ldots,\ a_n,\ x_{n+1}: a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
+respectively
+
+\code{\SUPER{}.\id($a_1, \ldots,\ a_n,\ x_{n+1}: a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
+
+\noindent{}%
+Let $S$ be the superclass of the enclosing class of $s$.
+It is a compile-time error if class $S$ does not declare a generative constructor named $S$ (respectively \code{$S$.\id}).
+Otherwise, the static analysis of $s$ is performed as specified in Section~\ref{bindingActualsToFormals},
+as if \code{\SUPER{}} respectively \code{\SUPER{}.\id}
+had had the function type of the denoted constructor,
+%% TODO(eernst): The following is very imprecise, it just serves to remember
+%% that we must specify how to deal with the type variables in that parameter
+%%  part. One thing that we weasel over is that the superclass may be a mixin
+%% application.
+and substituting the formal type variables of the superclass
+for the corresponding actual type arguments passed to the superclass
+in the header of the current class.
+
+\LMHash{}
 Let $k$ be a generative constructor.
 Then $k$ may include at most one superinitializer in its initializer list or a compile-time error occurs.
 If no superinitializer is provided, an implicit superinitializer of the form \SUPER{}() is added at the end of $k$'s initializer list,
@@ -1885,10 +2013,15 @@
 \LMHash{}
 It is a compile-time error if a generative constructor of class \code{Object} includes a superinitializer.
 
+
+\paragraph{Execution of Generative Constructors}
+\LMLabel{executionOfGenerativeConstructors}
+
 \LMHash{}
 Execution of a generative constructor $k$ of type $T$ to initialize a fresh instance $i$
 is always done with respect to a set of bindings for its formal parameters
-and the type parameters of the immediately enclosing class bound to a set of actual type arguments of $T$, $V_1, \ldots, V_m$.
+and the type parameters of the immediately enclosing class bound to
+a set of actual type arguments of $T$, $t_1, \ldots, t_m$.
 
 \commentary{
 These bindings are usually determined by the instance creation expression that invoked the constructor (directly or indirectly).
@@ -1902,17 +2035,25 @@
 
 where $g$ identifies another  generative constructor of the immediately surrounding class.
 Then execution of $k$ to initialize $i$ proceeds by evaluating the argument list
-\code{($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
 \code{($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$.
+to an actual argument list $a$ of the form
+\code{($o_1, \ldots,\ o_n,\ x_{n+1}$: $o_{n+1}, \ldots,\ x_{n+k}$: $o_{n+k}$)}
+in an environment where the type parameters of the enclosing class are bound to
+$t_1, \ldots, t_m$.
 
 \LMHash{}
-Otherwise, execution proceeds as follows:
+Next, the body of $g$ is executed to initialize $i$ with respect to the bindings that map
+the formal parameters of $g$ to the corresponding objects in the actual argument list $a$,
+with \THIS{} bound to $i$,
+and the type parameters of the immediately enclosing class bound to $t_1, \ldots, t_m$.
+
+\LMHash{}
+Otherwise, $k$ is not redirecting.
+Execution then proceeds as follows:
 
 \LMHash{}
 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$; }
+For each such declaration $d$, if $d$ has the form \code{\metavar{finalConstVarOrType} $v$ = $e$; }
 then $e$ is evaluated to an object $o$
 and the instance variable $v$ of $i$ is bound to $o$.
 
@@ -1921,7 +2062,8 @@
 % In fact, this order is unobservable; this could be done any time prior to running the body, since
 % these only effect \THIS{}.
 Then, the initializers of $k$'s initializer list are executed to initialize $i$
-in the order they appear in the program.
+in the order they appear in the program, as described below
+(p.\,\pageref{executionOfInitializerLists}).
 
 \rationale{
 We could observe the order by side effecting external routines called.
@@ -1944,9 +2086,14 @@
 \rationale{
 This process ensures that no uninitialized final instance variable 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.
+an instance method cannot be directly invoked,
+nor can \THIS{} be passed into any other code being invoked in the initializer.
 }
 
+
+\paragraph{Execution of Initializer Lists}
+\LMLabel{executionOfInitializerLists}
+
 \LMHash{}
 During the execution of a generative constructor to initialize an instance $i$,
 execution of an initializer of the form \code{\THIS{}.$v$ = $e$}
@@ -1955,45 +2102,46 @@
 \LMHash{}
 First, the expression $e$ is evaluated to an object $o$.
 Then, the instance variable $v$ of $i$ is bound to $o$.
-In checked mode, it is a dynamic type error if $o$ is not the null object (\ref{null}) and the interface of the class of $o$ is not a subtype of the actual type of the instance variable $v$.
-
-\LMHash{}
-An initializer of the form \code{$v$ = $e$} is equivalent to an initializer of the form \code{\THIS{}.$v$ = $e$}.
+In checked mode,
+it is a dynamic type error if $o$ is not the null object
+(\ref{null})
+and the interface of the class of $o$ is not a subtype of the actual type
+(\ref{actualTypeOfADeclaration})
+of the instance variable $v$.
 
 \LMHash{}
 Execution of an initializer that is an assertion proceeds by executing the assertion (\ref{assert}).
 
 \LMHash{}
-Execution of a superinitializer of the form
+Consider a superinitializer $s$ of the form
 
 \code{\SUPER{}($a_1, \ldots,\ a_n,\ x_{n+1}: a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
+respectively
 
-(respectively
-\code{\SUPER{}.\id($a_1, \ldots,\ a_n,\ x_{n+1}: a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)})
-
-proceeds as follows:
+\code{\SUPER{}.\id($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
 
 \LMHash{}
-First, the argument list
+Let $C$ be the class in which $s$ appears and let $S$ be the superclass of $C$.
+If $S$ is generic (\ref{generics}),
+let $u_1, \ldots, u_p$ be the actual type arguments passed to $S$,
+obtained by substituting $t_1, \ldots, t_m$
+for the formal type parameters of $C$
+in the superclass as specified in the header of $C$, and
+$t_1, \ldots, t_m$
+are the actual bindings of the type variables of $C$.
+Let $k$ be the constructor declared in $S$ and named
+$S$ respectively \code{$S$.\id}.
+
+\LMHash{}
+Execution of $s$ proceeds as follows:
+The argument list
 \code{($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
-is evaluated.
-
-\LMHash{}
-Then the superconstructor is executed as follows:
-
-\LMHash{}
-Let $C$ be the class in which the superinitializer appears and let $S$ be the superclass of $C$.
-If $S$ is generic (\ref{generics}), let $U_1, \ldots, U_p$ be the actual type arguments passed to $S$,
-obtained by substituting $V_1, \ldots, V_m$ for the formal parameters in the superclass clause of $C$.
-
-\LMHash{}
-The generative constructor $S$ (respectively \code{$S$.\id}) of $S$ is executed
-to initialize $i$ with respect to the bindings that resulted from the evaluation of
-\code{($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)},
-and the type parameters (if any) of class $S$ bound to $U_1, \ldots, U_p$.
-
-\LMHash{}
-It is a compile-time error if class $S$ does not declare a generative constructor named $S$ (respectively \code{$S$.\id}).
+is evaluated to an actual argument list $a$ of the form
+\code{($o_1, \ldots,\ o_n,\ x_{n+1}$: $o_{n+1}, \ldots,\ x_{n+k}$: $o_{n+k}$)}.
+Then the body of the superconstructor $k$ is executed
+in an environment where the formal parameters of $k$ are bound to
+the corresponding actual arguments from $a$,
+and the formal type parameters of $S$ are bound to $u_1, \ldots, u_p$.
 
 
 \subsubsection{Factories}
@@ -2066,6 +2214,15 @@
 The {\em redirectee constructor} for this declaration is then the constructor denoted by $R$.
 
 \LMHash{}
+A redirecting factory constructor $q'$ is {\em redirection-reachable}
+from a redirecting factory constructor $q$ if{}f
+$q'$ is the redirectee constructor of $q$,
+or $q''$ is the redirectee constructor of $q$
+and $q'$ is redirection-reachable from $q''$.
+It is a compile-time error if a redirecting factory constructor
+is redirection-reachable from itself.
+
+\LMHash{}
 Let $\argumentList{T}$ be the static argument list type (\ref{actualArgumentLists})
 \code{($T_1 \ldots,\ T_{n+k}$)}
 when $k$ takes no named arguments, and
@@ -2214,7 +2371,7 @@
 }
 
 \LMHash{}
-It is a compile-time error if a constant constructor is declared by a class that has a non-final instance variable.
+It is a compile-time error if a constant constructor is declared by a class that has a mutable instance variable.
 
 \commentary{
 The above refers to both locally declared and inherited instance variables.
@@ -2355,51 +2512,6 @@
 }
 
 
-\subsection{Static Variables}
-\LMLabel{staticVariables}
-
-\LMHash{}
-{\em Static variables} are variables whose declarations are immediately contained within a class declaration and that are declared \STATIC{}.
-The static variables of a class $C$ are those static variables declared by $C$.
-
-%A static variable declaration of one of the forms \code{\STATIC{} $T$ $v$;}, \code{\STATIC{} $T$ $v$ = $e$;}, \code{\STATIC{} \CONST{} $T$ $v$ = $e$;} or \code{\STATIC{} \FINAL{} $T$ $v$ = $e$;} always induces an implicit static getter function (\ref{getters}) with signature
-
-%\STATIC{} $T$ \GET{} $v$
-
-%whose invocation evaluates as described below (\ref{evaluationOfStaticVariableGetters}).%to the value stored in $v$.
-
-%A static variable declaration of one of the forms \code{\STATIC{} \VAR{} $v$;}, \code{\STATIC{} \VAR{} $v$ = $e$;}, \code{\STATIC{} \CONST{} $v$ = $e$;} or \code{\STATIC{} \FINAL{} $v$ = $e$;} always induces an implicit static getter function with signature
-
-%\STATIC{} \GET{} $v$
-
-%whose invocation evaluates as described below (\ref{evaluationOfStaticVariableGetters}).%to the value stored in $v$.
-
-%A non-final static variable declaration of the form \code{\STATIC{} $T$ $v$;} or the form \code{\STATIC{} $T$ $v$ = $e$;} always induces an implicit static setter function (\ref{setters}) with signature
-
-%\STATIC{} \VOID{} \SET{} $v=(T$ $x)$
-
-%whose execution sets the value of $v$ to the incoming argument $x$.
-
-%A static variable declaration of the form \code{\STATIC{} \VAR{} $v$;} or the form \code{\STATIC{} \VAR{} $v$ = $e$;} always induces an implicit static setter function with signature
-
-%\STATIC{} \SET{} $v=(x)$
-
-%whose execution sets the value of $v$ to the incoming argument $x$.
-
-%Extrernal static functions, getters, setters
-
-%\subsubsection{Evaluation of Implicit Static Variable Getters}
-%\LMLabel{evaluationOfStaticVariableGetters}
-
-%Let $d$ be the declaration of a static variable $v$. The implicit getter method of $v$ executes as follows:
-%\begin{itemize}
-%\item If $d$ is of one of the forms \code{\STATIC{} \VAR{} $v$ = $e$;} , \code{\STATIC{} $T$ $v$ = $e$; }, \code{\STATIC{} \FINAL{} $v$ = $e$; } or \code{\STATIC{} \FINAL{} $T$ $v$ = $e$;} and no value has yet been stored into $v$ then the initializer expression $e$ is evaluated. If, during the evaluation of $e$, the getter for $v$ is referenced, a \code{CyclicInitializationError} is thrown. If the evaluation succeeded yielding an object $o$, let $r$ be $o$, otherwise let $r$ be the null object (\ref{null}). In any case, $r$ is stored into $v$. The result of executing the getter is $r$.
-%\item If $d$ is of one of the forms \code{\STATIC{} \CONST{} $v$ = $e$; } or \code{\STATIC{} \CONST{} $T$ $v$ = $e$;} the result of the getter is the value of the compile-time constant $e$.
-%Otherwise
-%\item The result of executing the getter method is the value stored in $v$.
-%\end{itemize}
-
-
 \subsection{Superclasses}
 \LMLabel{superclasses}
 
@@ -2449,6 +2561,8 @@
 \end{dartCode}
 
 \LMHash{}
+%% TODO(eernst): Consider replacing all occurrences of `a superclass`
+%% by `a direct or indirect superclass`, because it's too confusing.
 A class $S$ is {\em a superclass} of a class $C$ if{}f either:
 \begin{itemize}
 \item $S$ is the superclass of $C$, or
@@ -2463,11 +2577,11 @@
 \subsubsection{Inheritance and Overriding}
 \LMLabel{inheritanceAndOverriding}
 
-%A class $C$ {\em inherits} any accessible instance members of its superclass that are not overridden by members declared in $C$.
-
 \LMHash{}
-Let $C$ be a class, let $A$ be a superclass of $C$, and let $S_1, \ldots, S_k$ be superclasses of $C$ that are also subclasses of $A$.
-$C$ {\em inherits} all accessible instance members of $A$ that have not been overridden by a declaration in $C$ or in at least one of $S_1, \ldots, S_k$.
+Let $C$ be a class, let $A$ be a superclass of $C$, and
+let $S_1, \ldots, S_k$ be superclasses of $C$ that are also subclasses of $A$.
+$C$ {\em inherits} all concrete, accessible instance members of $A$
+that have not been overridden by a concrete declaration in $C$ or in at least one of $S_1, \ldots, S_k$.
 
 \rationale{
 It would be more attractive to give a purely local definition of inheritance, that depended only on the members of the direct superclass $S$.
@@ -2481,11 +2595,16 @@
 A class may override instance members that would otherwise have been inherited from its superclass.
 
 \LMHash{}
-Let $C = S_0$ be a class declared in library $L$, and let $\{S_1, \ldots, S_k\}$ be the set of all superclasses of $C$, where $S_i$ is the superclass of $S_{i-1}$ for $i \in 1 .. k$.
-Let $C$ declare a member $m$, and let $m'$ be a member of $S_j, j \in 1 .. k$, that has the same name as $m$, such that $m'$ is accessible to $L$.
-Then $m$ overrides $m'$ if $m'$ is not already overridden by a member of at least one of $S_1, \ldots, S_{j-1}$ and neither $m$ nor $m'$ are instance variables.
-
-%Let $C$ be a class declared in library $L$, with superclass $S$ and let $C$ declare an instance member $m$, and assume $S$ declares an instance member $m'$ with the same name as $m$. Then $m$ {\em overrides} $m'$ if{}f $m'$ is accessible (\ref{privacy}) to $L$, $m$ has the same name as $m'$ and neither $m$ nor $m'$ are fields.
+Let $C = S_0$ be a class declared in library $L$, and
+let $\{S_1, \ldots, S_k\}$ be the set of all superclasses of $C$,
+where $S_i$ is the superclass of $S_{i-1}$ for $i \in 1 .. k$.
+\commentary{This means that $S_k$ is the built-in class \code{Object}.}
+Let $C$ declare a concrete member $m$, and
+let $m'$ be a concrete member of $S_j, j \in 1 .. k$, that has the same name as $m$,
+such that $m'$ is accessible to $L$.
+Then $m$ overrides $m'$
+if $m'$ is not already overridden by a concrete member of at least one of $S_1, \ldots, S_{j-1}$
+and neither $m$ nor $m'$ are instance variables.
 
 \commentary{
 Instance variables never override each other.
@@ -2514,53 +2633,126 @@
 Finally, static members never override anything.
 }
 
+\LMHash{}
+Let $C$ be a concrete class
+whose interface has an accessible member $m$ named \id{}.
+It is a compile-time error if $C$ does not have
+a concrete member $m'$ named \id{} which is a correct override of $m$,
+unless $C$ has a concrete method named \code{noSuchMethod}
+which is different from the one in the built-in class \code{Object},
+and $C$ does not have a concrete member named \id.
+
 \commentary{
-For convenience, here is a summary of the relevant rules, using `error' to denote compile-time errors.
+So it is an error even if $C$ does have a concrete member $m'$ named \id{}
+if $m'$ is an \emph{incorrect} override of $m$,
+also when $C$ has a \code{noSuchMethod} which is not from \code{Object}.
+Note that it is allowed to let inaccessible methods remain unimplemented;
+invocations of such methods will be redirected to \code{noSuchMethod}.
+}
+
+%% TODO(eernst): Why don't we just get rid of this list entirely?
+%% It's 'for convenience', but that's not otherwise a priority in this
+%% document, it is more important that it is correct and consistent.
+\commentary{
+For convenience, here is a summary of the relevant rules,
+using `error' to denote compile-time errors.
 Remember that this is not normative.
 The controlling language is in the relevant sections of the specification.
 
 \begin{enumerate}
 
-\item There is only one namespace for getters, setters, methods and constructors (\ref{scoping}).
-  An instance or static variable $f$ introduces a getter $f$ and a non-final instance or static variable $f$ also introduces a setter $f=$ (\ref{instanceVariables}, \ref{staticVariables}).
-  When we speak of members here, we mean accessible instance or static variables, getters, setters, and methods (\ref{classes}).
-\item You cannot have two members with the same name in the same class - be they declared or inherited (\ref{scoping}, \ref{classes}).
+\item There is only one namespace
+  for getters, setters, methods and constructors (\ref{scoping}).
+  An instance or static variable $f$ introduces a getter $f$,
+  and a mutable instance or static variable $f$ also introduces a setter
+  \code{$f$=} (\ref{instanceVariables}, \ref{staticVariables}).
+  When we speak of members here, we mean
+  accessible instance or static variables, getters, setters, and methods
+  (\ref{classes}).
+\item You cannot have two members with the same name in the same class---be
+  they declared or inherited (\ref{scoping}, \ref{classes}).
 \item Static members are never inherited.
-\item It is an error if you have an static member named $m$ in your class and an instance member of the same name (\ref{classMemborConflicts}).
-\item It is an error if you have a static setter $v=$, and an instance member $v$ (\ref{setters}).
-\item It is an error if you have a static getter $v$ and an instance setter $v=$ (\ref{getters}).
-\item If you define an instance member named $m$, and your superclass has an instance member of the same name, they override each other.
-This may or may not be legal.
+\item It is an error if you have a static member named $m$ in your class
+  and an instance member of the same name (\ref{classMemberConflicts}).
+\item It is an error if you have a static setter \code{$v$=},
+  and an instance member $v$ (\ref{setters}).
+\item It is an error if you have a static getter $v$
+  and an instance setter \code{$v$=} (\ref{getters}).
+\item If you define an instance member named $m$,
+  and your superclass has an instance member of the same name,
+  they override each other.
+  This may or may not be legal.
 \item \label{typeSigAssignable}
-%% TODO(eernst): This is commentary, but we may need to adjust it to say 'correctly overrides'.
-If two members override each other, it is an error if their type signatures are not assignable to each other (\ref{instanceMethods}, \ref{getters}, \ref{setters}) (and since these are function types, this means the same as "subtypes of each other").
+  %% TODO(eernst): This is commentary, but we may need to adjust it
+  %% to say 'correctly overrides'.
+  If two members override each other,
+  it is an error if their type signatures are not assignable to each other
+  (\ref{instanceMethods}, \ref{getters}, \ref{setters})
+  %% TODO(eernst): Revisit relative to the new subtyping.md rules.
+  (and since these are function types, this means the same as
+  "subtypes of each other").
 \item \label{requiredParams}
-If two members override each other, it is an error if the overriding member has more required parameters than the overridden one (\ref{instanceMethods}).
+  If two members override each other,
+  it is an error if the overriding member has
+  more required parameters than the overridden one (\ref{instanceMethods}).
 \item \label{optionalPositionals}
-If two members override each other, it is an error if the overriding member has fewer positional parameters than the overridden one (\ref{instanceMethods}).
+  If two members override each other,
+  it is an error if the overriding member has
+  fewer positional parameters than the overridden one (\ref{instanceMethods}).
 \item \label{namedParams}
-If two members override each other, it is an error if the overriding member does not have all the named parameters that the overridden one has (\ref{instanceMethods}).
-\item Setters, getters and operators never have optional parameters of any kind; it's an error (\ref{operators}, \ref{getters}, \ref{setters}).
-\item It is an error if a member has the same name as its enclosing class (\ref{classes}).
+  If two members override each other,
+  it is an error if the overriding member does not have
+  all the named parameters that the overridden one has (\ref{instanceMethods}).
+\item Setters, getters and operators never have
+  optional parameters of any kind;
+  it's an error (\ref{operators}, \ref{getters}, \ref{setters}).
+\item
+  It is an error if a member has the same name as its enclosing class
+  (\ref{classes}).
 \item A class has an implicit interface (\ref{classes}).
-\item Superinterface members are not inherited by a class, but are inherited by its implicit interface.
-Interfaces have their own inheritance rules (\ref{interfaceInheritanceAndOverriding}).
-\item A member is abstract if it has no body and is not labeled \EXTERNAL{} (\ref{abstractInstanceMembers}, \ref{externalFunctions}).
-\item A class is abstract if{}f it is explicitly labeled \ABSTRACT{}.% or if it declares (not just inherits) an abstract member (\ref{classes}).
-\item It is an error if a concrete class has an abstract member (declared or inherited).
-\item It is an error to call a non-factory constructor of an abstract class using an instance creation expression (\ref{instanceCreation}),
-  such a constructor may only be invoked from another constructor using a super invocation (\ref{superinvocation}).
+\item Superinterface members are not inherited by a class,
+  but are inherited by its implicit interface.
+  Interfaces have their own inheritance rules
+  (\ref{interfaceInheritanceAndOverriding}).
+\item A member is abstract if
+  it has no body and is not labeled \EXTERNAL{}
+  (\ref{abstractInstanceMembers}, \ref{externalFunctions}).
+\item A class is abstract if{}f it is explicitly labeled \ABSTRACT{}.
+\item It is an error if a concrete class has an abstract member
+  (declared or inherited), and there is no \code{noSuchMethod}.
+\item It is an error to call a non-factory constructor of an abstract class
+  using an instance creation expression (\ref{instanceCreation}),
+  such a constructor may only be invoked from another constructor
+  using a super invocation (\ref{superInvocation}).
 \item If a class defines an instance member named $m$,
   and any of its superinterfaces have a member named $m$,
   the interface of the class contains the $m$ from the class itself.
-\item An interface inherits all members of its superinterfaces that are not overridden and not members of multiple superinterfaces.
-\item If multiple superinterfaces of an interface define a member with the same name $m$, then at most one member is inherited.
-%% TODO(eernst): Switch to use 'correctly overrides' terminology.
-That member (if it exists) is the one whose type is a subtype of all the others.
-If there is no such member, then an error occurs (\ref{interfaceInheritanceAndOverriding}).
-\item Rule \ref{typeSigAssignable} applies to interfaces as well as classes (\ref{interfaceInheritanceAndOverriding}).
-\item It is an error if a concrete class does not have an implementation for a method in any of its superinterfaces unless it has a concrete \code{noSuchMethod} method (\ref{superinterfaces}) distinct from the one in class \code{Object}.
-\item The identifier of a named constructor cannot be the same as the name of a member declared (as opposed to inherited) in the same class (\ref{constructors}).
+\item
+  %% TODO(eernst): This needs to be updated when we introduce the
+  %% new override/conflict rules.
+  An interface inherits all members of its superinterfaces
+  that are not overridden and not members of multiple superinterfaces.
+\item
+  %% TODO(eernst): This must be rewritten when we introduce the new
+  %% override/conflict rules.
+  If multiple superinterfaces of an interface
+  define a member with the same name $m$,
+  then at most one member is inherited.
+  %% TODO(eernst): Switch to use 'correctly overrides' terminology.
+  That member (if it exists) is the one whose type is a subtype
+  of all the others.
+  If there is no such member, then an error occurs
+  (\ref{interfaceInheritanceAndOverriding}).
+\item Rule \ref{typeSigAssignable} applies to interfaces as well as classes
+  (\ref{interfaceInheritanceAndOverriding}).
+\item It is an error if a concrete class does not have an implementation
+  for a method in any of its superinterfaces
+  unless it has a concrete \code{noSuchMethod} method
+  (\ref{superinterfaces})
+  distinct from the one in class \code{Object}.
+\item The identifier of a named constructor cannot be
+  the same as the name of a static member declared in the same class
+  (\ref{classMemberConflicts}).
 \end{enumerate}
 }
 
@@ -2785,7 +2977,7 @@
 A mixin application of the form \code{$S$ \WITH{} $M$;} for the name $N$ defines a class $C$ with superclass $S$ and name $N$.
 
 \LMHash{}
-A mixin application of the form \code{$S$ \WITH{} $M_1,\ \ldots, M_k$;} for the name $N$ defines a class $C$ whose superclass is the application of the mixin composition (\ref{mixinComposition}) $M_{k-1} * \ldots * M_1$ to $S$ of a name that is a fresh identifer, and whose name is $N$.
+A mixin application of the form \code{$S$ \WITH{} $M_1,\ \ldots,\ M_k$;} for the name $N$ defines a class $C$ whose superclass is the application of the mixin composition (\ref{mixinComposition}) $M_{k-1} * \ldots * M_1$ to $S$ of a name that is a fresh identifer, and whose name is $N$.
 \rationale{The name of the resulting class is necessary because it is part of the names of the introduced constructors.}
 
 \LMHash{}
@@ -2977,7 +3169,10 @@
 
 \commentary{
 This allows non-generic cases to be included implicitly as special cases.
-For example, an invocation of a non-generic function arises as the special case where the function takes zero type arguments, and zero type arguments are passed.
+For example,
+an invocation of a non-generic function arises as the special case
+where the function takes zero type arguments,
+and zero type arguments are passed.
 In this situation some operations are also omitted (have no effect), e.g.,
 operations where formal type parameters are replaced by actual type arguments.
 }
@@ -3688,7 +3883,7 @@
 \item \NULL{} (\ref{null}).
 \item A qualified reference to a static constant variable (\ref{variables}) that is not qualified by a deferred prefix.
 \commentary{
-For example, If class C declares a constant static variable v, C.v is a constant.
+For example, if class C declares a constant variable v, C.v is a constant.
 The same is true if C is accessed via a prefix p; p.C.v is a constant unless p is a deferred prefix.
 }
 \item An identifier expression that denotes a constant variable.
@@ -4377,10 +4572,12 @@
 
 \LMHash{}
 It is a compile-time error if either a key or a value of an entry in a constant map literal is not a compile-time constant.
-It is a compile-time error if the key of an entry in a constant map literal is an instance of a class that implements the operator $==$ unless the key is a
-%symbol,
-string, an integer, a literal symbol or the result of invoking a constant constructor of class \code{Symbol}.
-It is a compile-time error if the type arguments of a constant map literal include a type parameter.
+It is a compile-time error if the key of an entry in a constant map literal is an instance of
+a class that has a concrete operator \code{==} declaration different from the one in \code{Object},
+unless the key is a string or an integer,
+or the key expression is a literal symbol or
+an invocation of a constant constructor of class \code{Symbol}.
+It is a compile-time error if the type arguments of a constant map literal include a type variable.
 
 \LMHash{}
 The value of a constant map literal \CONST{}$ <K, V>\{k_1:e_1, \ldots, k_n :e_n\}$ is an object $m$ whose class implements the built-in class $Map<K, V>$.
@@ -4531,16 +4728,16 @@
 
 \code{<$X_1\ B_1, \ldots,\ X_m\ B_m$>}
 
-\code{($T_1, \ldots,\ T_n, $ [$T_{n+1}\ x_{n+1}, \ldots,\ T_{n+k}\ x_{n+k}$]) $ \rightarrow$ Future<$flatten(T_0)$>},
+\code{($T_1, \ldots,\ T_n, $ [$T_{n+1}\ x_{n+1}, \ldots,\ T_{n+k}\ x_{n+k}$]) $ \rightarrow$ Future<\flatten{T_0}>},
 
 \noindent
 where $T_0$ is the static type of $e$.
 
 \LMHash{}
-In the previous two paragraphs, the type argument lists are omitted in the case where $m = 0$, and $flatten(T)$ is defined as follows:
+In the previous two paragraphs, the type argument lists are omitted in the case where $m = 0$, and \flatten{T} is defined as follows:
 
 \begin{itemize}
-\item If \code{$T =$ FutureOr<$S$>} then $flatten(T) = S$.
+\item If $T$ is \code{FutureOr<$S$>} for some $S$ then $\flatten{T} = S$.
 
 \item Otherwise if
 \code{$T <:$ Future}
@@ -4560,9 +4757,9 @@
 Note that $S$ is well-defined because of the requirements on superinterfaces.
 }
 
-Then $flatten(T) = S$.
+Then $\flatten{T} = S$.
 
-\item In any other circumstance, $flatten(T) = T$.
+\item In any other circumstance, $\flatten{T} = T$.
 \end{itemize}
 
 \LMHash{}
@@ -4592,7 +4789,7 @@
 
 \code{<$X_1 B_1, \ldots,\ X_m B_m$>}
 
-\code{($T_1, \ldots,\ T_n, $ \{$T_{n+1}\ x_{n+1}, \ldots,\ T_{n+k}\ x_{n+k}$\}) $ \rightarrow$ Future<$flatten(T_0)$>},
+\code{($T_1, \ldots,\ T_n, $ \{$T_{n+1}\ x_{n+1}, \ldots,\ T_{n+k}\ x_{n+k}$\}) $ \rightarrow$ Future<\flatten{T_0}>},
 
 \noindent
 where $T_0$ is the static type of $e$.
@@ -4726,7 +4923,17 @@
 \LMLabel{instanceCreation}
 
 \LMHash{}
-Instance creation expressions invoke constructors to produce instances.
+Instance creation expressions generally produce instances
+and invoke constructors to initialize them.
+
+\commentary{
+The exception is that
+a factory constructor invocation works like a regular function call.
+It may of course evaluate an instance creation expression and thus
+produce a fresh instance,
+but no fresh instances are created as a direct consequence of
+the factory constructor invocation.
+}
 
 %It is a compile-time error if any of the type arguments to a constructor of a generic type invoked by a new expression or a constant object expression do not denote types in the enclosing lexical scope.
 
@@ -4743,21 +4950,11 @@
 \code{\CONST{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)},
 
 \code{\CONST{} $T$($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
-is malformed (\ref{staticTypes}) or malbounded (\ref{parameterizedTypes}).
 
-\LMHash{}
-It is a compile-time error if the type $T$ in an instance creation expression of one of the forms
-
-\code{\NEW{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)},
-
-\code{\NEW{} $T$($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)},
-
-\code{\CONST{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)},
-
-\code{\CONST{} $T$($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
-
-is an enumerated type (\ref{enums}).
-%any of the type arguments to a constructor of a generic type $G$ invoked by a new expression or a constant object expression are not subtypes of the bounds of the corresponding formal type parameters of $G$.
+\noindent
+is malformed (\ref{staticTypes}),
+is malbounded (\ref{parameterizedTypes}),
+or is an enumerated type (\ref{enums}).
 
 
 \subsubsection{New}
@@ -4780,95 +4977,153 @@
 \code{\NEW{} $T$($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
 
 \LMHash{}
-If $T$ is a class or parameterized type accessible in the current scope then:
-\begin{itemize}
-\item
-If $e$ is of the form
-\code{\NEW{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}:\ a_{n+1}, \ldots,\ x_{n+k}:\ a_{n+k}$)}
-it is a compile-time error if \code{$T$.\id} is not the name of a constructor declared by the type $T$.
-\item
-If $e$ is of the form
-\code{\NEW{} $T$($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
-it is a compile-time error if the type $T$ does not declare a constructor with the same name as the declaration of $T$.
-\end{itemize}
+It is a compile-time error if $T$ is not
+a class or a parameterized type accessible in the current scope,
+or if $T$ is a parameterized type which is not a class.
+\commentary{
+For instance, \code{\NEW{} F<int>()} is an error if \code{F} is a type alias.
+}
 
 \LMHash{}
 If $T$ is a parameterized type (\ref{parameterizedTypes})
 \code{$S$<$U_1, \ldots,\ U_m$>},
-let $R = S$.
-%It is a
-%compile-time CHANGED
-%run-time type
-%error if $S$ is not a generic (\ref{generics}) type with $m$ type parameters.
-If $T$ is not a parameterized type, let $R = T$.
-Furthermore, if $e$ is of the form
-\code{\NEW{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
-then let $q$ be the constructor \code{$T$.\id}, otherwise let $q$ be the constructor $T$.
+let $R$ be the generic class $S$,
+and let
+\code{$X_1\ \EXTENDS\ B_1, \ldots,\ X_p\ \EXTENDS\ B_p$}
+be the formal type parameters of $S$.
+If $T$ is not a parameterized type, let $R$ be $T$.
 
-\LMHash{}
-If $R$ is a generic with $l = m$ type parameters then
 \begin{itemize}
-\item If $T$ is not a parameterized type, then for $ i \in 1 .. l$, let $V_i = \DYNAMIC{}$.
-\item If $T$ is a parameterized type then let $V_i = U_i$ for $ i \in 1 .. m$.
+\item
+  If $e$ is of the form
+  \code{\NEW{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
+  it is a compile-time error if \code{$R$.\id} is not the name of
+  a constructor declared by $R$, or \id{} is not accessible.
+\item
+  If $e$ is of the form
+  \code{\NEW{} $T$($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
+  it is a compile-time error if $R$ is not the name of
+  a constructor declared by $R$.
 \end{itemize}
 
 \LMHash{}
-If $R$ is a generic with $l \ne m$ type parameters then for $ i \in 1 .. l$, let $V_i = \DYNAMIC{}$.
-In any other case, let $V_i = U_i$ for $ i \in 1 .. m$.
+Let $q$ be the above-mentioned constructor named \code{$R$.\id} or $R$.
+
+\LMHash{}
+It is a compile-time error if $R$ is abstract
+and $q$ is not a factory constructor.
+It is a compile-time error if $R$ is a non-generic class
+and $T$ is a parameterized type.
+%% We assume that inference has taken place, so actual type arguments
+%% are always given explicitly.
+It is a compile-time error if $R$ is a generic class
+and $T$ is not a parameterized type.
+It is a compile-time error if $R$ is a generic class,
+$T$ is a parameterized type, and $m \not= p$.
+\commentary{That is, the number of type arguments is incorrect.}
+It is a compile-time error if $R$ is a generic class,
+$T$ is a parameterized type,
+and $T$ is not regular-bounded
+(\ref{superBoundedTypes}).
+
+\LMHash{}
+If $q$ is a redirecting factory constructor,
+it is a compile-time error if $q$ in some number of
+redirecting factory redirections redirects to itself.
+\commentary{
+It is possible and allowed for a redirecting factory $q'$
+to enter an infinite loop, e.g.,
+because $q'$ redirects to a non-redirecting factory constructor
+$q''$ whose body uses $q'$ in an instance creation expression.
+Only loops that consist exclusively of redirecting factory redirections
+are detected at compile time.
+}
+
+\LMHash{}
+Let $S_i$ be the static type of
+the formal parameter of the constructor \code{$R$.\id} (respectively $R$)
+corresponding to the actual argument $a_i$, $i \in 1 .. n+k$.
+It is a compile-time error if the static type of
+$a_i, i \in 1 .. n + k$
+is not assignable to $[U_1/X_1, \ldots, U_m/X_m]S_i$.
+\commentary{
+The non-generic case is covered with $m = 0$.
+}
+
+\LMHash{}
+The static type of $e$ is $T$.
 
 \LMHash{}
 Evaluation of $e$ proceeds as follows:
 
 \LMHash{}
-First, the argument list
-\code{($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
-is evaluated.
+First, the argument part
+
+\code{<$U_1, \ldots,\ U_m$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
+
+\noindent
+is evaluated, yielding the evaluated actual argument part
+
+\code{<$u_1, \ldots,\ u_m$>($o_1, \ldots,\ o_n,\ x_{n+1}$: $o_{n+1},\ \ldots,\ x_{n+k}$: $o_{n+k}$)}.
+
+\noindent
+\commentary{Note that the non-generic case is covered by letting $m = 0$.}
+If for any
+$j \in 1 .. n + k$
+the run-time type of $o_j$ is not a subtype of
+$[u_1/X_1, \ldots, u_m/X_m]S_j$,
+a dynamic error occurs.
 
 \LMHash{}
+\Case{Non-loaded deferred constructors}
 If $T$ is a deferred type with prefix $p$, then if $p$ has not been successfully loaded, a dynamic error occurs.
 
 \LMHash{}
-Then, if $q$ is a non-factory constructor of an abstract class then an \code{AbstractClassInstantiationError} is thrown.
+\Case{Generative constructors}
+When $q$ is a generative constructor
+(\ref{generativeConstructors})
+evaluation proceeds to allocate a fresh instance
+(\ref{generativeConstructors}), $i$, of class $T$.
+% We provide the type arguments as part of the class of the instance
+% because $T$ includes the type arguments; but we also provide them
+% as a binding accessible to the constructor: Otherwise we couldn't
+% access the type parameters in the initializing expressions of the
+% initializer list where there is no access to \THIS{}.
+Then $q$ is executed to initialize $i$ with respect to
+the bindings that resulted from the evaluation of the argument list, and,
+if $R$ is a generic class,
+with its type parameters bound to $u_1, \ldots, u_m$.
 
 \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 fewer than $n$ positional parameters or more than $n$ required parameters,
-or if $q$ lacks any of the named parameters $\{ x_{n+1}, \ldots, x_{n+k}\}$ a \code{NoSuchMethodError} is thrown.
-
-\LMHash{}
-Otherwise, if $q$ is a generative constructor (\ref{generativeConstructors}), then:
-
-\commentary{
-Note that at this point we are assured that the number of actual type arguments match the number of formal type parameters.
-}
-
-\LMHash{}
-A fresh instance (\ref{generativeConstructors}), $i$, of class $R$ is allocated.
-Then $q$ is executed to initialize $i$ with respect to the bindings that resulted from the evaluation of the argument list, and, if $R$ is a generic class, with its type parameters bound to $V_1, \ldots, V_m$.
-
 If execution of $q$ completes normally (\ref{completion}), $e$ evaluates to $i$.
 Otherwise execution of $q$ throws an exception object $x$ and stack trace $t$,
 and then evaluation of $e$ also throws exception object $x$ and stack trace $t$
 (\ref{evaluation}).
 
 \LMHash{}
-Otherwise, $q$ is a factory constructor (\ref{factories}).
-Then:
+\Case{Redirecting factory constructors}
+When $q$ is a redirecting factory constructor
+(\ref{factories})
+of the form \code{\CONST{}? $T$($p_1, \ldots,\ p_{n+k}$) = $c$;} or
+of the form \code{\CONST{}? $T$.\id($p_1, \ldots,\ p_{n+k}$) = $c$;}
+where \code{\CONST{}?} indicates that \CONST{} may be present or absent,
+the remaining evaluation of $e$ is equivalent to
+evaluating
+\code{\NEW{} $c$($v_1, \ldots,\ v_n,\ x_{n+1}$: $v_{n+1}, \ldots,\ x_{n+k}$: $v_{n+k}$)}
+in an environment where
+$v_j$ is a fresh variable bound to $o_j$ for $j \in 1 .. n + k$, and
+$X_j$ is bound to $u_j$ for $j \in 1 .. m$.
+\commentary{
+We need access to the type variables because $c$ may contain them.
+}
 
 \LMHash{}
-If $q$ is a redirecting factory constructor of the form $T(p_1, \ldots,\ p_{n+k}) = c;$ or of the form \code{$T$.\id($p_1, \ldots,\ p_{n+k}$) = $c$;} then the result of the evaluation of $e$ is equivalent to evaluating the expression
-
-\code{[$V_1/X_1, \ldots, V_m/X_m$](\NEW{} $c$($a_1, \ldots,\ a_n, x_{n+1}: a_{n+1}, \ldots,\ x_{n+k}: a_{n+k}$))}
-
-\noindent
-where $X_1, \ldots,\ X_m$ are the formal type parameters of $R$.
-If evaluation of $q$ causes $q$ to be re-evaluated cyclically, with only factory constructor redirections in-between, a run-time error occurs.
-% Used to not have the "in-between" clause, which would disallow a factory constructor redirecting to another constructor which conditionally calls the original factory constructor again with different arguments.
-
-\LMHash{}
-Otherwise, the body of $q$ is executed with respect to the bindings that resulted from the evaluation of the argument list, and with the type parameters (if any) of $q$ bound to the actual type arguments $V_1, \ldots, V_l$.
+\Case{Non-redirecting factory constructors}
+When $q$ is a non-redirecting factory constructor,
+the body of $q$ is executed with respect to
+the bindings that resulted from the evaluation of the argument list,
+and with the type parameters, if any, of $q$ bound to
+the actual type arguments $u_1, \ldots, u_m$.
 If this execution returns a value (\ref{completion}),
 then $e$ evaluates to the returned value.
 Otherwise, if the execution completes normally or returns with no value,
@@ -4876,144 +5131,182 @@
 Otherwise the execution throws an exception $x$ and stack trace $t$,
 and then evaluation of $e$ also throws $x$ and $t$ (\ref{evaluation}).
 
-\LMHash{}
-It is a compile-time error if $q$ is a constructor of an abstract class and $q$ is not a factory constructor.
-
-\commentary{
-The above gives precise meaning to the idea that instantiating an abstract class leads to an error.
-A similar clause applies to constant object creation in the next section.
-}
-
 \rationale{
-In particular, a factory constructor can be declared in an abstract class and used safely,
+A factory constructor can be declared in an abstract class and used safely,
 as it will either produce a valid instance or throw.
 }
 
-\LMHash{}
-The static type of an instance creation expression of either the form
-
-\code{\NEW{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}:\ a_{n+1}, \ldots,\ x_{n+k}:\ a_{n+k}$)}
-
-or the form
-
-\code{\NEW{} $T$($a_1, \ldots,\ a_n,\ x_{n+1}:\ a_{n+1}, \ldots,\ x_{n+k}:\ a_{n+k}$)}
-
-is $T$.
-It is a compile-time error if the static type of $a_i, 1 \le i \le n + k$ may not be assigned to the type of the corresponding formal parameter of the constructor \code{$T$.\id} (respectively $T$).
-
 
 \subsubsection{Const}
 \LMLabel{const}
 
 \LMHash{}
-A {\em constant object expression} invokes a constant constructor (\ref{constantConstructors}).
+A {\em constant object expression} invokes a constant constructor
+(\ref{constantConstructors}).
 
 \begin{grammar}
-{\bf constObjectExpression:}\CONST{} type ('{\escapegrammar .}' identifier)? arguments
+{\bf constObjectExpression:}\NEW{} type (`{\escapegrammar .}' identifier)? arguments
   .
 \end{grammar}
 
 \LMHash{}
 Let $e$ be a constant object expression of the form
 
-\code{\CONST{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}:\ a_{n+1}, \ldots,\ x_{n+k}:\ a_{n+k}$)}
-
+\code{\CONST{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
 or the form
-\code{\CONST{} $T$($a_1, \ldots,\ a_n,\ x_{n+1}:\ a_{n+1}, \ldots,\ x_{n+k}:\ a_{n+k}$)}.
-It is a compile-time error if $T$ does not denote a class accessible in the current scope.
-It is a compile-time error if $T$ is a deferred type (\ref{staticTypes}).
 
+\code{\CONST{} $T$($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
+
+\LMHash{}
+It is a compile-time error if $T$ is not
+a class or a parameterized type accessible in the current scope,
+or if $T$ is a parameterized type which is not a class.
+It is a compile-time error if $T$ is a deferred type
+(\ref{staticTypes}).
 \commentary{
-In particular, $T$ may not be a type variable.
+For instance, $T$ can not be a type variable.
 }
 
 \LMHash{}
-If $T$ is a parameterized type, it is a compile-time error if $T$ includes a type variable among its type arguments.
+It is a compile-time error if $a_i$ is not a constant expression
+for some $i \in 1 .. n + k$.
 
 \LMHash{}
-If $e$ is of the form
-\code{\CONST{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}:\ a_{n+1}, \ldots,\ x_{n+k}:\ a_{n+k}$)}
-it is a compile-time error if \code{$T$.\id} is not the name of a constant constructor declared by the type $T$.
-If $e$ is of the form
-\code{\CONST{} $T$($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
-it is a compile-time error if the type $T$ does not declare a constant constructor with the same name as the declaration of $T$.
+If $T$ is a parameterized type (\ref{parameterizedTypes})
+\code{$S$<$U_1, \ldots,\ U_m$>},
+let $R$ be the generic class $S$,
+and let
+\code{$X_1\ \EXTENDS\ B_1, \ldots,\ X_p\ \EXTENDS\ B_p$}
+be the formal type parameters of $S$.
+If $T$ is not a parameterized type, let $R$ be $T$.
 
 \LMHash{}
-In all of the above cases, it is a compile-time error if $a_i, i\in 1 .. n + k$, is not a compile-time constant expression.
+If $T$ is a parameterized type,
+it is a compile-time error if $U_j$ contains a type variable for any
+$j \in 1 .. m$.
 
-%If $T$ is a parameterized type (\ref{parameterizedTypes}) $S<U_1, \ldots,\ U_m>$, let $R = S$.  It is a compile-time error if $T$ is malformed. If $T$ is not a parameterized type, let $R = T$.
-%Finally,
-% If $T$ is a generic with $l$ retype parameters, then for all $ i \in 1 .. l$, let $V_i = \DYNAMIC{}$.
+\begin{itemize}
+\item
+  If $e$ is of the form
+  \code{\CONST{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
+  it is a compile-time error if \code{$R$.\id} is not the name of
+  a constant constructor declared by $R$, or \id{} is not accessible.
+\item
+  If $e$ is of the form
+  \code{\CONST{} $T$($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
+  it is a compile-time error if $R$ is not the name of
+  a constant constructor declared by $R$.
+\end{itemize}
+
+\LMHash{}
+Let $q$ be the above-mentioned constant constructor named \code{$R$.\id} or $R$.
+
+%% TODO(eernst): These errors are the same as with `new`. Can we avoid
+%% stating them twice? We'd need to refer to an awkwardly shaped portion
+%% of text in the previous subsection, or just loosely say "exactly the
+%% same errors"..
+\LMHash{}
+It is a compile-time error if $R$ is abstract
+and $q$ is not a factory constructor.
+It is a compile-time error if $R$ is a non-generic class
+and $T$ is a parameterized type.
+%% We assume that inference has taken place, so actual type arguments
+%% are always given explicitly.
+It is a compile-time error if $R$ is a generic class
+and $T$ is not a parameterized type.
+It is a compile-time error if $R$ is a generic class,
+$T$ is a parameterized type, and $m \not= p$.
+\commentary{That is, the number of type arguments is incorrect.}
+It is a compile-time error if $R$ is a generic class,
+$T$ is a parameterized type,
+and $T$ is not regular-bounded
+(\ref{superBoundedTypes}).
+
+\LMHash{}
+Let $S_i$ be the static type of
+the formal parameter of the constructor \code{$R$.\id} (respectively $R$)
+corresponding to the actual argument $a_i$, $i \in 1 .. n+k$.
+It is a compile-time error if the static type of
+$a_i, i \in 1 .. n + k$
+is not assignable to $[U_1/X_1, \ldots, U_m/X_m]S_i$.
+\commentary{
+The non-generic case is covered with $m = 0$.
+}
+
+\LMHash{}
+The static type of $e$ is $T$.
 
 \LMHash{}
 Evaluation of $e$ proceeds as follows:
 
 \LMHash{}
-First, if $e$ is of the form
-
-\code{\CONST{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}:\ a_{n+1}, \ldots,\ x_{n+k}:\ a_{n+k}$)}
-
-then let $i$ be the value of the expression
-
-\code{\NEW{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}:\ a_{n+1}, \ldots,\ x_{n+k}:\ a_{n+k}$)}.
+If $e$ is of the form
+\code{\CONST{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
+let $i$ be the value of the expression $e'$:
+\code{\NEW{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
+\commentary{
+Let $o$ be the result of an evaluation of $e'$,
+at some point in time of some execution of the program
+in the library $L$ where $e$ occurs.
+The result of an evaluation of $e'$ in $L$
+at some other time and/or in some other execution will
+yield a result $o'$, such that $o'$ would be replaced by $o$
+by canonicalization as described below.
+This means that the value is well-defined.
+}
 
 \LMHash{}
-Otherwise, $e$ must be of the form
-
+If $e$ is of the form
 \code{\CONST{} $T$($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)},
-
-in which case let $i$ be the result of evaluating
-
+let $i$ be the value of
 \code{\NEW{} $T$($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
+\commentary{
+Which is well-defined for the same reason.
+}
 
 \LMHash{}
-Then:
 \begin{itemize}
-\item If during execution of the program, a constant object expression has already evaluated to an instance $j$ of class $R$ with type arguments $V_i, 1 \le i \le m$, then:
+\item If during execution of the program,
+  a constant object expression has already evaluated to
+  an instance $j$ of class $R$ with type arguments $U_i, 1 \le i \le m$, then:
 \begin{itemize}
-\item For each instance variable $f$ of $i$, let $v_{if}$ be the value of the instance variable $f$ in $i$, and let $v_{jf}$ be the value of the instance variable $f$ in $j$.
-  If \code{identical($v_{if}$, $v_{jf}$)} for all instance variables $f$ in $i$ then the value of $e$ is $j$, otherwise the value of $e$ is $i$.
+\item For each instance variable $f$ of $i$,
+  let $v_{if}$ be the value of the instance variable $f$ in $i$, and
+  let $v_{jf}$ be the value of the instance variable $f$ in $j$.
+  If \code{identical($v_{if}$, $v_{jf}$)} for all instance variables $f$ in $i$
+  then the value of $e$ is $j$, otherwise the value of $e$ is $i$.
 \end{itemize}
 \item Otherwise the value of $e$ is $i$.
 \end{itemize}
 
 \commentary{
 In other words, constant objects are canonicalized.
-In order to determine if an object is actually new, one has to compute it; then it can be compared to any cached instances.
-If an equivalent object exists in the cache, we throw away the newly created object and use the cached one.
-Objects are equivalent if they have identical type arguments and identical instance variables.
-Since the constructor cannot induce any side effects, the execution of the constructor is unobservable.
+In order to determine if an object is actually new, one has to compute it;
+then it can be compared to any cached instances.
+If an equivalent object exists in the cache,
+we throw away the newly created object and use the cached one.
+Objects are equivalent if
+they have identical type arguments and identical instance variables.
+Since the constructor cannot induce any side effects,
+the execution of the constructor is unobservable.
 The constructor need only be executed once per call site, at compile time.
 }
 
 \LMHash{}
-The static type of a constant object expression of either the form
-
-\code{\CONST{} $T$.\id($a_1, \ldots,\ a_n,\ x_{n+1}:\ a_{n+1}, \ldots,\ x_{n+k}:\ a_{n+k}$)}
-
-or the form
-
-\code{\CONST{} $T$($a_1, \ldots,\ a_n,\ x_{n+1}:\ a_{n+1}, \ldots,\ x_{n+k}:\ a_{n+k}$)}
-
-is $T$.
-It is a compile-time error if the static type of $a_i, 1 \le i \le n+ k$ may not be assigned to the type of the corresponding formal parameter of the constructor \code{$T$.\id} (respectively $T$).
-
-\LMHash{}
-It is a compile-time error if evaluation of a constant object results in an uncaught exception being thrown.
+It is a compile-time error if evaluation of a constant object
+results in an uncaught exception being thrown.
 
 \commentary{
 To see how such situations might arise, consider the following examples:
 }
 
+%% TODO(eernst): Delete some \CONST{} when integrating implicit-creation.md
 \begin{dartCode}
 \CLASS{} A \{
    \FINAL{} x;
    \CONST{} A(p): x = p * 10;
 \}
 
-\CONST{} A("x"); // compile-time error
-\CONST{} A(5); // legal
-
 \CLASS{} IntPair \{
   \CONST{} IntPair(\THIS{}.x, \THIS{}.y);
   \FINAL{} int x;
@@ -5021,16 +5314,22 @@
   \OPERATOR *(v) => \NEW{} IntPair(x*v, y*v);
 \}
 
-\CONST{} A(\CONST{} IntPair(1,2)); // compile-time error: illegal in a subtler way
+\CONST a1 = \CONST{} A(true); // compile-time error
+\CONST a2 = \CONST{} A(5); // legal
+\CONST a3 = \CONST{} A(\CONST{} IntPair(1,2)); // compile-time error
 \end{dartCode}
 
 \commentary{
-Due to the rules governing constant constructors, evaluating the constructor \code{A()} with the argument \code{"x"} or the argument \code{\CONST{} IntPair(1, 2)} would cause it to throw an exception, resulting in a compile-time error.
+Due to the rules governing constant constructors,
+evaluating the constructor \code{A()}
+with the argument \code{"x"} or the argument \code{\CONST{} IntPair(1, 2)}
+would cause it to throw an exception, resulting in a compile-time error.
+In the latter case, the error is caused by the fact that
+\code{\OPERATOR{} *} can only be used with a few ``well-known'' types,
+which is required in order to avoid running arbitrary code during
+the evaluation of constant expressions.
 }
 
-\LMHash{}
-Given an instance creation expression of the form \CONST{} $q(a_1, \ldots,\ a_n)$ it is a compile-time error if $q$ is a constructor of an abstract class (\ref{abstractInstanceMembers}) but $q$ is not a factory constructor.
-
 
 \subsection{Spawning an Isolate}
 \LMLabel{spawningAnIsolate}
@@ -5284,7 +5583,8 @@
 and binding of the results to the function's formal parameters.
 
 \LMHash{}
-When parsing an argument list, an ambiguity may arise because the same source code could be one generic function invocation, and it could be two or more relational expressions and/or shift expressions.
+When parsing an argument list, an ambiguity may arise because the same source code could be one generic function invocation,
+and it could be two or more relational expressions and/or shift expressions.
 In this situation, the expression is always parsed as a generic function invocation.
 
 % Should we specify the precise disambiguation rule here?:
@@ -5323,35 +5623,75 @@
 \subsubsection{Binding Actuals to Formals}
 \LMLabel{bindingActualsToFormals}
 
-\LMHash{}
-Let $f$ be a function with $s$ type parameters and $h$ required parameters;
-let $p_1, \ldots, p_n$ be the positional parameters of $f$;
-and let $p_{h+1}, \ldots, p_{h+k}$ be the optional parameters declared by $f$.
-
 \commentary{
-Note that the type argument lists in the following are omitted in the case where $s = 0$,
+In the following, the non-generic case is covered implicitly:
+When the number of actual type arguments is zero
+the entire type argument list \code{<\ldots{}>} is omitted,
 and similarly for empty type parameter lists (\ref{generics}).
 }
 
 \LMHash{}
-An evaluated actual argument part
-\code{<$t_1, \ldots,\ t_r$>($o_1, \ldots,\ o_{m+l}$)}
-derived from an actual argument part of the form
+Consider an invocation $i$ of a function $f$ with an actual argument part of the form
+\code{<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_m,\ q_1$: $a_{m+1}, \ldots,\ q_l$: $a_{m+l}$)}.
 
-\code{<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_m,\ q_1$: $a_{m+1}, \ldots,\ q_l$: $a_{m+l}$)}
+\commentary{
+Note that $f$ denotes a function in a semantic sense,
+rather than a syntactic construct.
+A reference to this section is used in other sections
+when the static analysis of an invocation is specified,
+and the static type of $f$ has been determined.
+The function itself may have been obtained from a function declaration,
+from an instance bound to \THIS{} and an instance method declaration,
+or as a function object obtained by evaluation of an expression.
+Because of that, we cannot indicate here which syntactic construct
+corresponds to $f$.
+%
+A reference to this section is also used in other sections
+when actual arguments are to be bound to the corresponding formal parameters,
+and $f$ is about to be invoked, to specify the dynamic semantics.
+}
 
-\noindent
-is bound to the formal type parameters and formal parameters of $f$ as follows:
+\commentary{
+We do not call $f$ a `function object' here, because we do not wish to imply
+that every function invocation must involve a separate evaluation
+of an expression that yields a function object,
+followed by an invocation of that function object.
+For instance, an implementation should be allowed to compile the invocation
+of a top-level function as a series of steps whereby a stack frame is
+created, followed by a low-level jump to the generated code for the body.
+So, in this section,
+the word `function' is more low-level than `function object',
+but `function' still denotes a semantic entity
+which is associated with a function declaration,
+even though there may not be corresponding entity in the heap at run time.
+}
+
+\LMHash{}
+% We cannot pass the same named parameter twice.
+It is a compile-time error if $q_j = q_k$ for any $j \ne k$.
+
+\LMHash{}
+If the static type of $f$ is \DYNAMIC{} or the built-in class \FUNCTION{},
+no further static checks are performed and the static type of $i$ is \DYNAMIC{};
+otherwise, it is a compile-time error if the static type of $f$ is not a function type.
+
+\LMHash{}
+Otherwise, the static type of $f$ is a function type $F$.
+Let $S_0$ be the return type of $F$,
+let $X_1\ \EXTENDS\ B_1, \ldots, X_s\ \EXTENDS\ B_s$
+be the formal type parameters,
+let $h$ be the number of required parameters,
+let $p_1, \ldots, p_n$ be the positional parameters,
+and let $p_{h+1}, \ldots, p_{h+k}$ be the optional parameters of $F$.
+Let $S_i$ be the static type of the formal parameters $p_i, i \in 1 .. h+k$,
+and for each $q$ let $S_q$ be the type of the parameter named $q$,
+where each parameter type is obtained by replacing $X_j$ by $A_j, j \in 1 .. s$, in the given parameter type annotation.
+Finally, let $T_i$ be the static type of $a_i$.
 
 \commentary{
 We have an actual argument list consisting of $r$ type arguments, $m$ positional arguments, and $l$ named arguments.
 We have a function with $s$ type parameters, $h$ required parameters, and $k$ optional parameters.
-The number of type arguments must match the number of type parameters.
-The number of positional arguments must be at least as large as the number of required parameters, and no larger than the number of positional parameters.
-All named arguments must have a corresponding named parameter.
-A given named argument cannot be provided more than once.
-If an optional parameter has no corresponding argument, it gets its default value.
-In checked mode, all arguments must belong to subtypes of the type of their corresponding formal.
+Figure~\ref{fig:argumentsAndParameters} shows how this situation may arise.
 }
 
 % View on declaration:
@@ -5364,7 +5704,99 @@
 % Actual argument part:
 %
 %     |**   ...        *|**           ...          *|**     ...       *|
-%      <-r type par.s--> <----m positional arg.s---> <--l named arg.s->
+%      <-r type arg.s--> <----m positional arg.s---> <--l named arg.s->
+\begin{figure}[h]
+  \def\A#1{\mbox{\commentary{{#1} arguments}}}
+  \def\P#1{\mbox{\commentary{{#1} parameters}}}
+  %
+  \flushleft{\commentary{Actual arguments:}}
+  \begin{displaymath}
+    \begin{array}{rl}
+      \left<\A{$r$ type}\right>
+      \left(
+      \begin{array}{r@{,\;}l}
+        \A{$m$ positional}&\A{$l$ named}
+      \end{array}
+      \right)
+    \end{array}
+  \end{displaymath}
+  %
+  \flushleft{\commentary{Declaration with named parameters: $n = h$}}
+  \begin{displaymath}
+    \begin{array}{rl}
+      \left<\P{$s$ type}\right>
+      \left(
+      \begin{array}{r@{,\;}l}
+        \P{$h$ required}&\P{$k$ optional}\\
+        \multicolumn{2}{c}{\mbox{\scriptsize\textit{which may also be viewed as}}}\\
+        \P{$n$ positional}&\P{$k$ named}\\
+      \end{array}
+      \right)
+    \end{array}
+  \end{displaymath}
+  %
+  \flushleft{\commentary{Declaration with optional positional parameters: $n = h + k$}}
+  \begin{displaymath}
+    \begin{array}{rl}
+      \left<\P{$s$ type}\right>
+      \left(
+      \begin{array}{r@{,\;}l}
+        \P{$h$ required}&\P{$k$ optional}\\
+        \multicolumn{2}{c}{\mbox{\scriptsize\textit{which may also be viewed as}}}\\
+        \multicolumn{2}{c}{\P{$n$ positional}}
+      \end{array}
+      \right)
+    \end{array}
+  \end{displaymath}
+  %
+  \caption{Possible actual argument parts and formal parameter parts}
+  \label{fig:argumentsAndParameters}
+\end{figure}
+
+\LMHash{}
+% Type inference is assumed complete, so we must have the correct number of type arguments.
+It is a compile-time error if $r \not= s$.
+It is a compile-time error if $r = s$ and for some $j \in 1 .. s$,
+$A_j \not<: [A_1/X_1, \ldots, A_r/X_s]B_j$.
+It is a compile-time error unless $h \le m \le n$.
+If $l > 0$,
+it is a compile-time error unless $F$ has named parameters and
+$q_j \in \{p_{h+1}, \ldots, p_{h+k}\}, j \in 1 .. l$.
+
+\commentary{
+That is, the number of type arguments must match the number of type parameters,
+and the bounds must be respected.
+We must receive at least the required number of positional arguments,
+and not more than the total number of positional parameters.
+For each named argument there must be a named parameter with the same name.
+}
+
+\LMHash{}
+The static type of $i$ is $[A_1/X_1, \ldots, A_r/X_s]S_0$.
+
+\LMHash{}
+It is a compile-time error if $T_j$ may not be assigned to $S_j, j \in 1 .. m$.
+It is a compile-time error if $T_{m+j}$ may not be assigned to $S_{q_j}, j \in 1 .. l$.
+
+\LMHash{}
+For the dynamic semantics,
+let $f$ be a function with $s$ type parameters and $h$ required parameters;
+let $p_1, \ldots, p_n$ be the positional parameters of $f$;
+and let $p_{h+1}, \ldots, p_{h+k}$ be the optional parameters declared by $f$.
+
+\LMHash{}
+An evaluated actual argument part
+
+\code{<$t_1, \ldots,\ t_r$>($o_1, \ldots,\ o_m,\ q_1$: $o_{m+1},\ \ldots,\ q_l$: $o_{m+l}$)}
+
+\noindent
+derived from an actual argument part of the form
+
+\code{<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_m,\ q_1$: $a_{m+1}, \ldots,\ q_l$: $a_{m+l}$)}
+
+\noindent
+is bound to the formal type parameters and formal parameters of $f$ as follows:
+
 \LMHash{}
 % Passing a wrong number of actual type arguments.
 If $r = 0$ and $s > 0$ then replace the actual type argument list:
@@ -5372,7 +5804,7 @@
 %% should be chosen based on the instantiate-to-bound algorithm, but we
 %% cannot yet refer to that because it hasn't yet been specified here.
 let $r$ be $s$ and $t_i = \DYNAMIC{}$ for $i \in 1 .. s$.
-If $r \not= s$, a \code{NoSuchMethodError} is thrown.
+Then, if $r \not= s$, a \code{NoSuchMethodError} is thrown.
 % Passing named arguments to a function with optional positional parameters.
 If $l > 0$ and $n \not= h$, a \code{NoSuchMethodError} is thrown.
 % Passing too few or too many positional arguments.
@@ -5401,32 +5833,6 @@
 % Check the types of named arguments.
 In checked mode, it is a dynamic type error if $o_{m+j}$ is not the null object and the actual type (\ref{actualTypeOfADeclaration}) of $q_j$ is not a supertype of the type of $o_{m+j}, j \in 1 .. l$.
 
-\LMHash{}
-% We cannot pass the same named parameter twice.
-It is a compile-time error if $q_i = q_j$ for any $i \ne j$.
-
-\LMHash{}
-Let $T_i$ be the static type of $a_i$.
-If the static type of $f$ is \DYNAMIC{} or the built-in class \FUNCTION{},
-no further static checks are performed.
-Otherwise, it is a compile-time error if the static type of $f$ is not a function type.
-
-\LMHash{}
-Otherwise, let $X_1, \ldots, X_s$ be the formal type parameters of the static type of $f$,
-let $S_i$ be the type of $p_i, i \in 1 .. h+k$,
-and let $S_q$ be the type of the named parameter $q$ of $f$,
-where each parameter type is obtained by replacing $X_j$ by $A_j, j \in 1 .. s$, in the given parameter type annotation.
-
-\commentary{
-Checks regarding the number of type parameters and their bounds is specified in (\ref{generics}).
-}
-
-\LMHash{}
-It is a compile-time error if $T_j$ may not be assigned to $S_j, j \in 1 .. m$.
-It is a compile-time error if $m < h$ or if $m > n$.
-Furthermore, each $q_i, i \in 1 .. l$, must have a corresponding named parameter in the set $\{p_{h+1}, \ldots, p_{h+k}\}$ or a compile-time error occurs.
-It is a compile-time error if $T_{m+j}$ may not be assigned to $S_{q_j}, j \in 1 .. l$.
-
 
 \subsubsection{Unqualified Invocation}
 \LMLabel{unqualifiedInvocation}
@@ -5444,36 +5850,45 @@
 }
 
 \LMHash{}
-If there exists a lexically visible declaration named \id, let $f_{id}$ be the innermost such declaration.
+It is a compile-time error if $i$ occurs inside a top-level or static function
+(be it function, method, getter, or setter)
+or a top-level or static variable initializer,
+and there is no lexically visible declaration named \id{} in scope.
+
+\LMHash{}
+If there exists a lexically visible declaration named \id,
+let $f_{id}$ be the innermost such declaration.
 Then:
 \begin{itemize}
+\item It is a compile-time error if $f_{id}$ denotes a type
+  (\commentary{that is, if \id{} is a type literal or type variable}),
+  unless \id{} denotes a constructor.
+\item It is a compile-time error if $f_{id}$ is an import directive
+  where \id{} is declared to be a library prefix.
 \item
-If \id{} is a type literal, then $i$ is interpreted as a function expression invocation (\ref{functionExpressionInvocation}) with $(\id)$ as the expression $e_f$.
-\commentary{
-The expression $(\id)$ where \id{} is a type literal always evaluates to an instance of class \code{Type} which is not a function.
-This ensures that a run-time error occurs when trying to call a type literal.
-}
+If $f_{id}$ is
+a local function,
+a library function,
+a library or static getter or a variable,
+$i$ is interpreted as a function expression invocation
+(\ref{functionExpressionInvocation}).
 \item
-If $f_{id}$ is a prefix object, a compile-time error occurs.
-\item
-If $f_{id}$ is a local function, a library function, a library or static getter or a variable then $i$ is interpreted as a function expression invocation (\ref{functionExpressionInvocation}).
-\item
-Otherwise, if $f_{id}$ is a static method of the enclosing class $C$, $i$ is equivalent to
-\code{$C$.\id<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}:\ a_{n+1}, \ldots,\ x_{n+k}:\ a_{n+k}$)}.
-\item Otherwise, $f_{id}$ is equivalent to the ordinary method invocation
+Otherwise, if $f_{id}$ is a static method of the enclosing class $C$,
+$i$ is equivalent to
+\code{$C$.\id<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
+\item Otherwise, if $i$ occurs in an instance method body,
+$i$ is equivalent to the ordinary method invocation
 
 \code{\THIS{}.\id<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
 \end{itemize}
 
-\LMHash{}
-Otherwise, if $i$ occurs inside a top level or static function (be it function, method, getter, or setter) or variable initializer, evaluation of $i$ causes a \code{NoSuchMethodError} to be thrown.
-
-\LMHash{}
-If $i$ does not occur inside a top level or static function, $i$ is equivalent to
-\code{\THIS{}.\id<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
-
-% Should also say:
-% It is a compile-time error if $i$ occurs inside a top level or static function (be it function, method, getter, or setter) or variable initializer and there is no lexically visible declaration named \id{} in scope.
+\commentary{
+Otherwise $i$ must occur inside a top-level or static function
+(be it function, method, getter, or setter)
+or a top-level or static variable initializer,
+in which case a compile-time error occurs
+(\ref{unqualifiedInvocation}).
+}
 
 
 \subsubsection{Function Expression Invocation}
@@ -5492,15 +5907,22 @@
 }
 
 \LMHash{}
-If $e_f$ is an identifier \id, then \id{} must necessarily denote a local function, a library function, a library or static getter or a variable as described above, or $i$ is not considered a function expression invocation.
-If $e_f$ is a type literal, then it is equivalent to the expression $(e_f)$.
+If $e_f$ is an identifier \id, then \id{} must necessarily denote
+a local function, a library function, a library or static getter or a variable as described above,
+or $i$ is not considered a function expression invocation.
+It is a compile-time error if $e_f$ is a type literal,
+unless $e_f$ denotes a constructor.
 
 \commentary{
-The expression $(e_f)$ where $e_f$ is a type literal always evaluates to an instance of class \code{Type} which is not a function.
-This ensures that a run-time error occurs when trying to call a type literal.
+This error was already specified elsewhere
+(\ref{unqualifiedInvocation})
+for the case where $e_f$ is an identifier,
+but $e_f$ may also have other forms, e.g., \code{p.C}.
 }
 
-If $e_f$ is a property extraction expression (\ref{propertyExtraction}), then $i$ isn't a function expression invocation and is instead recognized as an ordinary method invocation (\ref{ordinaryInvocation}).
+\LMHash{}
+If $e_f$ is a property extraction expression (\ref{propertyExtraction}),
+then $i$ isn't a function expression invocation and is instead recognized as an ordinary method invocation (\ref{ordinaryInvocation}).
 
 \commentary{
 \code{$a.b(x)$} is parsed as a method invocation of method \code{$b()$} on object \code{$a$}, not as an invocation of getter \code{$b$} on \code{$a$} followed by a function call \code{$(a.b)(x)$}.
@@ -5510,103 +5932,62 @@
 }
 
 \LMHash{}
-Otherwise, evaluation of a function expression invocation
+Let $F$ be the static type of $e_f$.
+The static analysis of $i$ is performed as specified in Section~\ref{bindingActualsToFormals},
+and the static type of $i$ is as specified there.
+
+\LMHash{}
+Evaluation of a function expression invocation
 
 \code{$e_f$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
 
 \noindent
 proceeds to evaluate $e_f$, yielding an object $o$.
 Let $f$ be a fresh variable bound to $o$.
-If $o$ is a function object then the following function invocation is evaluated
-and its result is the result of evaluating $i$:
+If $o$ is a function object then the function invocation
 
 \code{$f$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
 
-\noindent
-Otherwise, if $o$ has a method named \CALL{},
-the following method invocation is evaluated and its result is the result of evaluating $i$:
+is evaluated by binding actuals to formals as specified in Section~\ref{bindingActualsToFormals},
+and executing the body of $f$ with those bindings;
+the returned result is then the result of evaluating $i$.
+
+\LMHash{}
+Otherwise $o$ is not a function object.
+If $o$ has a method named \CALL{}
+the following ordinary method invocation is evaluated,
+and its result is then the result of evaluating $i$:
 
 \code{$f$.call<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
 
-\noindent
-Otherwise, when $o$ has no method named \CALL{},
-a new instance $im$ of the predefined class \code{Invocation} is created, such that:
+\LMHash{}
+Otherwise $o$ has no method named \CALL{}.
+A new instance $im$ of the predefined class \code{Invocation} is created, such that:
 \begin{itemize}
-\item \code{im.isMethod} evaluates to \code{\TRUE{}}.
-\item \code{im.memberName} evaluates to the symbol \code{\#call}.
-\item \code{im.positionalArguments} evaluates to an unmodifiable list with the values
+\item \code{$im$.isMethod} evaluates to \code{\TRUE{}}.
+\item \code{$im$.memberName} evaluates to the symbol \code{\#call}.
+\item \code{$im$.positionalArguments} evaluates to an unmodifiable list with the values
 resulting from evaluation of
 \code{<Object>[$a_1, \ldots,\ a_n$]}.
-\item \code{im.namedArguments} evaluates to an unmodifiable map
+\item \code{$im$.namedArguments} evaluates to an unmodifiable map
 with the keys and values resulting from evaluation of
 
-\code{<Symbol, Object>\{$\#x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $\#a_{n+k}$\}}.
-\item \code{im.typeArguments} evaluates to an unmodifiable list
+\code{<Symbol, Object>\{$\#x_{n+1}$: $a_{n+1}, \ldots,\ \#x_{n+k}$: $a_{n+k}$\}}.
+\item \code{$im$.typeArguments} evaluates to an unmodifiable list
 with the values resulting from evaluation of
 \code{<Type>[$A_1, \ldots,\ A_r$]}.
 \end{itemize}
 
 \LMHash{}
 Then the method invocation \code{f.noSuchMethod($im$)} is evaluated,
-and its result is the result of evaluating $i$.
-
-\LMHash{}
-Let $F$ be the static type of $e_f$.
-It is a compile-time error unless one of the following conditions is satisfied:
-\begin{enumerate}
-\item $F$ is \DYNAMIC{}.
-\item $F$ is \FUNCTION{}.
-\item\label{InvocationTypeListNamed}
-$F$ is a function type
-
-\code{<$X_1\ \EXTENDS\ B_1, \ldots,\ A_s\ \EXTENDS\ B_s$>}
-
-\code{($T_1, \ldots,\ T_n,\ $\{$T_{n+1}\ x_{n+1}, \ldots,\ T_{n+k}\ x_{n+k}, \ldots,\ T_{n+k+p}\ x_{n+k+p}$\}) $ \rightarrow T_0$}
-
-\noindent
-where $r = s$, and the static type of $a_j$ is assignable to
-$[A_1/X_1, \ldots, A_r/X_s]T_j$, for all $j \in 1 .. n+k$.
-
-\item\label{InvocationTypeListPositional}
-$k$ is zero, $0 \leq m \leq n$, and $F$ is a function type
-
-\code{<$X_1\ \EXTENDS\ B_1, \ldots,\ A_s\ \EXTENDS\ B_s$>}
-
-\code{($T_1, \ldots,\ T_m,\ $[$T_{m+1}, \ldots,\ T_n, \ldots,\ T_{n+p}$]) $ \rightarrow T_0$}
-
-\noindent
-where $r = s$, and the static type of $a_j$ is assignable to
-$[A_1/X_1, \ldots, A_r/X_s]T_j$,
-for all $j \in 1 .. n$.
-
-\item\label{InvocationTypeListCall}
-$F$ is an interface type that has a method named \CALL{}, and then,
-considering $F$ to denote the function type of that method,
-criterion~\ref{InvocationTypeListNamed} or~\ref{InvocationTypeListPositional}
-in this list is satisfied.
-\end{enumerate}
+and its result is then the result of evaluating $i$.
 
 \commentary{
-This means that the types of the actual arguments must match the declared types of the corresponding parameters,
-where the formal type parameters have been replaced by the actual type arguments.
-%
-Note that the type parameter lists are omitted when $s = 0$ (\ref{generics}),
-and that checks on the number of type arguments and their bounds is specified elsewhere (\ref{generics}).
-%
-Criterion~\ref{InvocationTypeListCall} ensures that
-a function expression invocation may amount to an invocation of the instance method \CALL{}
-when such a method is statically known,
-and the run-time semantics ensures that
-a function invocation may amount to an invocation of the instance method \CALL{}
-also for an invocation of a function of type \DYNAMIC{} or \FUNCTION{},
-but that an interface type with a method named \CALL{} is not itself a subtype of any function type.
+The run-time semantics ensures that
+a function invocation may amount to an invocation of the instance method \CALL{}.
+However, an interface type with a method named \CALL{} is not itself a subtype of any function type.
 }
 
-\LMHash{}
-If $F$ is not a function type or $r \not= s$, the static type of $i$ is \DYNAMIC{}.
-Otherwise, the static type of $i$ is the return type
-$[A_1/X_1, \ldots, A_r/X_s]T_0$ of $F$.
-
 
 \subsection{Function Closurization}
 \LMLabel{functionClosurization}
@@ -5650,38 +6031,79 @@
 \subsection{Lookup}
 \LMLabel{lookup}
 
-
-\subsubsection{Method Lookup}
-\LMLabel{methodLookup}
-
 \LMHash{}
-The result of a lookup of a method $m$ in object $o$ with respect to library $L$ is the result of a lookup of method $m$ in class $C$ with respect to library $L$, where $C$ is the class of $o$.
+A {\em lookup} is a procedure which selects
+a concrete instance member declaration based on a traversal of
+a sequence of classes, starting with a given class $C$
+and proceeding with the superclass of the current class at each step.
+A lookup may be part of the static analysis, and it may be performed
+at run time. It may succeed or fail.
 
-\LMHash{}
-The result of a lookup of method $m$ in class $C$ with respect to library $L$ is:
-If $C$ declares a concrete instance method named $m$ that is accessible to $L$, then that method is the result of the lookup, and we say that the method was {\em looked up in $C$}.
-Otherwise, if $C$ has a superclass $S$, then the result of the lookup is the result of looking up $m$ in $S$ with respect to $L$.
-Otherwise, we say that the method lookup has failed.
-
-\rationale{
-The motivation for skipping abstract members during lookup is largely to allow smoother mixin composition.
+\commentary{
+We define several kinds of lookup with a very similar structure.
+We spell out each of them in spite of the redundancy,
+in order to avoid introducing meta-level abstraction mechanisms just for this purpose.
+The point is that we must indicate for each lookup which kind of member it is looking for,
+because, e.g., a `method lookup' and a `getter lookup' are used in different situations.
 }
 
+{ % Scope for 'lookup' definition.
 
-\subsubsection{Getter and Setter Lookup}
-\LMLabel{getterAndSetterLookup}
+\def\LookupDefinitionWithStart#1{
+\LMHash{}
+The result of a
+{\em {#1} lookup for $m$ in $o$ with respect to $L$ starting in class $C$}
+is the result of a {#1} lookup for $m$ in $C$ with respect to $L$.
+The result of a {\em {#1} lookup for $m$ in $C$ with respect to $L$} is:
+If $C$ declares a concrete instance {#1} named $m$
+that is accessible to $L$,
+then that {#1} declaration is the result of the {#1} lookup,
+and we say that the {#1} was {\em looked up in $C$}.
+Otherwise, if $C$ has a superclass $S$,
+the result of the {#1} lookup is
+the result of a {#1} lookup for $m$ in $S$ with respect to $L$.
+Otherwise, we say that the {#1} lookup has failed.
+
+}
 
 \LMHash{}
-The result of a lookup of a getter (respectively setter) $m$ in object $o$ with respect to library $L$ is the result of looking up getter (respectively setter) $m$ in class $C$ with respect to $L$, where $C$ is the class of $o$.
+Let $m$ be an identifier, $o$ an object, $L$ a library,
+and $C$ a class which is the class of $o$ or a superclass thereof.
+
+\LookupDefinitionWithStart{method}
+\LookupDefinitionWithStart{getter}
+\LookupDefinitionWithStart{setter}
+
+\def\LookupDefinition#1{%
+The result of a
+{\em {#1} lookup for $m$ in $o$ with respect to $L$}
+is the result of a
+{#1} lookup for $m$ in $o$ with respect to $L$
+starting with the class of $o$.
+}
 
 \LMHash{}
-The result of a lookup of a getter (respectively setter) $m$ in class $C$ with respect to library $L$ is:
-If $C$ declares a concrete instance getter (respectively setter) named $m$ that is accessible to $L$, then that getter (respectively setter) is the result of the lookup, and we say that the getter (respectively setter) was {\em looked up in $C$}.
-Otherwise, if $C$ has a superclass $S$, then the result of the lookup is the result of looking up getter (respectively setter) $m$ in $S$ with respect to $L$.
-Otherwise, we say that the lookup has failed.
+Let $m$ be an identifier, $o$ an object, and $L$ a library.
+\LookupDefinition{method}
+\LookupDefinition{getter}
+\LookupDefinition{setter}
+
+} % End of scope for lookup definitions.
+
+\commentary{
+Note that for getter (setter) lookup, the result may be
+a getter (setter) which has been induced by an instance variable
+declaration.
+}
+
+\commentary{
+Note that we sometimes use phrases like `looking up method $m$'
+to indicate that a method lookup is performed,
+and similarly for setter lookups and getter lookups.
+}
 
 \rationale{
-The motivation for skipping abstract members during lookup is largely to allow smoother mixin composition.
+The motivation for ignoring abstract members during lookup is largely to allow smoother mixin composition.
 }
 
 
@@ -5713,6 +6135,14 @@
 \subsubsection{Ordinary Invocation}
 \LMLabel{ordinaryInvocation}
 
+\LMHash{}
+An ordinary method invocation can be {\em conditional} or {\em unconditional}.
+
+\LMHash{}
+\Case{\code{$e$?.$m$<$\cdots$>($\cdots$)}}
+Consider a {\em conditional ordinary method invocation} $i$ of the form
+\code{$e$?.$m$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
+
 \commentary{
 Note that non-generic invocations arise as the special case where the number of type arguments is zero,
 in which case the type argument list is omitted,
@@ -5720,30 +6150,6 @@
 }
 
 \LMHash{}
-An ordinary method invocation can be {\em conditional} or {\em unconditional}.
-
-\LMHash{}
-Evaluation of a {\em conditional ordinary method invocation} $i$ of the form
-
-\code{$e$?.$m$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
-
-\noindent
-proceeds as follows:
-
-\LMHash{}
-If $e$ is a type literal, $i$ is equivalent to
-
-\code{$e.m$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
-
-\LMHash{}
-Otherwise, evaluate $e$ to an object $o$.
-If $o$ is the null object, $i$ evaluates to the null object (\ref{null}).
-Otherwise let $v$ be a fresh variable bound to $o$ and evaluate
-\code{$v$.$m$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
-to a value $r$.
-Then $e$ evaluates to $r$.
-
-\LMHash{}
 The static type of $i$ is the same as the static type of
 
 \code{$e$.$m$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
@@ -5754,106 +6160,141 @@
 \code{$e$.$m$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
 
 \noindent
-are also generated in the case of
-
-\code{$e$?.$m$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
+are also generated in the case of $i$.
 
 \LMHash{}
-An {\em unconditional ordinary method invocation} $i$ has the form
+Evaluation of $i$ proceeds as follows:
+
+\LMHash{}
+If $e$ is a type literal, $i$ is equivalent to
 
 \code{$e$.$m$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
 
 \LMHash{}
+Otherwise, evaluate $e$ to an object $o$.
+If $o$ is the null object, $i$ evaluates to the null object (\ref{null}).
+Otherwise let $v$ be a fresh variable bound to $o$ and evaluate
+\code{$v$.$m$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
+to a value $r$.
+Then $e$ evaluates to $r$.
+
+\LMHash{}
+\Case{\code{$e$.$m$<$\cdots$>($\cdots$)}}
+An {\em unconditional ordinary method invocation} $i$ has the form
+\code{$e$.$m$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
+
+\commentary{
+Non-generic invocations again arise as the special case
+where the number of type arguments is zero (\ref{generics}).
+}
+
+\LMHash{}
+Let $T$ be the static type of $e$.
+It is a compile-time error if $T$ does not have an accessible (\ref{privacy}) instance member named $m$, unless either:
+\begin{itemize}
+\item
+%% TODO(eernst): This is metaclass stuff, should be deleted.
+$T$ is \code{Type}, $e$ is a constant type literal,
+and the class corresponding to $e$ has a static getter named $m$.
+Or
+\item $T$ is \DYNAMIC{}.
+Or
+\item $T$ is \FUNCTION{} and $m$ is \CALL.
+\rationale{
+This means that for invocations of an instance method named \CALL,
+a receiver of type \FUNCTION{} is treated like a receiver of type \DYNAMIC{}.
+The expectation is that any concrete subclass of \FUNCTION{} will implement \CALL,
+but there is no method signature which can be assumed for \CALL{} in \FUNCTION{}
+because every signature will conflict with some potential overriding declarations.
+Note that any use of \CALL{} on a subclass of \FUNCTION{} that fails to implement \CALL{} will provoke a compile-time error,
+as this exemption is limited to type \FUNCTION{}, and does not apply to its subtypes.
+}
+\end{itemize}
+
+\LMHash{}
+If $T$ did not have an accessible member named $m$ the static type of $i$ is \DYNAMIC{},
+and no further static checks are performed on $i$
+(\commentary{except that subexpressions of $i$ are subject to their own static analysis}).
+
+\LMHash{}
+Otherwise \code{$T$.$m$} denotes an instance member.
+Let $L$ be the library that contains $i$.
+Let $d$ be the result of method lookup for $m$ in $T$ with respect to $L$,
+and if the method lookup succeeded then let $F$ be the static type of $d$.
+Otherwise, let $d$ be the result of getter lookup for $m$ in $T$ with respect to $L$
+and let $F$ be the return type of $d$.
+(\commentary{Since \code{$T$.$m$} exists we cannot have a failure in both lookups.})
+
+\LMHash{}
+The static analysis of $i$ is performed as specified in Section~\ref{bindingActualsToFormals},
+and the static type of $i$ is as specified there.
+
+\LMHash{}
+It is a compile-time error to invoke any of the methods of class \code{Object} on a prefix object (\ref{imports})
+or on a constant type literal that is immediately followed by the token `.'\,.
+
+\rationale{
+The reason for the latter is that this syntax is reserved for invocation of static methods.
+For instance, \code{int.toString()} is similar to \code{C.someStaticMethod()}, and
+it would be confusing if just a couple of expressions of this form were instance method invocations.
+If needed, \code{(int).toString()} may be used instead.
+}
+
+\LMHash{}
 Evaluation of an unconditional ordinary method invocation $i$ of the form
 \code{$e$.$m$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
 proceeds as follows:
 
 \LMHash{}
 First, the expression $e$ is evaluated to a value $o$.
-Next, the argument part
-\code{<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
-is evaluated yielding actual type arguments
-$t_1, \ldots, t_r$
-and actual argument objects $o_1, \ldots, o_{n+k}$.
-Let $f$ be the result of looking up (\ref{methodLookup}) method $m$ in $o$ with respect to the current library $L$.
+Let $f$ be the result of looking up (\ref{lookup}) method $m$ in $o$ with respect to the current library $L$.
 
 \LMHash{}
-Let $X_1, \ldots, X_s$ be the formal type parameters of $f$,
-let $p_1, \ldots, p_h$ be the required parameters of $f$,
-let $p_1, \ldots, p_m$ be the positional parameters of $f$,
-and let $p_{h+1}, \ldots, p_{h+l}$ be the optional parameters declared by $f$.
-
-\commentary{
-We have an actual argument list consisting of $r$ type arguments, $n$ positional arguments, and $k$ named arguments.
-We have a function with $s$ type parameters, $h$ required parameters, and $l$ optional parameters.
-The number of type arguments must match the number of type parameters.
-The number of positional arguments must be at least as large as the number of required parameters, and no larger than the number of positional parameters.
-All named arguments must have a corresponding named parameter.
-A given named argument cannot be provided more than once.
-}
-
-% View on declaration:
-%
-%     |**   ...        *|**        ...         *|**     ...          *|
-%      <-s type par.s--> <--h required par.s---> <--l optional par.s->
-%                        <--m pos, par.s, h=m--> <---l named par.s---> NAMED
-%                        <----------m positional par.s, m=h+l--------> POS
-%
-% Actual argument part:
-%
-%     |**   ...        *|**           ...          *|**     ...       *|
-%      <-r type par.s--> <----n positional arg.s---> <--k named arg.s->
-\LMHash{}
-% Passing a wrong number of actual type arguments.
-If $r = 0$ and $s > 0$ then replace the actual type argument list:
-%% TODO[instantiate-to-bound]: The actual type arguments passed here
-%% should be chosen based on the instantiate-to-bound algorithm, but we
-%% cannot yet refer to that because it hasn't yet been specified here.
-let $r$ be $s$ and $t_i = \DYNAMIC{}$ for $i \in 1 .. s$.
-If $r \not= s$, the method lookup has failed.
-% Passing named arguments to a function with optional positional parameters.
-If $k > 0$ and $m \not= h$, the method lookup has failed.
-% Passing too few or too many positional arguments.
-If $n < h$, or $n > m$, the method lookup has failed.
-% When k>0, h=m and there are l named parameters p_{h+1} .. p_{h+l}.
-Furthermore, each
-$x_i, i \in n+1 .. n+k$, must have a corresponding named parameter in the set
-$\{p_{h+1}, \ldots, p_{h+l}\}$,
-or the method lookup also fails.
-
-\LMHash{}
-If $o$ is an instance of \code{Type} but $e$ is not a constant type literal,
+%% TODO(eernst): This is metaclass stuff, should be deleted.
+If method lookup succeeded,
+but $o$ is an instance of \code{Type} and $e$ is not a constant type literal,
 then if $m$ is a method that forwards (\ref{functionDeclarations}) to a static method,
-method lookup fails.
-Otherwise method lookup has succeeded.
+method lookup is considered to have failed.
 
 \LMHash{}
 If the method lookup succeeded,
-the body of $f$ is executed with respect to the bindings that resulted from the evaluation of the argument list,
+the binding of actual arguments to formal parameters is performed as specified in Section~\ref{bindingActualsToFormals}.
+The body of $f$ is then executed with respect to the bindings that resulted from the evaluation of the argument list,
 and with \THIS{} bound to $o$.
-The value of $i$ is the value returned after $f$ is executed.
+The value of $i$ is the value returned by the execution of $f$'s body.
 
 \LMHash{}
-If the method lookup has failed,
-then let $g$ be the result of looking up getter (\ref{getterAndSetterLookup}) $m$ in $o$ with respect to $L$.
-If $o$ is an instance of \code{Type} but $e$ is not a constant type literal,
-then if $g$ is a getter that forwards to a static getter, getter lookup fails.
-If the getter lookup succeeded,
-let $v_g$ be the value of the getter invocation $e.m$.
-Now repeat from finding $f$ above, this time with $o$ being $v_g$ and $m$ being \code{call}.
+If the method lookup failed,
+then let $g$ be the result of looking up getter (\ref{lookup}) $m$ in $o$ with respect to $L$.
+%% TODO(eernst): This is metaclass stuff, should be deleted.
+If getter lookup succeeded,
+but $o$ is an instance of \code{Type} and $e$ is not a constant type literal,
+then if $g$ is a getter that forwards to a static getter,
+getter lookup is considered to have failed.
+
+\LMHash{}
+If the getter lookup succeeded then invoke the getter $o.m$
+and let $v_g$ be the returned value.
+Then the value of $i$ is the value of
+
+\code{$v_g$<$A_1, \ldots,\ A_r$>($a_1,\ \ldots,\ a_n,\ x_{n+1}$: $a_{n+1},\ \ldots,\ x_{n+k}$: $a_{n+k}$)}.
 
 \LMHash{}
 If getter lookup has also failed,
 then a new instance $im$ of the predefined class \code{Invocation} is created, such that:
 \begin{itemize}
-\item \code{im.isMethod} evaluates to \code{\TRUE{}}.
-\item \code{im.memberName} evaluates to the symbol \code{m}.
-\item \code{im.positionalArguments} evaluates to an unmodifiable list with the same values as
-\code{<Object>[$o_1, \ldots, o_n$]}.
-\item \code{im.namedArguments} evaluates to an unmodifiable map with the same keys and values as
-\code{<Symbol, Object>\{$\#x_{n+1}$: $o_{n+1}, \ldots, \#x_{n+k}$: $o_{n+k}$\}}.
-\item \code{im.typeArguments} evaluates to an unmodifiable list with the same values as
-\code{<Type>[$t_1, \ldots, t_r$]}.
+\item \code{$im$.isMethod} evaluates to \code{\TRUE{}}.
+\item \code{$im$.memberName} evaluates to the symbol \code{m}.
+\item \code{$im$.positionalArguments} evaluates to an unmodifiable list
+  with the values resulting from the evaluation of
+  \code{<Object>[$a_1, \ldots,\ a_n$]}.
+\item \code{$im$.namedArguments} evaluates to an unmodifiable map
+  with the keys and values resulting from the evaluation of
+
+  \code{<Symbol, Object>\{$\#x_{n+1}$: $a_{n+1}, \ldots,\ \#x_{n+k}$: $a_{n+k}$\}}.
+\item \code{$im$.typeArguments} evaluates to an unmodifiable list
+  with the values resulting from the evaluation of
+  \code{<Type>[$A_1, \ldots,\ A_r$]}.
 \end{itemize}
 
 \LMHash{}
@@ -5861,47 +6302,18 @@
 and the result of this invocation is the result of evaluating $i$.
 
 \commentary{
+Notice that the wording avoids re-evaluating the receiver $o$ and the arguments $a_i$.
+Also note that there is no need to specify how to handle an invocation of \code{noSuchMethod}
+that fails because ``there is no such method'':
 It is not possible to override the \code{noSuchMethod} of class \code{Object}
 in such a way that it cannot be invoked with one argument of type \code{Invocation}.
-% .. leaving `noSuchMethod(covariant Null n) => n;` as an exercise for the reader.
+It can fail with a dynamic type error if the parameter type is overridden with a
+proper subtype of \code{Invocation},
+but that does not give rise to yet another invocation of \code{noSuchMethod}.
+% We might want to mention `noSuchMethod(covariant Null n) => n;`, but
+% `covariant` is not yet specified, and it is not a big problem to omit it.
 }
 
-\commentary{
-Notice that the wording carefully avoids re-evaluating the receiver $o$ and the arguments $a_i$.
-}
-
-\LMHash{}
-Let $T$ be the static type of $e$.
-It is a compile-time error if $T$ does not have an accessible (\ref{privacy}) instance member named $m$, unless either:
-\begin{itemize}
-\item $T$ is \code{Type}, $e$ is a constant type literal,
-and the class corresponding to $e$ has a static getter named $m$.
-Or
-\item $T$ is \FUNCTION{} and $m$ is \CALL.
-\rationale{
-This means that for invocations of an instance method named \code{call},
-a receiver of type \FUNCTION{} is treated like a receiver of type \DYNAMIC{}.
-The expectation is that any concrete subclass of \FUNCTION{} will implement \CALL,
-but there is no method signature which can be assumed for \CALL{} in \FUNCTION{}
-because every signature will conflict with some potential overriding declarations.
-}
-\end{itemize}
-
-\LMHash{}
-If $T.m$ exists, it is a compile-time error if the type $F$ of $T.m$ may not be assigned to a function type.
-If $T.m$ does not exist, or if $F$ is not a function type, the static type of $i$ is \DYNAMIC{}.
-Otherwise, let $X_1, \ldots, X_s$ be the formal type parameters of the type of $F$,
-and $T_0$ its declared return type.
-If $r \not= s$ the static type of $i$ is \DYNAMIC{};
-otherwise, the static type of $i$ is $[A_1/X_1, \ldots, A_r/X_s]T_0$.
-
-\commentary{
-That is, the declared return type where each formal type parameter has been replaced by the corresponding actual type argument.
-}
-
-\LMHash{}
-It is a compile-time error to invoke any of the methods of class \code{Object} on a prefix object (\ref{imports}) or on a constant type literal that is immediately followed by the token `.'\,.
-
 
 \subsubsection{Cascaded Invocations}
 \LMLabel{cascadedInvocations}
@@ -5948,12 +6360,6 @@
 \subsubsection{Super Invocation}
 \LMLabel{superInvocation}
 
-\commentary{
-Note that non-generic invocations arise as the special case where the number of type arguments is zero,
-in which case the type argument list is omitted,
-and similarly for formal type parameter lists (\ref{generics}).
-}
-
 % Conditional super invocation is meaningless: \THIS{} is not null.
 
 \LMHash{}
@@ -5961,101 +6367,12 @@
 
 \code{\SUPER{}.$m$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}.
 
-\LMHash{}
-Evaluation of $i$ proceeds as follows:
-
-\LMHash{}
-First, the argument part
-
-\code{<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
-
-\noindent
-is evaluated producing actual type arguments $t_1, \ldots, t_r$ and actual argument objects $o_1, \ldots, o_{n+k}$.
-Let $g$ be the method currently executing,
-and let $C$ be the class in which $g$ was looked up (\ref{methodLookup}).
-Let $S_{dynamic}$ be the superclass of $C$,
-and let $f$ be the result of looking up method (\ref{methodLookup}) $m$ in $S_{dynamic}$ with respect to the current library $L$.
-
-\LMHash{}
-Let $X_1, \ldots, X_s$ be the formal type parameters of $f$.
-Let $p_1, \ldots, p_h$ be the required parameters of $f$,
-let $p_1, \ldots, p_m$ be the positional parameters of $f$,
-and let $p_{h+1}, \ldots, p_{h+l}$ be the optional parameters declared by $f$.
-
 \commentary{
-We have an actual argument list consisting of $r$ type arguments, $n$ positional arguments, and $k$ named arguments.
-We have a function with $s$ type parameters, $h$ required parameters, and $l$ optional parameters.
-The number of type arguments must match the number of type parameters.
-The number of positional arguments must be at least as large as the number of required parameters, and no larger than the number of positional parameters.
-All named arguments must have a corresponding named parameter.
-A given named argument cannot be provided more than once.
+Note that non-generic invocations arise as the special case where the number of type arguments is zero,
+in which case the type argument list is omitted,
+and similarly for formal type parameter lists (\ref{generics}).
 }
 
-% View on declaration:
-%
-%     |**   ...        *|**        ...         *|**     ...          *|
-%      <-s type par.s--> <--h required par.s---> <--l optional par.s->
-%                        <--m pos, par.s, h=m--> <---l named par.s---> NAMED
-%                        <----------m positional par.s, m=h+l--------> POS
-%
-% Actual argument part:
-%
-%     |**   ...        *|**           ...          *|**     ...       *|
-%      <-r type par.s--> <----n positional arg.s---> <--k named arg.s->
-\LMHash{}
-% Passing a wrong number of actual type arguments.
-If $r \not= s$, the method lookup has failed.
-% Passing named arguments to a function with optional positional parameters.
-If $k > 0$ and $m \not= h$, the method lookup has failed.
-% Passing too few or too many positional arguments.
-If $n < h$, or $n > m$, the method lookup has failed.
-% When k>0, h=m and there are l named parameters p_{h+1} .. p_{h+l}.
-Furthermore, each
-$x_i, i \in n+1 .. n+k$, must have a corresponding named parameter in the set
-$\{p_{h+1}, \ldots, p_{h+l}\}$,
-or the method lookup also fails.
-Otherwise, method lookup has succeeded.
-
-\LMHash{}
-If the method lookup succeeded,
-the body of $f$ is executed with respect to the bindings that resulted from the evaluation of the argument list,
-and with \THIS{} bound to the current value of \THIS{}.
-The value of $i$ is the value returned after $f$ is executed.
-
-\LMHash{}
-If the method lookup has failed,
-then let $g$ be the result of looking up getter (\ref{getterAndSetterLookup}) $m$ in $S_{dynamic}$ with respect to $L$.
-If the getter lookup succeeded,
-let $v_g$ be the value of the getter invocation $\SUPER{}.m$.
-Now repeat from finding $f$ above, this time with $o$ being $v_g$ and $m$ being \code{call}.
-
-\LMHash{}
-If getter lookup has also failed,
-then a new instance $im$ of the predefined class \code{Invocation} is created, such that:
-\begin{itemize}
-\item \code{im.isMethod} evaluates to \code{\TRUE{}}.
-\item \code{im.memberName} evaluates to the symbol \code{m}.
-\item \code{im.positionalArguments} evaluates to an unmodifiable list with the same values as
-$\code{<Object>}[o_1, \ldots, o_n]$.
-\item \code{im.namedArguments} evaluates to an unmodifiable map with the same keys and values as
-$\code{<Symbol, Object>}\{\#x_{n+1}: o_{n+1}, \ldots, \#x_{n+k}: o_{n+k}\}$.
-\item \code{im.typeArguments} evaluates to an unmodifiable list with the same values as
-$\code{<Type>}[t_1, \ldots, t_r]$.
-\end{itemize}
-
-\LMHash{}
-Then the method \code{noSuchMethod()} is looked up in $S_{dynamic}$ and invoked on \THIS{} with argument $im$,
-and the result of this invocation is the result of evaluating $i$.
-
-% TODO(eernst): We have removed the description of how to invoke noSuchMethod
-% in Object if the overriding noSuchMethod does not accept one argument of
-% type Invocation, because that will be a compile-time error soon. At this
-% point we just keep a commentary ready to say that:
-%
-%% \commentary {
-%% It is a compile-time error to override the \code{noSuchMethod} of class \code{Object} in such a way that it cannot be invoked with one positional argument of type \code{Invocation}.
-%% }
-
 \LMHash{}
 It is a compile-time error if a super method invocation occurs in a top-level function or variable initializer,
 in an instance variable initializer or initializer list,
@@ -6063,24 +6380,70 @@
 in a factory constructor,
 or in a static method or variable initializer.
 
-\LMHash{}
-Let $S_{static}$ be the superclass of the immediately enclosing class.
-It is a compile-time error if $S_{static}$ does not have an accessible (\ref{privacy}) instance member named $m$.
+{ % Scope for superclass name.
+
+\def\SuperClass{\ensuremath{S_{\mbox{\scriptsize{}super}}}}
 
 \LMHash{}
-If $S_{static}.m$ exists, it is a compile-time error if the type $F$ of $S_{static}.m$ may not be assigned to a function type.
-If $S_{static}.m$ does not exist, or if $F$ is not a function type, the static type of $i$ is \DYNAMIC{};
-Otherwise, let $X_1, \ldots, X_s$ be the formal type parameters of the type of $F$,
-and $T_0$ its declared return type.
-If $r \not= s$ the static type of $i$ is \DYNAMIC{};
-otherwise, the static type of $i$ is $[A_1/X_1, \ldots, A_r/X_s]T_0$.
+Let \SuperClass{} be the superclass (\ref{superclasses})
+of the immediately enclosing class for $i$,
+and let $L$ be the library that contains $i$.
+Let the declaration $d$ be
+the result of looking up the method $m$ in \SuperClass{}
+with respect to $L$ (\ref{lookup}),
+and let $F$ be the static type of $d$.
+Otherwise, if the method lookup failed,
+let the declaration $d$ be the result of looking up
+the getter $m$ with respect to $L$ in \SuperClass{}
+(\ref{lookup}),
+and let $F$ be the return type of $d$.
+If both lookups failed, a compile-time error occurs.
+
+\LMHash{}
+Otherwise (\commentary{when one of the lookups succeeded}),
+the static analysis of $i$ is performed as specified in Section~\ref{bindingActualsToFormals},
+considering the function to have static type $F$,
+and the static type of $i$ is as specified there.
 
 \commentary{
-That is, the declared return type where each formal type parameter has been replaced by the corresponding actual type argument.
+Note that member lookups ignore abstract declarations,
+which means that there will be a compile-time error if the targeted member $m$ is abstract,
+as well as when it does not exist at all.
 }
 
-% The following is not needed because it is specified in 'Binding Actuals to Formals"
-%Let $T_i$ be the static type of $a_i, i \in 1 .. n+k$. It is a compile-time error if $F$ is not a supertype of $(T_1, \ldots, t_n, \{T_{n+1}\ x_{n+1}, \ldots, T_{n+k}\ x_{n+k}\}) \to \bot$.
+\LMHash{}
+Evaluation of $i$ proceeds as follows:
+Let $o$ be the current binding of \THIS{},
+let $C$ be the enclosing class for $i$,
+and let \SuperClass{} be the superclass (\ref{superclasses}) of $C$.
+Let the declaration $d$ be the result of looking up
+the method $m$ with respect to $L$ in $o$ starting with \SuperClass{}
+(\ref{lookup}).
+If the lookup succeeded,
+let $f$ denote the function associated with $d$.
+%
+Otherwise (\commentary{when method lookup failed}),
+let the declaration $d$ be the result of looking up
+the getter $m$ with respect to $L$ in $o$ starting with \SuperClass{}
+(\ref{lookup}).
+If the getter lookup succeeded,
+invoke said getter with \THIS{} bound to $o$,
+and let $f$ denote the returned object.
+
+\commentary{
+If both lookups failed, the exact same lookups would have failed
+at compile-time, and the program then has a compile-time error.
+}
+
+\LMHash{}
+Otherwise perform the binding of actual arguments to formal parameters for
+\code{$f$<$A_1, \ldots,\ A_r$>($a_1, \ldots,\ a_n,\ x_{n+1}$: $a_{n+1}, \ldots,\ x_{n+k}$: $a_{n+k}$)}
+as specified in Section~\ref{bindingActualsToFormals},
+and execute the body of $f$ with said bindings
+plus a binding of \THIS{} to $o$.
+The result returned by $f$ is then the result of evaluating $i$.
+
+} % End of scope for superclass name.
 
 
 \subsubsection{Sending Messages}
@@ -6111,7 +6474,7 @@
 \end{enumerate}
 
 \commentary{
-Function objects derived via closurization are colloquially known as tear-offs.
+Function objects derived from members via closurization are colloquially known as tear-offs.
 }
 
 Property extraction can be either {\em conditional} or {\em unconditional}.
@@ -6146,7 +6509,8 @@
 
 \LMHash{}
 First, the expression $e$ is evaluated to an object $o$.
-Let $f$ be the result of looking up (\ref{methodLookup}) method (\ref{instanceMethods}) $m$ in $o$ with respect to the current library $L$.
+Let $f$ be the result of looking up (\ref{lookup}) method (\ref{instanceMethods}) $m$ in $o$ with respect to the current library $L$.
+%% TODO(eernst): This is metaclass stuff, should be deleted.
 If $o$ is an instance of \code{Type} but $e$ is not a constant type literal, then if $f$ is a method that forwards (\ref{functionDeclarations}) to a static method, method lookup fails.
 If method lookup succeeds then $i$ evaluates to the closurization of method $f$ on object $o$ (\ref{ordinaryMemberClosurization}).
 
@@ -6159,22 +6523,23 @@
 
 \LMHash{}
 Otherwise, $i$ is a getter invocation.
-Let $f$ be the result of looking up (\ref{getterAndSetterLookup}) getter (\ref{getters}) $m$ in $o$ with respect to $L$.
+Let $f$ be the result of looking up (\ref{lookup}) getter (\ref{getters}) $m$ in $o$ with respect to $L$.
+%% TODO(eernst): This is metaclass stuff, should be deleted.
 If $o$ is an instance of \code{Type} but $e$ is not a constant type literal, then if $f$ is a getter that forwards to a static getter, getter lookup fails.
 Otherwise, the body of $f$ is executed with \THIS{} bound to $o$.
 The value of $i$ is the result returned by the call to the getter function.
 
 \LMHash{}
-If the getter lookup has failed, then a new instance $im$ of the predefined class \code{Invocation} is created, such that :
+If the getter lookup has failed, then a new instance $im$ of the predefined class \code{Invocation} is created, such that:
 \begin{itemize}
-\item \code{im.isGetter} evaluates to \code{\TRUE{}}.
-\item \code{im.memberName} evaluates to the symbol \code{m}.
-\item \code{im.positionalArguments} evaluates to an empty, unmodifiable instance of
+\item \code{$im$.isGetter} evaluates to \code{\TRUE{}}.
+\item \code{$im$.memberName} evaluates to the symbol \code{m}.
+\item \code{$im$.positionalArguments} evaluates to an empty, unmodifiable instance of
 \code{List<Object>}.
-\item \code{im.namedArguments} evaluates to an empty, unmodifiable instance of
+\item \code{$im$.namedArguments} evaluates to an empty, unmodifiable instance of
 
 \code{Map<Symbol, Object>}.
-\item \code{im.typeArguments} evaluates to an empty, unmodifiable instance of
+\item \code{$im$.typeArguments} evaluates to an empty, unmodifiable instance of
 
 \code{List<Type>}.
 \end{itemize}
@@ -6202,6 +6567,7 @@
 \LMHash{}
 Let $T$ be the static type of $e$.
 It is a compile-time error if $T$ does not have a method or getter named $m$,
+%% TODO(eernst): This is metaclass stuff, should be deleted.
 unless $T$ is \code{Type},
 $e$ is a constant type literal,
 and the class corresponding to $e$ has a static method or getter named $m$.
@@ -6209,10 +6575,18 @@
 \LMHash{}
 The static type of $i$ is:
 \begin{itemize}
-\item The declared return type of $T.m$, if $T$ has an accessible instance getter named $m$.
-\item The declared return type of $m$, if $T$ is \code{Type}, $e$ is a constant type literal and the class corresponding to $e$ declares an accessible static getter named $m$.
-\item The static type of function $T.m$ if $T$ has an accessible instance method named $m$.
-\item The static type of function $m$, if $T$ is \code{Type}, $e$ is a constant type literal and the class corresponding to $e$ declares an accessible static method named $m$.
+\item The declared return type of \code{$T$.$m$}, if $T$ has an accessible instance getter named $m$.
+\item
+%% TODO(eernst): This is metaclass stuff, should be deleted.
+The declared return type of $m$, if $T$ is \code{Type},
+$e$ is a constant type literal
+and the class corresponding to $e$ declares an accessible static getter named $m$.
+\item The static type of function \code{$T$.$m$} if $T$ has an accessible instance method named $m$.
+\item
+%% TODO(eernst): This is metaclass stuff, should be deleted.
+The static type of function $m$, if $T$ is \code{Type},
+$e$ is a constant type literal
+and the class corresponding to $e$ declares an accessible static method named $m$.
 \item The type \DYNAMIC{} otherwise.
 \end{itemize}
 
@@ -6238,14 +6612,14 @@
 \LMHash{}
 If the getter lookup has failed, then a new instance $im$ of the predefined class \code{Invocation} is created, such that:
 \begin{itemize}
-\item \code{im.isGetter} evaluates to \code{\TRUE{}}.
-\item \code{im.memberName} evaluates to the symbol \code{m}.
-\item \code{im.positionalArguments} evaluates to an empty, unmodifiable instance of
+\item \code{$im$.isGetter} evaluates to \code{\TRUE{}}.
+\item \code{$im$.memberName} evaluates to the symbol \code{m}.
+\item \code{$im$.positionalArguments} evaluates to an empty, unmodifiable instance of
 \code{List<Object>}.
-\item \code{im.namedArguments} evaluates to an empty, unmodifiable instance of
+\item \code{$im$.namedArguments} evaluates to an empty, unmodifiable instance of
 
 \code{Map<Symbol, Object>}.
-\item \code{im.typeArguments} evaluates to an empty, unmodifiable instance of
+\item \code{$im$.typeArguments} evaluates to an empty, unmodifiable instance of
 
 \code{List<Type>}.
 \end{itemize}
@@ -6294,8 +6668,8 @@
 \begin{itemize}
 %\item $(a) \{\RETURN{}$ $u$ $op$ $a;$\} if $f$ is named $op$ and $op$ is one of \code{<, >, <=, >=, ==, -, +, /, \~{}/, *, \%, $|$, \^{}, \&, $<<$, $>>$} (this precludes closurization of unary -).
 %\item $() \{\RETURN{}$ \~{} $u;$\} if $f$ is named \~{}.
-%\item $(a) \{\RETURN{}$ $u[a];$\} if $f$ is named $[]$.
-%\item $(a, b) \{\RETURN{}$ $u[a] = b;$\} if $f$ is named $[]=$.
+%\item $(a) \{\RETURN{}$ $u[a];$\} if $f$ is named \code{[]}.
+%\item $(a, b) \{\RETURN{}$ $u[a] = b;$\} if $f$ is named \code{[]=}.
 \item
 \begin{dartCode}
 <$X_1\ \EXTENDS\ B'_1, \ldots,\ X_s\ \EXTENDS\ B'_s$>
@@ -6374,7 +6748,10 @@
 obtained by closurization of $m$ on $o_1$ respectively $o_2$.
 Then \code{$c_1$ == $c_2$} evaluates to true if and only if $o_1$ and $o_2$ is the same object.
 
-%\item The static type of the property extraction is the static type of function $T.m$, where $T$ is the static type of $e$, if $T.m$ is defined. Otherwise the static type of $e.m$ is \DYNAMIC{}.
+%% TODO(eernst): This being a comment, it's presumably spelled out somewhere
+%% else. Find it and check that it does actually say that it is an error
+%% except when the type of $e$ is \DYNAMIC{}.
+%\item The static type of the property extraction is the static type of function \code{$T$.$m$}, where $T$ is the static type of $e$, if \code{$T$.$m$} is defined. Otherwise the static type of $e.m$ is \DYNAMIC{}.
 
 \commentary{
 % Spell out the consequences for `==` and for `identical`, for the receivers
@@ -6408,7 +6785,7 @@
 and there is no class $U$ which is a subclass of $S$ and a superclass of $T$ which implements $f$.
 
 \commentary{
-In short, consider a situation where a superinvocation of $f$ will execute $f$ as declared in $S$.
+In short, consider a situation where a super invocation of $f$ will execute $f$ as declared in $S$.
 }
 
 \LMHash{}
@@ -6422,8 +6799,8 @@
 \begin{itemize}
 %\item $(a) \{\RETURN{}$ \SUPER{} $op$ $a;$\} if $f$ is named $op$ and $op$ is one of \code{<, >, <=, >=, ==, -, +, /, \~{}/, *, \%, $|$, \^{}, \&, $<<$, $>>$}.
 %\item $() \{\RETURN{}$ \~{}\SUPER;\} if $f$ is named \~{}.
-%\item $(a) \{\RETURN{}$ $\SUPER[a];$\} if $f$ is named $[]$.
-%\item $(a, b) \{\RETURN{}$ $\SUPER[a] = b;$\} if $f$ is named $[]=$.
+%\item $(a) \{\RETURN{}$ $\SUPER[a];$\} if $f$ is named \code{[]}.
+%\item $(a, b) \{\RETURN{}$ $\SUPER[a] = b;$\} if $f$ is named \code{[]=}.
 \item
 \begin{dartCode}
 <$X_1\ \EXTENDS\ B'_1, \ldots,\ X_s\ \EXTENDS\ B'_s$>
@@ -6516,56 +6893,80 @@
 \end{grammar}
 
 \LMHash{}
-Evaluation of an assignment $a$ of the form $v$ \code{=} $e$ proceeds as follows:
-
-%If there is neither a local variable declaration with name $v$ nor a setter declaration with name $v=$ in the lexical scope enclosing $a$, then:
-%\begin{itemize}
-% \item If $a$ occurs inside a top level or static function (be it function, method, getter, or setter) or variable initializer, evaluation of $a$ causes $e$ to be evaluated, after which a \code{NoSuchMethodError} is thrown.
-% \item Otherwise, the assignment is equivalent to the assignment \code{\THIS{}.$v$ = $e$}.
-% \end{itemize}
-
-%Otherwise
+\Case{\code{$v$ = $e$}}
+Consider an assignment $a$ of the form \code{$v$ = $e$},
+where $v$ is an identifier or an identifier qualified by an import prefix,
+and $v$ denotes a variable (\ref{variables}) or \code{$v$=} denotes a setter
+(\commentary{which may be declared explicitly or induced by an instance variable, etc}).
+Let $T$ be the static type of $v$ when $v$ denotes a variable,
+otherwise let $T$ be the static type of the formal parameter of the setter \code{$v$=}.
+It is a compile-time error if the static type of $e$ may not be assigned to $T$.
+The static type of $a$ is the static type of $e$.
 
 \LMHash{}
-Let $d$ be the innermost declaration whose name is $v$ or $v=$, if it exists.
-It is a compile-time error if $d$ denotes a prefix object.
+It is a compile-time error if an assignment of the form \code{$v$ = $e$} occurs
+inside a top level or static function (be it function, method, getter, or setter) or variable initializer,
+and there is neither a mutable local variable declaration with name $v$
+nor a setter declaration with name \code{$v$=} in the lexical scope enclosing the assignment.
+
+\LMHash{}
+Evaluation of an assignment $a$ of the form \code{$v$ = $e$}
+proceeds as follows:
+%% TODO(eernst): $d$ is defined ambiguously: both getter & setter may exist.
+Let $d$ be the innermost declaration whose name is $v$ or \code{$v$=}, if it exists.
+It is a compile-time error if $d$ denotes
+a prefix object, type declaration, or function declaration.
 
 \LMHash{}
 If $d$ is the declaration of a local variable, the expression $e$ is evaluated to an object $o$.
-Then, the variable $v$ is bound to $o$ unless $v$ is \FINAL{} or \CONST{}, in which case a dynamic error occurs.
+Then, the variable $v$ is bound to $o$.
 If no error occurs, the value of the assignment expression is $o$.
 
+\commentary{
+If $v$ is a final variable, a compile-time error has occurred,
+but a type check may cause a dynamic error.
+}
+
 % add local functions per bug 23218
 
 \LMHash{}
+% TODO(eernst): $d$ defined ambiguously, re-check next sentence when fixing.
 If $d$ is the declaration of a library variable, top level getter or top level setter, the expression $e$ is evaluated to an object $o$.
-Then the setter $v=$ is invoked with its formal parameter bound to $o$.
+% TODO(eernst): $d$ defined ambiguously, re-check when fixing: Case $d$ is the getter and there is no setter.
+Then the setter \code{$v$=} is invoked with its formal parameter bound to $o$.
 The value of the assignment expression is $o$.
 
 \LMHash{}
-Otherwise, if $d$ is the declaration of a static variable, static getter or static setter in class $C$, then the assignment is equivalent to the assignment \code{$C.v$ = $e$}.
+Otherwise, if $d$ is the declaration of a class variable, static getter or static setter in class $C$,
+then the assignment is equivalent to the assignment \code{$C$.$v$ = $e$}.
+
+\commentary{
+Otherwise, if $a$ occurs inside a top level or static function
+(be it function, method, getter, or setter) or variable initializer,
+a compile-time error has occurred.
+}
 
 \LMHash{}
-Otherwise, If $a$ occurs inside a top level or static function (be it function, method, getter, or setter) or variable initializer, evaluation of $a$ causes $e$ to be evaluated, after which a \code{NoSuchMethodError} is thrown.
-
-\LMHash{}
+%% TODO(eernst): We don't want to transform code and than complain, see if this
+%% can be reworded to rely on static checks such that it only happens when it
+%% works, or maybe that's already true.
 Otherwise, the assignment is equivalent to the assignment \code{\THIS{}.$v$ = $e$}.
 
 \LMHash{}
-In checked mode, it is a dynamic type error if $o$ is not the null object (\ref{null}) and the interface of the class of $o$ is not a subtype of the actual type (\ref{actualTypeOfADeclaration}) of $v$.
+In checked mode, it is a dynamic type error if $o$ is not the null object (\ref{null})
+and the interface of the class of $o$ is not a subtype of the actual type (\ref{actualTypeOfADeclaration}) of $v$.
 
 \LMHash{}
-It is a compile-time error if the static type of $e$ may not be assigned to the static type of $v$.
-The static type of the expression $v$ \code{=} $e$ is the static type of $e$.
+\Case{\code{$e_1$?.$v$ = $e_2$}}
+Consider an assignment $a$ of the form \code{$e_1$?.$v$ = $e_2$}.
+Let $S$ be the static type of the formal parameter of the setter \code{$v$=}.
+It is a compile-time error if the static type of $e_2$ may not be assigned to $S$.
+The static type of $a$ is the static type of $e_2$.
 
 \LMHash{}
 Evaluation of an assignment $a$ of the form \code{$e_1$?.$v$ = $e_2$}
 proceeds as follows:
-
-\LMHash
 If $e_1$ is a type literal, $a$ is equivalent to \code{$e_1$.$v$ = $e_2$}.
-
-\LMHash{}
 Otherwise evaluate $e_1$ to an object $o$.
 If $o$ is the null object, $a$ evaluates to the null object (\ref{null}).
 Otherwise let $x$ be a fresh variable bound to $o$
@@ -6573,35 +6974,37 @@
 Then $a$ evaluates to $r$.
 
 \LMHash{}
+\Case{\code{$e_1$.$v$ = $e_2$}}
+Consider an assignment $a$ of the form \code{$e_1$.$v$ = $e_2$}.
+Let $S$ be the static type of the formal parameter of the setter \code{$v$=}.
+It is a compile-time error if the static type of $e_2$ may not be assigned to $S$.
 The static type of $a$ is the static type of $e_2$.
-Let $T$ be the static type of $e_1$ and let $y$ be a fresh variable of type $T$.
-Exactly the same compile-time errors that would be caused by \code{$y$.$v$ = $e_2$} are also generated in the case of \code{$e_1$?.$v$ = $e_2$}.
 
 \LMHash{}
-Evaluation of an assignment of the form \code{$e_1$.$v$ = $e_2$} proceeds as follows:
-
-\LMHash{}
+Evaluation of an assignment of the form \code{$e_1$.$v$ = $e_2$}
+proceeds as follows:
 The expression $e_1$ is evaluated to an object $o_1$.
 Then, the expression $e_2$ is evaluated to an object $o_2$.
-Then, the setter $v=$ is looked up (\ref{getterAndSetterLookup}) in $o_1$ with respect to the current library.
+Then, the setter \code{$v$=} is looked up (\ref{lookup}) in $o_1$ with respect to the current library.
+%% TODO(eernst): This is metaclass stuff, should be deleted.
 If $o_1$ is an instance of \code{Type} but $e_1$ is not a constant type literal,
-then if $v=$ is a setter that forwards (\ref{functionDeclarations}) to a static setter, setter lookup fails.
-Otherwise, the body of $v=$ is executed with its formal parameter bound to $o_2$ and \THIS{} bound to $o_1$.
+then if \code{$v$=} is a setter that forwards (\ref{functionDeclarations}) to a static setter, setter lookup fails.
+Otherwise, the body of \code{$v$=} is executed with its formal parameter bound to $o_2$ and \THIS{} bound to $o_1$.
 
 \LMHash{}
 If the setter lookup has failed, then a new instance $im$ of the predefined class \code{Invocation} is created, such that:
 \begin{itemize}
-\item \code{im.isSetter} evaluates to \code{\TRUE{}}.
-\item \code{im.memberName} evaluates to the symbol \code{v=}.
-\item \code{im.positionalArguments} evaluates to an unmodifiable list with the same values as
+\item \code{$im$.isSetter} evaluates to \code{\TRUE{}}.
+\item \code{$im$.memberName} evaluates to the symbol \code{v=}.
+\item \code{$im$.positionalArguments} evaluates to an unmodifiable list with the same values as
 $\code{<Object>}[o_2]$.
-\item \code{im.namedArguments} evaluates to an empty, unmodifiable instance of
+\item \code{$im$.namedArguments} evaluates to an empty, unmodifiable instance of
 
 \code{Map<Symbol, Object>}.
-\item \code{im.typeArguments} evaluates to an empty, unmodifiable instance of
+\item \code{$im$.typeArguments} evaluates to an empty, unmodifiable instance of
 
 \code{List<Type>}.
-m\end{itemize}
+\end{itemize}
 
 \LMHash{}
 Then the method \code{noSuchMethod()} is looked up in $o_1$ and invoked with argument $im$.
@@ -6623,30 +7026,40 @@
 
 \LMHash{}
 Let $T$ be the static type of $e_1$.
-It is a compile-time error if $T$ does not have an accessible instance setter named $v=$ unless $T$ is \code{Type}, $e_1$ is a constant type literal and the class corresponding to $e_1$ has a static setter named $v=$.
+It is a compile-time error if $T$ does not have an accessible instance setter named \code{$v$=}
+%% TODO(eernst): This is metaclass stuff, should be deleted.
+unless $T$ is \code{Type}, $e_1$ is a constant type literal and the class corresponding to $e_1$ has a static setter named \code{$v$=}.
 
 \LMHash{}
-It is a compile-time error if the static type of $e_2$ may not be assigned to the static type of the formal parameter of the setter $v=$.
-The static type of the expression $e_1.v$ \code{=} $e_2$ is the static type of $e_2$.
+\Case{\code{\SUPER.$v$ = $e$}}
+Consider an assignment $a$ of the form \code{\SUPER.$v$ = $e$}.
+Let $S_{static}$ be the superclass of the immediately enclosing class.
+It is a compile-time error if $S_{static}$ does not have an accessible instance setter named \code{$v$=}.
+Otherwise, it is a compile-time error if the static type of $e$ may not be assigned to the static type of the formal parameter of the setter \code{$v$=}.
+The static type of $a$ is the static type of $e$.
 
 \LMHash{}
-Evaluation of an assignment of the form $\SUPER.v$ \code{=} $e$ proceeds as follows:
-
-\LMHash{}
-Let $g$ be the method currently executing, and let $C$ be the class in which $g$ was looked up.
+Evaluation of an assignment of the form \code{\SUPER.$v$ = $e$}
+proceeds as follows:
+Let $g$ be the currently executing method, and let $C$ be the class in which $g$ was looked up.
 Let $S_{dynamic}$ be the superclass of $C$.
 The expression $e$ is evaluated to an object $o$.
-Then, the setter $v=$ is looked up (\ref{getterAndSetterLookup}) in $S_{dynamic}$ with respect to the current library.
-The body of $v=$ is executed with its formal parameter bound to $o$ and \THIS{} bound to \THIS{}.
+Then, the setter \code{$v$=} is looked up (\ref{lookup}) in $S_{dynamic}$ with respect to the current library.
+The body of \code{$v$=} is executed with its formal parameter bound to $o$
+and \THIS{} bound to the current value of \THIS{}.
 
 \LMHash{}
 If the setter lookup has failed, then a new instance $im$ of the predefined class \code{Invocation} is created, such that:
 \begin{itemize}
-\item \code{im.isSetter} evaluates to \code{\TRUE{}}.
-\item \code{im.memberName} evaluates to the symbol \code{v=}.
-\item \code{im.positionalArguments} evaluates to an unmodifiable list with the same values as \code{[$o$]}.
-\item \code{im.namedArguments} evaluates to an empty unmodifiable instance of \code{Map<Symbol, Object>}.
-\item \code{im.typeArguments} evaluates to an empty, unmodifiable instance of
+\item \code{$im$.isSetter} evaluates to \code{\TRUE{}}.
+\item \code{$im$.memberName} evaluates to the symbol \code{v=}.
+\item \code{$im$.positionalArguments} evaluates to an unmodifiable list
+with the same values as \code{<Object>[$o$]}.
+\item \code{$im$.namedArguments} evaluates to an empty unmodifiable instance of
+
+\code{Map<Symbol, Object>}.
+\item \code{$im$.typeArguments} evaluates to an empty, unmodifiable instance of
+
 \code{List<Type>}.
 \end{itemize}
 
@@ -6657,73 +7070,93 @@
 The value of the assignment expression is $o$ irrespective of whether setter lookup has failed or succeeded.
 
 \LMHash{}
-In checked mode, it is a dynamic type error if $o$ is not the null object (\ref{null}) and the interface of the class of $o$ is not a subtype of the actual type of $S.v$.
+In checked mode, it is a dynamic type error if $o$ is not the null object (\ref{null})
+and the interface of the class of $o$ is not a subtype of the actual type of $S.v$.
 
 \LMHash{}
-Let $S_{static}$ be the superclass of the immediately enclosing class.
-It is a compile-time error if $S_{static}$ does not have an accessible instance setter named $v=$ unless $S_{static}$.
+\Case{\code{$e_1$[$e_2$] = $e_3$}}
+Consider an assignment $a$ of the form \code{$e_1$[$e_2$] = $e_3$}.
+It is a compile-time error if the static type of $e_1$ does not have a method named \code{[]=}.
+Otherwise, let $S_2$ be the static type of the first formal parameter of the method \code{[]=}
+and $S_3$ the static type of the second.
+It is a compile-time error if the static type of $e_2$ may not be assigned to $S_2$,
+and if the static type of $e_3$ may not be assigned to $S_3$.
+The static type of $a$ is the static type of $e_3$.
 
 \LMHash{}
-It is a compile-time error if the static type of $e$ may not be assigned to the static type of the formal parameter of the setter $v=$.
-The static type of the expression $\SUPER.v$ \code{=} $e$ is the static type of $e$.
-
-\LMHash{}
-Evaluation of an assignment $e$ of the form \code{$e_1$[$e_2$] = $e_3$}
+Evaluation of an assignment $a$ of the form \code{$e_1$[$e_2$] = $e_3$}
 proceeds as follows:
-
-\LMHash{}
 Evaluate $e_1$ to an object $a$, then evaluate $e_2$ to an object $i$, and finally evaluate $e_3$ to an object $v$.
 Call the method \code{[]=} on $a$ with $i$ as first argument and $v$ as second argument.
-Then $e$ evaluates to $v$.
+Then $a$ evaluates to $v$.
+% Should we add: It is a dynamic error if $e_1$ evaluates to a constant list or map?
 
 \LMHash{}
-The static type of the expression \code{$e_1$[$e_2$] = $e_3$} is the static type of $e_3$.
+\Case{\code{\SUPER[$e_1$] = $e_2$}}
+Consider an assignment $a$ of the form \code{\SUPER[$e_1$] = $e_2$}.
+Let $S_{static}$ be the superclass of the immediately enclosing class.
+It is a compile-time error if $S_{static}$ does not have a method \code{[]=}.
+Otherwise, let $S_1$ be the static type of the first formal parameter of the method \code{[]=}
+and $S_2$ the static type of the second.
+It is a compile-time error if the static type of $e_1$ may not be assigned to $S_1$,
+and if the static type of $e_2$ may not be assigned to $S_2$.
+The static type of $a$ is the static type of $e_2$.
 
 \LMHash{}
-An assignment of the form \code{\SUPER[$e_1$] = $e_2$} is equivalent to the expression \code{\SUPER.[$e_1$] = $e_2$}.
-The static type of the expression \code{\SUPER[$e_1$] = $e_2$} is the static type of $e_2$.
+For evaluation, an assignment of the form \code{\SUPER[$e_1$] = $e_2$}
+is equivalent to the expression \code{\SUPER.[$e_1$] = $e_2$}.
 
-% Should we add: It is a dynamic error if $e_1$ evaluates to an constant list or map.
-
-\LMHash{}
-It is a compile-time error if an assignment of the form $v = e$ occurs inside a top level or static function (be it function, method, getter, or setter) or variable initializer,
-and there is neither a local variable (\commentary{which includes formal parameters}) with name $v$
-nor a setter declaration with name $v=$ in the lexical scope enclosing the assignment.
-
-\LMHash{}
-It is a compile-time error to invoke any of the setters of class \code{Object} on a prefix object (\ref{imports}) or on a constant type literal that is immediately followed by the token `.'.
 
 \subsubsection{Compound Assignment}
 \LMLabel{compoundAssignment}
 
 \LMHash{}
-Evaluation of a compound assignment $a$ of the form \code{$v$ ??= $e$}
-proceeds as follows:
+\Case{\code{$v$ ??= $e$}}
+Consider a compound assignment $a$ of the form \code{$v$ ??= $e$}
+where $v$ is an identifier or an identifier qualified by an import prefix,
+such that $v$ denotes a variable or $v$ denotes a getter, and \code{$v$=} denotes a setter.
+Exactly the same compile-time errors that would be caused by \code{$v$ = $e$} are also generated in the case of $a$.
+%% TODO(eernst): We should mention other cases, e.g., `v=` denotes a setter, but there is no getter.
+The static type of $a$ is the least upper bound of the static type of $v$ and the static type of $e$.
 
 \LMHash{}
+Evaluation of a compound assignment $a$ of the form \code{$v$ ??= $e$}
+proceeds as follows:
 Evaluate $v$ to an object $o$.
 If $o$ is not the null object (\ref{null}), $a$ evaluates to $o$.
 Otherwise evaluate \code{$v$ = $e$} to a value $r$,
 and then $a$ evaluates to $r$.
 
 \LMHash{}
-Evaluation of a compound assignment, $a$ of the form \code{$C$.$v$ ??= $e$}, where $C$ is a type literal, proceeds as follow:
+\Case{\code{$C$.$v$ ??= $e$}}
+Consider a compound assignment $a$ of the form \code{$C$.$v$ ??= $e$}
+where $C$ is a type literal
+that may or may not be qualified by an import prefix,
+such that \code{$C$.$v$} denotes a getter and \code{$C$.$v$=} denotes a setter.
+Exactly the same compile-time errors that would be caused by \code{$C$.$v$ = $e$} are also generated in the case of $a$.
+%% TODO(eernst): We should mention other cases, e.g., `C.v=` denotes a setter, but there is no getter.
+The static type of $a$ is the least upper bound of the static type of \code{$C$.$v$} and the static type of $e$.
 
 \LMHash{}
+Evaluation of a compound assignment $a$ of the form \code{$C$.$v$ ??= $e$}
+where $C$ is a type literal proceeds as follow:
 Evaluate \code{$C$.$v$} to an object $o$.
 If $o$ is not the null object (\ref{null}), $a$ evaluates to $o$.
 Otherwise evaluate \code{$C$.$v$ = $e$} to a value $r$,
 and then $a$ evaluates to $r$.
 
-\commentary{
-The two rules above also apply when the variable v or the type C is prefixed.
-}
+\LMHash{}
+\Case{\code{$e_1$.$v$ ??= $e_2$}}
+Consider a compound assignment $a$ of the form \code{$e_1$.$v$ ??= $e_2$}.
+Let $T$ be the static type of $e_1$ and let $x$ be a fresh variable of type $T$.
+Except for errors inside $e_1$ and references to the name $x$,
+exactly the same compile-time errors that would be caused by \code{$x$.$v$ = $e_2$} are also generated in the case of $a$.
+%% TODO(eernst): Also, we should mention other cases, e.g., there is no getter `z.v`.
+The static type of $a$ is the least upper bound of the static type of \code{$e_1$.$v$} and the static type of $e_2$.
 
 \LMHash{}
 Evaluation of a compound assignment $a$ of the form \code{$e_1$.$v$ ??= $e_2$}
 proceeds as follows:
-
-\LMHash{}
 Evaluate $e_1$ to an object $u$.
 Let $x$ be a fresh variable bound to $u$.
 Evaluate \code{$x$.$v$} to an object $o$.
@@ -6732,10 +7165,15 @@
 and then $a$ evaluates to $r$.
 
 \LMHash{}
-Evaluation of a compound assignment $a$ of the form \code{$e_1$[$e_2$] ??= $e_3$}
-proceeds as follows:
+\Case{\code{$e_1$[$e_2$] ??= $e_3$}}
+Consider a compound assignment $a$ of the form \code{$e_1$[$e_2$] ??= $e_3$}.
+Exactly the same compile-time errors that would be caused by \code{$e_1$[$e_2$] = $e_3$} are also generated in the case of $a$.
+%% TODO(eernst): We should mention other cases, e.g., there is no `operator []`.
+The static type of $a$ is the least upper bound of the static type of \code{$e_1$[$e_2$]} and the static type of $e_3$.
 
 \LMHash{}
+Evaluation of a compound assignment $a$ of the form \code{$e_1$[$e_2$] ??= $e_3$}
+proceeds as follows:
 Evaluate $e_1$ to an object $u$ and then evaluate $e_2$ to an object $i$.
 Call the \code{[]} method on $u$ with argument $i$, and let $o$ be the returned value.
 If $o$ is not the null object (\ref{null}), $a$ evaluates to $o$.
@@ -6744,73 +7182,102 @@
 Then $a$ evaluates to $v$.
 
 \LMHash{}
-Evaluation of a compound assignment $a$ of the form \code{\SUPER.$v$ ??= $e$}
-proceeds as follows:
+\Case{\code{\SUPER.$v$ ??= $e$}}
+Consider a compound assignment $a$ of the form \code{\SUPER.$v$ ??= $e$}.
+Exactly the same compile-time errors that would be caused by \code{\SUPER.$v$ = $e$} are also generated in the case of $a$.
+%% TODO(eernst): We should mention other cases, e.g., there is no getter `\SUPER.v`.
+The static type of $a$ is the least upper bound of the static type of \code{\SUPER.$v$} and the static type of $e$.
 
 \LMHash{}
+Evaluation of a compound assignment $a$ of the form \code{\SUPER.$v$ ??= $e$}
+proceeds as follows:
 Evaluate \code{\SUPER.$v$} to an object $o$.
 If $o$ is not the null object (\ref{null}) then $a$ evaluates to $o$.
 Otherwise evaluate \code{\SUPER.$v$ = $e$} to an object $r$,
 and then $a$ evaluates to $r$.
 
 \LMHash{}
-Evaluation of a compound assignment $a$ of the form \code{$e_1$?.$v$ ??= $e_2$}
-proceeds as follows:
+\Case{\code{$e_1$?.$v$ ??= $e_2$}}
+Consider a compound assignment $a$ of the form \code{$e_1$?.$v$ ??= $e_2$}.
+Exactly the same compile-time errors that would be caused by \code{$e_1$.$v$ ??= $e_2$} are also generated in the case of $a$.
+% Note: We use the static type of \code{$e_1$?.$v$} rather than \code{$e_1$.$v$} even
+% though the latter would be simpler. This is because the former will remain correct
+% if NNBD is introduced, and because it reduces the amount of synthetic syntax.
+The static type of $a$ is the least upper bound of the static type of \code{$e_1$?.$v$} and the static type of $e_2$.
 
 \LMHash{}
-Evaluate $e_1$ to an object $u$ and let $x$ be a fresh variable bound to $u$.
+Evaluation of a compound assignment $a$ of the form \code{$e_1$?.$v$ ??= $e_2$}
+proceeds as follows:
+Evaluate $e_1$ to an object $u$.
+If $u$ is the null object (\ref{null}) then $a$ evaluates to the null object.
+Otherwise, let $x$ be a fresh variable bound to $u$.
 Evaluate \code{$x$.$v$} to an object $o$.
 If $o$ is not the null object (\ref{null}) then $a$ evaluates to $o$.
 Otherwise evaluate \code{$x$.$v$ = $e_2$} to an object $r$,
 and then $a$ evaluates to $r$.
 
-% But what about C?.v ??= e
+\LMHash{}
+\Case{\code{$C$?.$v$ ??= $e_2$}}
+A compound assignment of the form \code{$C$?.$v$ ??= $e_2$}
+where $C$ is a type literal
+that may or may not be be qualified by an import prefix
+is equivalent to the expression \code{$C$.$v$ ??= $e$}.
 
 \LMHash{}
-A compound assignment of the form $C?.v$ {\em ??=} $e_2$ is equivalent to the expression $C.v$ {\em ??=} $e$.
+\Case{\code{$v$ $op$= $e$}}
+For any other valid operator $op$, a compound assignment of the form \code{$v$ $op$= $e$}
+is equivalent to \code{$v$ = $v$ $op$ $e$},
+where $v$ is an identifier or an identifier qualified by an import prefix.
 
 \LMHash{}
-The static type of a compound assignment of the form $v$ {\em ??=} $e$ is the least upper bound of the static type of $v$ and the static type of $e$.
-Exactly the same compile-time errors that would be caused by $v = e$ are also generated in the case of $v$ {\em ??=} $e$.
+\Case{\code{$C$.$v$ $op$= $e$}}
+A compound assignment of the form \code{$C$.$v$ $op$= $e$}
+where $C$ is a type literal
+that may or may not be qualified by an import prefix
+is equivalent to \code{$C$.$v$ = $C$.$v$ $op$ $e$}.
 
 \LMHash{}
-The static type of a compound assignment of the form $C.v$ {\em ??=} $e$ is the least upper bound of the static type of $C.v$ and the static type of $e$.
-Exactly the same compile-time errors that would be caused by $C.v = e$ are also generated in the case of $C.v$ {\em ??=} $e$.
+\Case{\code{$e_1$.$v$ $op$= $e_2$}}
+Consider a compound assignment $a$ of the form \code{$e_1$.$v$ $op$= $e_2$}.
+Let $x$ be a fresh variable whose static type is the static type of $e_1$.
+Except for errors inside $e_1$ and references to the name $x$,
+exactly the same compile-time errors that would be caused by \code{$x$.$v$ = $x$.$v$ $op$ $e_2$} are also generated in the case of $a$.
+The static type of $a$ is the static type of \code{$e_1$.$v$ $op$ $e_2$}.
 
 \LMHash{}
-The static type of a compound assignment of the form $e_1.v$ {\em ??=} $e_2$ is the least upper bound of the static type of $e_1.v$ and the static type of $e_2$.
-Let $T$ be the static type of $e_1$ and let $z$ be a fresh variable of type $T$.
-Exactly the same compile-time errors that would be caused by $z.v = e_2$ are also generated in the case of $e_1.v$ {\em ??=} $e_2$.
-
-\LMHash{}
-The static type of a compound assignment of the form $e_1[e_2]$ {\em ??=} $e_3$ is the least upper bound of the static type of $e_1[e_2]$ and the static type of $e_3$.
-Exactly the same compile-time errors that would be caused by $e_1[e_2] = e_3$ are also generated in the case of $e_1[e_2]$ {\em ??=} $e_3$.
-
-\LMHash{}
-The static type of a compound assignment of the form $\SUPER.v$ {\em ??=} $e$ is the least upper bound of the static type of $\SUPER.v$ and the static type of $e$.
-Exactly the same compile-time errors that would be caused by $\SUPER.v = e$ are also generated in the case of $\SUPER.v$ {\em ??=} $e$.
-
-\LMHash{}
-For any other valid operator $op$, a compound assignment of the form \code{$v$ $op$= $e$} is equivalent to \code{$v$ = $v$ $op$ $e$}.
-A compound assignment of the form \code{$C$.$v$ $op$= $e$} is equivalent to \code{$C$.$v$ = $C$.$v$ $op$ $e$}.
-
-\LMHash{}
-Evaluation of a compound assignment $a$ of the form \code{$e_1$.$v$ $op$= $e_2$} proceeds as follows:
+Evaluation of a compound assignment $a$ of the form \code{$e_1$.$v$ $op$= $e_2$}
+proceeds as follows:
 Evaluate $e_1$ to an object $u$ and let $x$ be a fresh variable bound to $u$.
 Evaluate \code{$x$.$v$ = $x$.$v$ $op$ $e_2$} to an object $r$
 and then $a$ evaluates to $r$.
 
 \LMHash{}
-Evaluation of s compound assignment $a$ of the form \code{$e_1$[$e_2$] $op$= $e_3$} proceeds as follows:
+\Case{\code{$e_1$[$e_2$] $op$= $e_3$}}
+Consider a compound assignment $a$ of the form \code{$e_1$[$e_2$] $op$= $e_3$}.
+Let $x$ and $i$ be fresh variables
+where the static type of the former is the static type of $e_1$
+and the static type of the latter is the static type of $e_2$.
+Except for errors inside $e_1$ and $e_2$ and references to the names $x$ and $i$,
+exactly the same compile-time errors that would be caused by \code{$x$[$i$] = $x$[$i$] $op$ $e_3$} are also generated in the case of $a$.
+The static type of $a$ is the static type of \code{$x$[$i$] $op$ $e_3$}.
+
+\LMHash{}
+Evaluation of s compound assignment $a$ of the form \code{$e_1$[$e_2$] $op$= $e_3$}
+proceeds as follows:
 Evaluate $e_1$ to an object $u$ and evaluate $e_2$ to an object $v$.
-Let $a$ and $i$ be fresh variables bound to $u$ and $v$ respectively.
-Evaluate \code{$a$[$i$] = $a$[$i$] $op$ $e_3$} to an object $r$,
+Let $x$ and $i$ be fresh variables bound to $u$ and $v$ respectively.
+Evaluate \code{$x$[$i$] = $x$[$i$] $op$ $e_3$} to an object $r$,
 and then $a$ evaluates to $r$.
 
 \LMHash{}
-Evaluation of a compound assignment $a$ of the form \code{$e_1$?.$v$ $op$ = $e_2$} proceeds as follows:
+\Case{\code{$e_1$?.$v$ $op$= $e_2$}}
+Consider a compound assignment $a$ of the form \code{$e_1$?.$v$ $op$= $e_2$}.
+Exactly the same compile-time errors that would be caused by \code{$e_1$.$v$ $op$= $e_2$} are also generated in the case of $a$.
+The static type of $a$ is the static type of \code{$e_1$.$v$ $op$= $e_2$}.
 
 \LMHash{}
+Evaluation of a compound assignment $a$ of the form \code{$e_1$?.$v$ $op$= $e_2$}
+proceeds as follows:
 Evaluate $e_1$ to an object $u$.
 If $u$ is the null object, then $a$ evaluates to the null object (\ref{null}).
 Otherwise let $x$ be a fresh variable bound to $u$.
@@ -6818,12 +7285,10 @@
 Then $a$ evaluates to $r$.
 
 \LMHash{}
-The static type of \code{$e_1$?.$v$ $op$= $e_2$} is the static type of \code{$e_1$.$v$ $op$ $e_2$}.
-Exactly the same compile-time errors that would be caused by \code{$e_1$.$v$ $op$= $e_2$} are also generated in the case of \code{$e_1$?.$v$ $op$= $e_2$}.
-
-\LMHash{}
-A compound assignment of the form $C?.v$ $op = e_2$ is equivalent to the expression
-$C.v$ $op = e_2$.
+\Case{\code{$C$?.$v$ $op$ = $e_2$}}
+A compound assignment of the form \code{$C$?.$v$ $op$ = $e_2$}
+where $C$ is a type literal
+is equivalent to the expression \code{$C$.$v$ $op$ = $e_2$}.
 
 \begin{grammar}
 {\bf compoundAssignmentOperator:}`*=';
@@ -6867,9 +7332,10 @@
 \LMHash{}
 If all of the following hold:
 \begin{itemize}
-\item $e_1$ shows that a variable $v$ has type $T$.
+\item $e_1$ shows that a local variable $v$ has type $T$.
 \item $v$ is not potentially mutated in $e_2$ or within a function.
-\item If the variable $v$ is accessed by a function in $e_2$ then the variable $v$ is not potentially mutated anywhere in the scope of $v$.
+\item If the variable $v$ is accessed by a function in $e_2$ then
+$v$ is not potentially mutated anywhere in the scope of $v$.
 \end{itemize}
 
 then the type of $v$ is known to be $T$ in $e_2$.
@@ -6936,12 +7402,12 @@
 Otherwise the result of evaluating $b$ is $o_2$.
 
 \LMHash{}
-A logical boolean expression $b$ of the form $e_1 \&\& e_2$ shows that a variable $v$ has type
-$T$ if all of the following conditions hold:
+A logical boolean expression $b$ of the form $e_1 \&\& e_2$
+shows that a local variable $v$ has type $T$
+if both of the following conditions hold:
 \begin{itemize}
 \item Either $e_1$ shows that $v$ has type $T$ or $e_2$ shows that $v$ has type $T$.
-\item $v$ is a local variable or formal parameter.
-\item The variable $v$ is not mutated in $e_2$ or within a function.
+\item $v$ is not mutated in $e_2$ or within a function.
 \end{itemize}
 
 \LMHash{}
@@ -6949,7 +7415,8 @@
 \begin{itemize}
 \item $e_1$ shows that $v$ has type $T$.
 \item $v$ is not mutated in either $e_1$, $e_2$ or within a function.
-\item If the variable $v$ is accessed by a function in $e_2$ then the variable $v$ is not potentially mutated anywhere in the scope of $v$.
+\item If $v$ is accessed by a function in $e_2$ then
+$v$ is not potentially mutated anywhere in the scope of $v$.
 \end{itemize}
 then the type of $v$ is known to be $T$ in $e_2$.
 
@@ -7296,7 +7763,7 @@
 }
 
 \LMHash{}
-The static type of $a$ is $flatten(T)$ (the $flatten$ function is defined in section \ref{functionExpressions}) where $T$ is the static type of $e$.
+The static type of $a$ is \flatten{T} (\flatten{} is defined in section \ref{functionExpressions}) where $T$ is the static type of $e$.
 
 
 \subsection{Postfix Expressions}
@@ -7343,7 +7810,7 @@
 
 \LMHash{}
 Evaluation of a postfix expression $e$ of the form \code{$C$.$v$++}
-proceeds as follows:
+where $C$ is a type literal proceeds as follows:
 
 \LMHash{}
 Evaluate \code{$C$.$v$} to a value $r$
@@ -7510,7 +7977,7 @@
 \LMHash{}
 An assignable expression of the form \id{} is evaluated as an identifier expression (\ref{identifierReference}).
 
-%An assignable expression of the form \code{$e$.\id($a_1, \ldots, a_n$)} is evaluated as a method invocation (\ref{methodInvocation}).
+%An assignable expression of the form \code{$e$.\id($a_1, \ldots,\ a_n$)} is evaluated as a method invocation (\ref{methodInvocation}).
 
 \LMHash{}
 An assignable expression of the form \code{$e$.\id} or \code{$e$?.\id} is evaluated as a property extraction (\ref{propertyExtraction}).
@@ -7614,7 +8081,6 @@
 \LMHash{}
 Let $d$ be the innermost declaration in the enclosing lexical scope whose name is \id{} or \code{\id=}.
 If no such declaration exists in the lexical scope, let $d$ be the declaration of the inherited member named \id{} if it exists.
-%If no such member exists, let $d$ be the declaration of the static member name \id{} declared in a superclass of the current class, if it exists.
 
 \begin{itemize}
 \item if $d$ is a prefix $p$, a compile-time error occurs unless the token immediately following $d$ is \code{'.'}.
@@ -7630,10 +8096,9 @@
 %  Otherwise
 %  \item $e$ evaluates to the current binding of \id.
 %  \end{itemize}
-\item If $d$ is a local variable or formal parameter then $e$ evaluates to the current binding of \id.
-%\item If $d$ is a library variable, local variable, or formal parameter, then $e$ evaluates to the current binding of \id. \commentary{This case also applies if d is a library or local function declaration, as these are equivalent to function-valued variable declarations.}
+\item If $d$ is a local variable (\commentary{which can be a formal parameter}) then $e$ evaluates to the current binding of \id.
 \item If $d$ is a static method, top-level function or local function then $e$ evaluates to the function object obtained by closurization (\ref{functionClosurization}) of the declaration denoted by $d$.
-\item If $d$ is the declaration of a static variable, static getter or static setter declared in class $C$, then evaluation of $e$ is equivalent to evaluation of the property extraction (\ref{propertyExtraction}) \code{$C$.\id}.
+\item If $d$ is the declaration of a class variable, static getter or static setter declared in class $C$, then evaluation of $e$ is equivalent to evaluation of the property extraction (\ref{propertyExtraction}) \code{$C$.\id}.
 \item If $d$ is the declaration of a library variable, top-level getter or top-level setter, then evaluation of $e$ is equivalent to evaluation of the top level getter invocation (\ref{topLevelGetterInvocation}) \id.
 \item Otherwise, if $e$ occurs inside a top level or static function (be it function, method, getter, or setter) or variable initializer, evaluation of $e$ causes a \code{NoSuchMethod} to be thrown.
 \item Otherwise, evaluation of $e$ is equivalent to evaluation of the property extraction (\ref{propertyExtraction}) \code{\THIS.\id}.
@@ -7644,12 +8109,19 @@
 
 \begin{itemize}
 \item If $d$ is a class, type alias or type parameter the static type of $e$ is \code{Type}.
-\item If $d$ is a local variable or formal parameter the static type of $e$ is the type of the variable \id, unless \id{} is known to have some type $T$, in which case the static type of $e$ is $T$, provided that $T$ is more specific than any other type $S$ such that $v$ is known to have type $S$.
+\item If $d$ is a local variable (\commentary{which can be a formal parameter})
+  the static type of $e$ is the type of the variable \id,
+  unless \id{} is known to have some type $T$,
+  in which case the static type of $e$ is $T$,
+  provided that $T$ is more specific than any other type $S$ such that $v$ is known to have type $S$.
 \item If $d$ is a static method, top-level function or local function the static type of $e$ is the function type defined by $d$.
-\item If $d$ is the declaration of a static variable, static getter or static setter declared in class $C$, the static type of $e$ is the static type of the getter invocation (\ref{propertyExtraction}) \code{$C$.\id}.
-\item If $d$ is the declaration of a library variable, top-level getter or top-level setter, the static type of $e$ is the static type of the top level getter invocation \id.
-\item Otherwise, if $e$ occurs inside a top level or static function (be it function, method, getter, or setter) or variable initializer, the static type of $e$ is \DYNAMIC{}.
-\item Otherwise, the static type of $e$ is the type of the property extraction (\ref{propertyExtraction}) \THIS{}.\id.
+\item If $d$ is the declaration of a class variable, static getter or static setter declared in class $C$,
+  the static type of $e$ is the static type of the getter invocation (\ref{propertyExtraction}) \code{$C$.\id}.
+\item If $d$ is the declaration of a library variable, top-level getter or top-level setter,
+  the static type of $e$ is the static type of the top level getter invocation \id.
+\item Otherwise, if $e$ occurs inside a top level or static function (be it function, method, getter, or setter) or variable initializer,
+  the static type of $e$ is \DYNAMIC{}.
+\item Otherwise, the static type of $e$ is the type of the property extraction (\ref{propertyExtraction}) \code{\THIS.\id}.
 \end{itemize}
 
 \commentary{
@@ -7707,7 +8179,7 @@
 % Add flow dependent types
 
 \LMHash{}
-Let $v$ be a local variable or a formal parameter.
+Let $v$ be a local variable (\commentary{which can be a formal parameter}).
 An is-expression of the form \code{$v$ \IS{} $T$} shows that $v$ has type $T$ if{}f $T$ is more specific than the type $S$ of the expression $v$ and both $T \ne \DYNAMIC{}$ and $S \ne \DYNAMIC{}$.
 
 \rationale{
@@ -7715,7 +8187,7 @@
 The rules in the current specification are deliberately kept simple.
 It would be upwardly compatible to refine these rules in the future; such a refinement would accept more code without errors, but not reject any code now error-free.
 
-The rule only applies to locals and parameters, as instance or static variables could be modified via side-effecting functions or methods that are not accessible to a local analysis.
+The rule only applies to locals and parameters, as instance and static variables could be modified via side-effecting functions or methods that are not accessible to a local analysis.
 
 It is pointless to deduce a weaker type than what is already known.
 Furthermore, this would lead to a situation where multiple types are associated with a variable at a given point, which complicates the specification.
@@ -7867,11 +8339,14 @@
 If the expression evaluates to a value, then the value is ignored
 and the execution completes normally.
 
+
 \subsection{Local Variable Declaration}
 \LMLabel{localVariableDeclaration}
 
 \LMHash{}
-A {\em variable declaration statement }declares a new local variable.
+A {\em variable declaration statement},
+also known as a {\em local variable declaration},
+has the following form:
 
 \begin{grammar}
 {\bf localVariableDeclaration:}initializedVariableDeclaration `{\escapegrammar ;}'
@@ -7879,37 +8354,153 @@
 \end{grammar}
 
 \LMHash{}
- Executing a variable declaration statement of one of the forms \VAR{} $v = e;$, $T$ $v = e; $, \CONST{} $v = e;$, \CONST{} $T$ $v = e;$, \FINAL{} $v = e;$ or \FINAL{} $T$ $v = e;$ proceeds as follows:
+Each local variable declaration introduces
+a {\em local variable} into the innermost enclosing scope.
+
+\commentary{
+Local variables do not induce getters and setters.
+Note that a formal parameter declaration also introduces
+a local variable into the associated formal parameter scope
+(\ref{formalParameters}).
+}
+
+\LMHash{}
+The properties of being
+{\em initialized}, {\em constant}, {\em final}, and {\em mutable}
+apply to local variables with the same definitions as for other variables
+(\ref{variables}).
+
+\LMHash{}
+We say that a local variable $v$ is {\em potentially mutated} in some scope $s$
+if $v$ is mutable, and an assignment to $v$ occurs in $s$.
+
+\LMHash{}
+A local variable declaration of the form \code{\VAR{} $v$;} is equivalent to \code{\VAR{} $v$ = \NULL{};}.
+A local variable declaration of the form \code{$T$ $v$;} is equivalent to \code{$T$ $v$ = \NULL{};}.
+
+\commentary{
+This holds regardless of the type $T$.
+E.g., \code{int i;} is equivalent to \code{int i = null;}.
+}
+
+\LMHash{}
+The type of a local variable with a declaration of one of the forms
+\code{$T$ $v$ = $e$;}
+\code{\CONST{} $T$ $v$ = $e$;}
+\code{\FINAL{} $T$ $v$ = $e$;}
+is $T$.
+The type of a local variable with a declaration of one of the forms
+\code{\VAR{} $v$ = $e$;}
+\code{\CONST{} $v$ = $e$;}
+\code{\FINAL{} $v$ = $e$;}
+is \DYNAMIC{}.
+
+\LMHash{}
+Let $v$ be an initialized local variable and let $e$ be the associated initializing expression.
+It is a compile-time error if the static type of $e$ is not assignable to the type of $v$.
+It is a compile-time error if a local variable $v$ is final and $v$ is not an initialized variable.
+
+\commentary{
+It is also a compile-time error to assign to a final local variable
+(\ref{assignment}).
+}
+
+\LMHash{}
+It is a compile-time error if
+a local variable is referenced at a source code location that is before
+the end of its initializing expression, if any,
+and otherwise before the identifier which names the variable.
+
+\commentary{
+The example below illustrates the expected behavior.
+A variable `\code{x}' is declared at the library level,
+and another `\code{x}' is declared inside the function `\code{f}'.
+}
+
+\begin{dartCode}
+\VAR{} x = 0;
+
+f(y) \{
+  \VAR{} z = x; // compile-time error
+  if (y) \{
+    x = x + 1; // two compile-time errors
+    print(x); // compile-time error
+  \}
+  \VAR{} x = x++; // compile-time error
+  print(x);
+\}
+\end{dartCode}
+
+\commentary{
+The declaration inside `\code{f}' hides the enclosing one.
+So all references to `\code{x}' inside `\code{f}'
+refer to the inner declaration of `\code{x}'.
+However, many of these references are illegal,
+because they appear before the declaration.
+The assignment to `\code{z}' is one such case.
+The assignment to `\code{x}' in the \IF{} statement
+suffers from multiple problems.
+The right hand side reads `\code{x}' before its declaration,
+and the left hand side assigns to `\code{x}' before its declaration.
+Each of these are, independently, compile-time errors.
+The print statement inside the \IF{} is also illegal.
+
+The inner declaration of `\code{x}' is itself erroneous
+because its right hand side attempts to
+read `\code{x}' before the declaration has terminated.
+The occurrence of `\code{x}' that declares and names the variable
+(that is, the one to the left of `\code{=}' in the inner declaration)
+is not a reference, and so is legal.
+The last print statement is perfectly legal as well.
+}
+
+\commentary{
+As another example \code{\VAR{} x = 3, y = x;} is legal,
+because \code{x} is referenced after its initializer.
+
+A particularly perverse example involves
+a local variable name shadowing a type.
+This is possible because Dart has a
+single namespace for types, functions and variables.
+}
+
+\begin{dartCode}
+\CLASS{} C \{\}
+perverse() \{
+   \VAR{} v = \NEW{} C(); // compile-time error
+   C aC; // compile-time error
+   \VAR{} C = 10;
+\}
+\end{dartCode}
+
+\commentary{
+Inside \code{perverse()}, `\code{C}' denotes a local variable.
+The type `\code{C}' is hidden by the variable of the same name.
+The attempt to instantiate `\code{C}' causes a compile-time error
+because it references a local variable prior to its declaration.
+Similarly, for the declaration of `\code{aC}'.
+}
+
+\LMHash{}
+Execution of a variable declaration statement of one of the forms
+\code{\VAR{} $v$ = $e$;}
+\code{$T$ $v$ = $e$;}
+\code{\CONST{} $v$ = $e$;}
+\code{\CONST{} $T$ $v$ = $e$;}
+\code{\FINAL{} $v$ = $e$;} or
+\code{\FINAL{} $T$ $v$ = $e$;}
+proceeds as follows:
 
 \LMHash{}
 The expression $e$ is evaluated to an object $o$.
 Then, the variable $v$ is set to $o$.
+A dynamic error occurs
+if the dynamic type of $o$ is not a subtype of the actual type
+(\ref{actualTypeOfADeclaration})
+of $v$.
 
-\LMHash{}
-A variable declaration statement of the form \code{\VAR{} $v$;} is equivalent to \code{\VAR{} $v$ = \NULL{};}.
-A variable declaration statement of the form \code{$T$ $v$;} is equivalent to \code{$T$ $v$ = \NULL{};}.
-
-\commentary{
-This holds regardless of the type $T$.
-For example, \code{int i;} does not cause \code{i} to be initialized to zero.
-Instead, \code{i} is initialized to the null object (\ref{null}), just as if we had written \VAR{} \code{i;} or \code{Object i;} or \code{Collection<String> i;}.
-}
-
-\rationale{
-To do otherwise would undermine the optionally typed nature of Dart, causing type annotations to modify program behavior.
-}
-
-%A variable declaration statement of one of the forms $T$ $v;$, $T$ $v = e;$, \CONST{} $T$ $v = e;$, or \FINAL{} $T$ $v = e;$ causes a new getter named $v$ with static return type $T$ to be added to the innermost enclosing scope at the point following the variable declaration statement. The result of executing this getter is the value stored in $v$.
-
-%A variable declaration statement \VAR{} $v;$, \VAR{} $v = e;$, \CONST{} $v = e;$ or \FINAL{} $v = e;$ causes a new getter named $v$ with static return type \DYNAMIC{} to be added to the innermost enclosing scope at the point following the variable declaration statement. The result of executing this getter is the value stored in $v$.
-
-%A variable declaration statement of one of the forms $T$ $v;$, or $T$ $v = e;$ causes a new setter named $v=$ with argument type $T$ to be added to the innermost enclosing scope at the point following the variable declaration statement. The effect of executing this setter is to store its argument in $v$.
-
-%A variable declaration statement \VAR{} $v;$, \VAR{} $v = e;$, \CONST{} $v = e;$ or \FINAL{} $v = e;$ causes a new setter named $v=$ with argument type \DYNAMIC{} to be added to the innermost enclosing scope at the point following the variable declaration statement. The effect of executing this setter is to store its argument in $v$.
-
-%\rationale{
- %The use of getters and setters here is a device to help make the specification more uniform. Introducing getters and setters for local variables has no performance consequences, since they can never be overridden, and so can always be optimized away.  It is not possible to declare a local getter or setter explicitly, since there is little reason to ever do so.
-%}
+% The local variable discussion does not mention how to read/write locals.
+% Consider spelling this out, in terms of storage.
 
 
 \subsection{Local Function Declaration}
@@ -7954,8 +8545,11 @@
 \end{dartCode}
 
 \commentary{
-There is no way to write a pair of mutually recursive local functions, because one always has to come before the other is declared.
-These cases are quite rare, and can always be managed by defining a pair of variables first, then assigning them appropriate function literals:
+There is no way to write a pair of mutually recursive local functions,
+because one always has to come before the other is declared.
+These cases are quite rare,
+and can always be managed by defining a pair of variables first,
+then assigning them appropriate function literals:
 }
 
 \begin{dartCode}
@@ -8022,9 +8616,10 @@
 \LMHash{}
 If:
 \begin{itemize}
-\item $b$ shows that a variable $v$ has type $T$.
+\item $b$ shows that a local variable $v$ has type $T$.
 \item $v$ is not potentially mutated in $s_1$ or within a function.
-\item If the variable $v$ is accessed by a function in $s_1$ then the variable $v$ is not potentially mutated anywhere in the scope of $v$.
+\item If $v$ is accessed by a function in $s_1$ then
+$v$ is not potentially mutated anywhere in the scope of $v$.
 \end{itemize}
 then the type of $v$ is known to be $T$ in $s_1$.
 
@@ -8095,12 +8690,15 @@
 
 \rationale{
 The definition above is intended to prevent the common error where users create a function object inside a for loop,
-intending to close over the current binding of the loop variable,
-and find (usually after a painful process of debugging and learning) that all the created function objects have captured the same value---the one current in the last iteration executed.
+intending to close over the current binding of the loop variable, and find
+(usually after a painful process of debugging and learning)
+that all the created function objects have captured the same value---the one current in the last iteration executed.
 
 Instead, each iteration has its own distinct variable.
 The first iteration uses the variable created by the initial declaration.
-The expression executed at the end of each iteration uses a fresh variable $v''$, bound to the value of the current iteration variable, and then modifies $v''$ as required for the next iteration.
+The expression executed at the end of each iteration uses a fresh variable $v''$,
+bound to the value of the current iteration variable,
+and then modifies $v''$ as required for the next iteration.
 }
 
 \LMHash{}
@@ -8321,7 +8919,7 @@
 \}
 \end{dartCode}
 
- or the form
+or the form
 
 \begin{dartCode}
 \SWITCH{} ($e$) \{
@@ -8331,7 +8929,7 @@
 \}
 \end{dartCode}
 
- it is a compile-time error if the expressions $e_k$ are not compile-time constants for all $k \in 1 .. n$.
+it is a compile-time error if the expressions $e_k$ are not compile-time constants for all $k \in 1 .. n$.
 It is a compile-time error if the values of the expressions $e_k$ are not either:
 \begin{itemize}
 \item instances of the same class $C$, for all $k \in 1 .. n$, or
@@ -8345,7 +8943,11 @@
 }
 
 \LMHash{}
-It is a compile-time error if the class $C$ has an implementation of the operator $==$ other than the one inherited from \code{Object} unless the value of the expression is a string, an integer, literal symbol or the result of invoking a constant constructor of class \code{Symbol}.
+It is a compile-time error if the class $C$ has an implementation of
+the operator \code{==} other than the one inherited from \code{Object},
+unless the expression evaluates to a string or an integer,
+or the expression is a literal symbol or
+an invocation of a constant constructor of class \code{Symbol}.
 
 \rationale{
 The prohibition on user defined equality allows us to implement the switch efficiently for user defined types.
@@ -8679,7 +9281,9 @@
 \LMLabel{return}
 
 \LMHash{}
-The {\em return statement} returns a result to the caller of a synchronous function, completes the future associated with an asynchronous function or terminates the stream or iterable associated with a generator (\ref{functions}).
+The {\em return statement} returns a result to the caller of a synchronous function,
+completes the future associated with an asynchronous function,
+or terminates the stream or iterable associated with a generator (\ref{functions}).
 
 \begin{grammar}
 {\bf returnStatement:}\RETURN{} expression? `{\escapegrammar ;}'
@@ -8687,38 +9291,14 @@
 \end{grammar}
 
 \LMHash{}
-Executing a return statement \code{\RETURN{} $e$;} proceeds as follows:
+Consider a return statement of the form \code{\RETURN{} $e$;}.
+Let $T$ be the static type of $e$, let $f$ be the immediately enclosing function,
+and let $S$ be the declared return type of $f$.
 
 \LMHash{}
-Let $T$ be the static type of $e$, let $f$ be the immediately enclosing function, and let $S$ be the actual return type (\ref{actualTypeOfADeclaration}) of $f$.
-
-\LMHash{}
-First the expression $e$ is evaluated, producing an object $o$.
-If the body of $f$ is marked \ASYNC{} (\ref{functions}) and the run-time type of $o$ is a subtype of \code{Future<$flatten(S)$>}, then let $r$ be the result of evaluating \code{await $v$} where $v$ is a fresh variable bound to $o$. Otherwise let $r$ be $o$.
-Then the return statement returns the value $r$ (\ref{completion}).
-
-\LMHash{}
-It is a compile-time error 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 compile-time error if $T$ may not be assigned to the declared return type of $f$.
-
-\LMHash{}
-Let $S$ be the run-time 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 the null object (\ref{null}),
-% TODO(lrn): Remove the next line when void is a proper supertype of all types.
-the actual return type (\ref{actualTypeOfADeclaration}) of $f$ is not \VOID,
-and \code{Future<$flatten(S)$>} is not a subtype of the actual return type of $f$.
-% TODO(lrn): The "void foo() async { return e }" case is somewhat speculative.
-% When we disallow "return e" in a void function, we might also want to revisit
-% this rule. Currently it also covers the "void foo() async => e;" case, which
-% we might want to allow.
-\item Otherwise, it is a dynamic type error if $o$ is not the null object (\ref{null}),
-% TODO(lrn): Remove the next line when void is a proper supertype of all types.
-the actual return type of $f$ is not \VOID{},
-and $S$ is not a subtype of the actual return type of $f$.
-\end{itemize}
+It is a compile-time error if the body of $f$ is marked \ASYNC{}
+and the type \code{Future<\flatten{T}>} (\ref{functionExpressions}) may not be assigned to $S$.
+Otherwise, it is a compile-time error if $T$ may not be assigned to $S$.
 
 \LMHash{}
 It is a compile-time error if a return statement of the form \code{\RETURN{} $e$;} appears in a generative constructor (\ref{generativeConstructors}).
@@ -8741,12 +9321,16 @@
 Let $f$ be the function immediately enclosing a return statement of the form \RETURN{};.
 It is a compile-time error if $f$ is neither a generator nor a generative constructor and either:
 \begin{itemize}
+%% TODO(eernst): Integrating generalized-void.md, "may not be assigned
+%% to void" is useless. Update, also considering invalid_returns.md.
 \item $f$ is synchronous and the return type of $f$ may not be assigned to \VOID{} (\ref{typeVoid}) or,
+%% TODO(eernst): Revisit when integrating invalid_returns.md.
 \item $f$ is asynchronous and the return type of $f$ may not be assigned to \code{Future<Null>}.
 \end{itemize}
 
 \commentary{
-Hence, a compile-time error will not be raised if $f$ has no declared return type, since the return type would be \DYNAMIC{} and \DYNAMIC{} may be assigned to \VOID{} and to \code{Future<Null>}.
+Hence, a compile-time error will not be raised if $f$ has no declared return type,
+since the return type would be \DYNAMIC{} and \DYNAMIC{} may be assigned to \VOID{} and to \code{Future<Null>}.
 However, any synchronous non-generator function that declares a return type must return an expression explicitly.
 }
 \rationale{
@@ -8763,6 +9347,65 @@
 }
 
 \LMHash{}
+Executing a return statement \code{\RETURN{} $e$;} proceeds as follows:
+
+\LMHash{}
+First the expression $e$ is evaluated, producing an object $o$.
+Let $T$ be the run-time type of $o$ and
+let $S$ be the actual return type of $f$
+(\ref{actualTypeOfADeclaration}).
+If the body of $f$ is marked \ASYNC{} (\ref{functions})
+and $T$ is a subtype of \code{Future<\flatten{S}>}
+then let $r$ be the result of evaluating \code{await $v$}
+where $v$ is a fresh variable bound to $o$.
+Otherwise let $r$ be $o$.
+Then the return statement returns the value $r$ (\ref{completion}).
+
+%% TODO(eernst): We have some special cases with the dynamic semantics
+%% specified above that we may wish to consider:
+%%
+%% Future<int> foo() async {
+%%   return new Future<Object>.value(42);
+%% }
+%%
+%% Statically we will allow this because `Future<flatten(Future<Object>)>`,
+%% i.e., `Future<Object>`, is assignable to `Future<int>`. But at run time
+%% we get an error because `Future<Object>` is is not a subtype of
+%% `Future<flatten(Future<int>)>` = `Future<int>`. We could have awaited
+%% the value just because we're about to return a `Future`, and it would
+%% then have succeeded. Are we doing the right thing? Might be fine, but
+%% it seems surprising that the compiler will sometimes insert `await`,
+%% and here we have to do it explicitly in order to succeed.
+%%
+%% Object /* or dynamic, etc. */ foo() async {
+%%   Object o;
+%%   if (someCondition) o = 42; else o = new Future<T>.value(42);
+%%   return o;
+%% }
+%%
+%% Here we will interject an `await` on the returned value whenever
+%% we return a future (for all `T`). This means that we will `await o`
+%% in some situations and not in others. It may surprise developers
+%% that we can have this dynamic variation at a location in the code
+%% where there is no static justification for expecting a future.
+
+\LMHash{}
+Let $U$ be the run-time type of $r$.
+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 the null object (\ref{null}),
+% TODO(lrn): Remove the next line when void is a proper supertype of all types.
+$S$ is not \VOID,
+and \code{Future<$U$>} is not a subtype of $S$.
+\item Otherwise,
+it is a dynamic type error if $r$ is not the null object (\ref{null}),
+% TODO(lrn): Remove the next line when void is a proper supertype of all types.
+$S$ is not \VOID{},
+and $U$ is not a subtype of $S$.
+\end{itemize}
+
+\LMHash{}
 Executing a return statement with no expression, \code{\RETURN;} returns with no value (\ref{completion}).
 
 
@@ -9015,7 +9658,7 @@
 An assertion with a trailing comma is equivalent to one with that comma removed.
 
 \LMHash{}
-An assertion of the form \code{\ASSERT($e$))} is equivalent to an assertion of the form \code{\ASSERT($e$, \NULL{})}.
+An assertion of the form \code{\ASSERT($e$)} is equivalent to an assertion of the form \code{\ASSERT($e$, \NULL{})}.
 
 \LMHash{}
 Execution of an assert statement executes the assertion as described below
@@ -9301,7 +9944,7 @@
 then let $NS_i = \SHOW{}([\id_1, \ldots,\ \id_k], NS_{i-1}$)
 
 where $show(l,n)$ takes a list of identifiers $l$ and a namespace $n$, and produces a namespace that maps each name in $l$ to the same element that $n$ does.
-Furthermore, for each name $x$ in $l$, if $n$ defines the name $x=$ then the new namespace maps $x=$ to the same element that $n$ does.
+Furthermore, for each name $x$ in $l$, if $n$ defines the name \code{$x$=} then the new namespace maps \code{$x$=} to the same element that $n$ does.
 Otherwise the resulting mapping is undefined.
 
 \item If $C_i$ is of the form
@@ -9310,7 +9953,7 @@
 
 then let $NS_i = \HIDE{}([\id_1, \ldots,\ \id_k], NS_{i-1}$)
 
-where $hide(l, n)$ takes a list of identifiers $l$ and a namespace $n$, and produces a namespace that is identical to $n$ except that for each name $k$ in $l$, $k$ and $k=$ are undefined.
+where $hide(l, n)$ takes a list of identifiers $l$ and a namespace $n$, and produces a namespace that is identical to $n$ except that for each name $k$ in $l$, $k$ and \code{$k$=} are undefined.
 \end{itemize}
 
 \LMHash{}
@@ -9789,7 +10432,8 @@
 
 \LMHash{}
 The static type system ascribes a static type to every expression.
-In some cases, the types of local variables and formal parameters may be promoted from their declared types based on control flow.
+In some cases, the type of a local variable (\commentary{which can be a formal parameter})
+may be promoted from the declared type, based on control flow.
 
 \LMHash{}
 We say that a variable $v$ is known to have type $T$ whenever we allow the type of $v$ to be promoted.
@@ -10033,11 +10677,6 @@
 \subsection{Function Types}
 \LMLabel{functionTypes}
 
-\commentary{
-Note that the non-generic case is covered by using $s = 0$,
-in which case the type parameter declarations are omitted (\ref{generics}).
-}
-
 \LMHash{}
 Function types come in two variants:
 \begin{enumerate}
@@ -10057,15 +10696,10 @@
 \code{($T_1, \ldots,\ T_n,\ $\{$T_{x_1}\ x_1, \ldots,\ T_{x_k}\ x_k$\}) $ \rightarrow T$}.
 \end{enumerate}
 
-%$(T_1, \ldots, T_n) \rightarrow T$ is a subtype of  $(S_1, \ldots, S_n, ) \rightarrow S$, if all of the following conditions are met:
-%\begin{enumerate}
-%\item Either
-%\begin{itemize}
-%\item $S$ is \VOID{}, Or
-%\item $T \Longleftrightarrow S$.
-%\end{itemize}
-%\item$ \forall i \in 1 .. n, T_i \Longleftrightarrow S_i$.
-%\end{enumerate}
+\commentary{
+Note that the non-generic case is covered by using $s = 0$,
+in which case the type parameter declarations are omitted (\ref{generics}).
+}
 
 \LMHash{}
 Two function types are considered equal if consistent renaming of type
@@ -10074,7 +10708,9 @@
 \commentary{
 A common way to say this is that we do not distinguish function types which are alpha-equivalent.
 For the subtyping rule below this means we can assume that a suitable renaming has already taken place.
-In cases where this is not possible because the number of type parameters in the two types differ or the bounds are different, no subtype relationship exists.
+In cases where this is not possible
+because the number of type parameters in the two types differ or the bounds are different,
+no subtype relationship exists.
 }
 
 \LMHash{}