Mixin DEP changes

docs/language/dartLangSpec.tex

 \documentclass{article}
 \usepackage{epsfig}
 \usepackage{color}
 \usepackage{dart}
 \usepackage{bnf}
 \usepackage{hyperref}
 \usepackage{lmodern}
 \newcommand{\code}[1]{{\sf #1}}
-\title{Dart Programming Language  Specification \\
+\title{Dart Programming Language  Specification (Mixin DEP)\\
 {\large Version 1.10}}
 
 % For information about Location Markers (and in particular the
 % commands \LMHash and \LMLabel), see the long comment at the
 % end of this file.
 
 \begin{document}
 \maketitle
 \tableofcontents
 
@@ skipping 1985 matching lines @@
 % Need warnings if overrider conflicts with overriddee either because signatures are incompatible or because done is a method and one is a getter or setter.
 
 \section{Mixins}
 \LMLabel{mixins} 
 
 
 \LMHash{}
 A mixin describes the difference between a class and its superclass. A mixin is always derived from an existing class declaration. 
 
 \LMHash{}
-It is a compile-time error if a declared or derived mixin refers to \SUPER{}. It is a compile-time error if a declared or derived mixin explicitly declares a constructor. It is a compile-time error if a mixin is derived from a class whose superclass is not \code{Object}.
+It is a compile-time error if a declared or derived mixin explicitly declares a constructor. 
 
 \rationale{
-These restrictions are temporary.  We expect to remove them in later versions of Dart.
-
-The restriction on the use of \SUPER{} avoids the problem of rebinding \SUPER{} when the mixin is bound to difference superclasses.
+This restriction is temporary.  We expect to remove it in later versions of Dart.
 
 The restriction on constructors simplifies the construction of mixin applications because the process of creating instances is simpler.
-
-The restriction on the superclass means that the type of a class  from which a mixin is derived is always implemented by any class that mixes it in. This allows us to defer the question of whether and how to express the type of the mixin independently of its superclass and super interface types.
-
-Reasonable answers exist for all these issues, but their implementation is non-trivial.
 }
 
 \subsection{Mixin Application}
 \LMLabel{mixinApplication}
 
 \LMHash{}
 A mixin may be applied to a superclass, yielding a new class. Mixin application occurs when a mixin is mixed into a class declaration via its \WITH{} clause.  The mixin application may be used to extend a class per section (\ref{classes}); alternately, a class may be defined as a mixin application as described in this section.   It is a compile-time error if the \WITH{} clause of a mixin application $C$ includes a deferred type expression.
 
 
 \begin{grammar}
@@ skipping 33 matching lines @@
 
 \commentary{
 If, for example, $M$ declares an instance member $im$ whose type is at odds with the type of a member of the same name in $S$, this will result in a static warning just as if we had defined $K$ by means of an ordinary class declaration extending $S$, with a body that included $im$.
 
 }
 
 \LMHash{}
 The effect of a class definition of the form \code{\CLASS{} $C$ = $M$; } or the form 
  \code{\CLASS{} $C<T_1, \ldots, T_n>$ = $M$; } in library $L$  is to introduce the name $C$ into the scope of $L$, bound to the class (\ref{classes}) defined by the mixin application $M$. The name of the class is also set to $C$. Iff the  class is prefixed by the built-in identifier \ABSTRACT{}, the class being defined is an abstract class.
  
+ Let $M_A$ be a mixin derived from a class $M$ with direct superclass $S_{static}$.
+
+Let $A$ be an application of $M_A$. It is a static warning if the superclass of $A$ is not a subtype of $S_{static}$.
+
+Let $C$ be a class declaration that includes $M_A$ in a with clause. It is a static warning if $C$ does not implement, directly or indirectly, all the direct superinterfaces of $M$.
+ 
 
 \subsection{Mixin Composition}
 \LMLabel{mixinComposition}
 
 \rationale{
 Dart does not directly support mixin composition, but the concept is useful when defining how the superclass of a class with a mixin clause is created.
 }
 
 \LMHash{}
 The {\em composition of two mixins}, $M_1<T_1 \ldots T_{k_{M_1}}>$ and $M_2<U_1  \ldots U_{k_{M_2}}>$, written $M_1<T_1 \ldots T_{k_{M_1}}> * M_2<U_1  \ldots U_{k_{M_2}}>$ defines an anonymous mixin such that for any class $S<V_1 \ldots V_{k_S}>$, the application of 
@@ skipping 429 matching lines @@
 The reserved word \NULL{} denotes the {\em null object}.
 %\Q{Any methods, such as \code{isNull}?}
 
 \begin{grammar}
 {\bf nullLiteral:}
       \NULL{}
 .
 \end{grammar}
 
 \LMHash{}
-The null object is the sole instance of the built-in class \code{Null}. Attempting to instantiate \code{Null} causes a run-time error. It is a compile-time error for a class to attempt to extend or implement \code{Null}. 
+The null object is the sole instance of the built-in class \code{Null}. Attempting to instantiate \code{Null} causes a run-time error. It is a compile-time error for a class to attempt to extend, mix in or implement \code{Null}. 
 Invoking a method on \NULL{}  yields a \code{NoSuchMethodError} unless the method is explicitly implemented by class \code{Null}.
 
 \LMHash{}
 The static type of \NULL{} is $\bot$.
 
 \rationale{The decision to use $\bot$ instead of \code{Null} allows \NULL{} to be be assigned everywhere without complaint by the static checker. 
 }
 
 
 \subsection{Numbers}
@@ skipping 29 matching lines @@
 If a numeric literal begins with the prefix `0x' or `0X', it denotes the hexadecimal integer represented by the part of the literal following `0x' (respectively `0X'). Otherwise, if the numeric literal does not include a decimal point  it denotes a decimal integer.  Otherwise, the numeric literal  denotes a 64 bit double precision floating point number as specified by the IEEE 754 standard. 
 
 \LMHash{}
 In principle, the range of integers supported by a Dart implementations is unlimited. In practice, it is limited by available memory. Implementations may also be limited by other considerations.
 
 \commentary{
 For example, implementations may choose to limit the range to facilitate efficient compilation to Javascript. These limitations should be relaxed as soon as technologically feasible.
 }
 
 \LMHash{}
-It is a compile-time error for a class to attempt to extend or implement \code{int}. It is a compile-time error for a class to attempt to extend or implement \code{double}. It is a compile-time error for any type other than the types \code{int} and \code{double} to attempt to extend or implement \code{num}.
+It is a compile-time error for a class to attempt to extend, mix in or implement \code{int}. It is a compile-time error for a class to attempt to extend, mix in or implement \code{double}. It is a compile-time error for any type other than the types \code{int} and \code{double} to attempt to extend, mix in or implement \code{num}.
 
 \LMHash{}
 An {\em integer literal} is either a hexadecimal integer literal or a  decimal integer literal. Invoking the getter \code{runtimeType} on an integer literal returns the \code{Type} object that is the value of the expression \code{int}. The static type of an integer literal is \code{int}. 
 
 \LMHash{}
 A {\em literal double} is a numeric literal that is not an integer literal. Invoking the getter \code{runtimeType} on a literal double returns the \code{Type} object that is the value of the expression \code{double}.
 The static type of a literal double is \code{double}.
     
 \subsection{Booleans}
 \LMLabel{booleans}
 
 \LMHash{}
 The reserved words \TRUE{} and \FALSE{} denote objects that represent the boolean values true and false respectively. They are the {\em boolean literals}.
 
 \begin{grammar}
 {\bf booleanLiteral:}\TRUE{};
         \FALSE{}
     .
 \end{grammar}
 
 \LMHash{}
-Both  \TRUE{} and \FALSE{} implement the built-in class \code{bool}.  It is a compile-time error for a class to attempt to extend or implement\code{ bool}. 
+Both  \TRUE{} and \FALSE{} implement the built-in class \code{bool}.  It is a compile-time error for a class to attempt to extend, mix in or implement\code{ bool}. 
 
 \commentary{
 It follows that the two boolean literals are the only two instances of \code{bool}. 
 }
 
 \LMHash{}
 Invoking the getter \code{runtimeType} on a boolean literal returns the \code{Type} object that is the value of the expression \code{bool}. The static type of a boolean literal is \code{bool}.
 
 \subsubsection{Boolean Conversion}
 \LMLabel{booleanConversion}
@@ skipping 187 matching lines @@
      stringInterpolation
     .
     
 {\bf NEWLINE:}$\backslash$ n;
       $\backslash$ r
     .
 
  \end{grammar}
  
 \LMHash{}
-All string literals implement the built-in class \code{String}. It is a compile-time error for a class to attempt to extend or implement \code{String}. Invoking the getter \code{runtimeType} on a string literal returns the \code{Type} object that is the value of the expression \code{String}. The static type of a string literal is \code{String}.
+All string literals implement the built-in class \code{String}. It is a compile-time error for a class to attempt to extend, mix in or implement \code{String}. Invoking the getter \code{runtimeType} on a string literal returns the \code{Type} object that is the value of the expression \code{String}. The static type of a string literal is \code{String}.
 
 \subsubsection{String Interpolation}
 \LMLabel{stringInterpolation}
 
 \LMHash{}
 It is possible to embed expressions within non-raw string literals, such that the these expressions are evaluated, and the resulting values are converted into strings and concatenated with the enclosing string. This process is known as {\em string interpolation}.
 
  \begin{grammar}
 {\bf stringInterpolation:}`\$' IDENTIFIER\_NO\_DOLLAR;
       `\$' `\{' expression `\}' % could be top level expression, no?
@@ skipping 906 matching lines @@
 \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$.
 
 \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. 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.
+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. 
 }
 
 
 \subsubsection{ Getter and Setter Lookup}
 \LMLabel{getterAndSetterLookup}
 
 \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$.
 
 \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. 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.
+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.
 
 \rationale {
 The motivation for skipping abstract members during lookup is largely to allow smoother mixin composition. 
 }
 
 
 \subsection{ Top level Getter Invocation}
 \LMLabel{topLevelGetterInvocation}
 
 \LMHash{}
@@ skipping 150 matching lines @@
 
 \LMHash{}
 A super method invocation $i$ has the form 
 
 $\SUPER{}.m(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 list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated  yielding actual argument objects $o_1, \ldots , o_{n+k}$. Let $S$ be the superclass of the immediately enclosing class, and let $f$ be the result of looking up method (\ref{methodLookup})  $m$ in $S$  with respect to the current library $L$. 
+First, the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated  yielding actual argument objects $o_1, \ldots , o_{n+k}$. Let $g$ be the method currently executing, and let $C$ be the class in which $g$ was looked up (\ref{methodLookup}). Let $S_{dynamic}$ be the superclass of $C$, and let $f$ be the result of looking up method (\ref{methodLookup})  $m$ in $S_{dynamic}$  with respect to the current library $L$. 
 Let $p_1 \ldots p_h$ be the required parameters of $f$,  let $p_1 \ldots p_m$ be the positional parameters of $f$ and let $p_{h+1}, \ldots, p_{h+l}$ be the optional parameters declared by $f$.
 
 \LMHash{}
 If  $n < h$, or $n > m$, the method lookup has failed. Furthermore, each $x_i, n+1 \le i \le n+k$,  must have a corresponding named parameter in the set $\{p_{m+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$ with respect to $L$. If the getter lookup succeeded, let $v_g$ be the value of the getter invocation $\SUPER{}.m$. Then the value of $i$ is the result of invoking 
-the static method \code{Function.apply()} with arguments $v.g, [o_1, \ldots , o_n], \{x_{n+1}: o_{n+1}, \ldots , x_{n+k}: o_{n+k}\}$.
+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$. Then the value of $i$ is the result of invoking 
+the static method \code{Function.apply()} with arguments $v_g, [o_1, \ldots , o_n], \{x_{n+1}: o_{n+1}, \ldots , x_{n+k}: o_{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 immutable list with the same  values as  \code{[$o_1, \ldots, o_n$]}.
 \item \code{im.namedArguments} evaluates to an immutable map with the same keys and values as \code{\{$x_{n+1}: o_{n+1}, \ldots, x_{n+k} : o_{n+k}$\}}.
 \end{itemize}
-Then the method \code{noSuchMethod()} is looked up in $S$ and invoked on \THIS{} with argument $im$, and the result of this invocation is the result of evaluating $i$. However, if the implementation found cannot be invoked with a single positional argument, the implementation  of \code{noSuchMethod()} in class \code{Object} is invoked on \THIS{} with argument $im'$, where $im'$ is an instance of \code{Invocation} such that :
+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$. However, if the implementation found cannot be invoked with a single positional argument, the implementation  of \code{noSuchMethod()} in class \code{Object} is invoked on \THIS{} with argument $im'$, where $im'$ is an instance of \code{Invocation} such that :
 \begin{itemize}
 \item  \code{im'.isMethod} evaluates to \code{\TRUE{}}.
 \item  \code{im'.memberName} evaluates to \code{\#noSuchMethod}.
 \item \code{im'.positionalArguments} evaluates to an immutable list whose sole element is  $im$.
 \item \code{im'.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
 \end{itemize}
 
 and the result of this latter invocation is the result of evaluating $i$.
 
 
 \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, in class \code{Object}, in a factory constructor or in a static method or variable initializer.
 
 \LMHash{}
-It is a static type warning if $S$ does not have an accessible (\ref{privacy}) instance member named $m$ unless $S$ or a superinterface of $S$ is annotated with an annotation denoting a constant identical to the constant \code{@proxy} defined in \code{dart:core}. If $S.m$ exists, it  is a static type warning if the type $F$ of $S.m$ may not be assigned to a function type. If $S.m$ does not exist, or if $F$ is not a function type, the static type of $i$ is \DYNAMIC{}; otherwise the static type of $i$ is the declared return type of  $F$.  
+Let $S_{static}$ be the superclass of the immediately enclosing class. It is a static type warning if $S_{static}$ does not have an accessible (\ref{privacy}) instance member named $m$ unless $S_{static}$ or a superinterface of $S_{static}$ is annotated with an annotation denoting a constant identical to the constant \code{@proxy} defined in \code{dart:core}. If $S_{static}.m$ exists, it  is a static type warning 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 the static type of $i$ is the declared return type of  $F$.  
 % 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 static warning 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$.
 
 
 
 
 \subsubsection{Sending Messages}
 \LMLabel{sendingMessages}
 
 \LMHash{}
@@ skipping 94 matching lines @@
 \end{itemize}
 
 
 \subsubsection{Super Getter Access and Method Closurization}
 \LMLabel{superGetterAccessAndMethodClosurization}
 
 \LMHash{}
 Evaluation of a property extraction $i$ of the form $\SUPER.m$ proceeds as follows:
 
 \LMHash{}
- Let $S$ be the superclass of the immediately enclosing class. Let $f$ be the result of looking up method $m$ in $S$ with respect to the current library $L$.  If method lookup succeeds then $i$ evaluates to the closurization of method $f$ with respect to superclass $S$ (\ref{superClosurization}).  
+Let $g$ be the method currently executing, and let $C$ be the class in which $g$ was looked up.  Let $S_{dynamic}$ be the superclass of $C$. Let $f$ be the result of looking up method $m$ in $S_{dynamic}$ with respect to the current library $L$.  If method lookup succeeds then $i$ evaluates to the closurization of method $f$ with respect to superclass $S_{dynamic}$ (\ref{superClosurization}).  
  
 \LMHash{}
- Otherwise, $i$ is a getter invocation.  Let $f$ be the result of  looking up getter $m$ in $S$  with respect to $L$.  The body of $f$  is executed with \THIS{} bound to the current value of  \THIS{}.  The value of $i$ is the result returned by the call to the getter function. 
+ Otherwise, $i$ is a getter invocation.  Let $f$ be the result of  looking up getter $m$ in $S_{dynamic}$  with respect to $L$.  The body of $f$  is executed with \THIS{} bound to the current value of  \THIS{}.  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 :
 \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 the value of \code{\CONST{} []}.
 \item \code{im.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
 \end{itemize}
-Then the method \code{noSuchMethod()} is looked up in $S$ and invoked  with argument $im$, and the result of this invocation is the result of evaluating $i$. However, if the implementation found cannot be invoked with a single positional argument, the implementation  of \code{noSuchMethod()} in class \code{Object} is invoked on \THIS{} with argument $im'$, where $im'$ is an instance of \code{Invocation} such that :
+Then the method \code{noSuchMethod()} is looked up in $S_{dynamic}$ and invoked  with argument $im$, and the result of this invocation is the result of evaluating $i$. However, if the implementation found cannot be invoked with a single positional argument, the implementation  of \code{noSuchMethod()} in class \code{Object} is invoked on \THIS{} with argument $im'$, where $im'$ is an instance of \code{Invocation} such that :
 \begin{itemize}
 \item  \code{im'.isMethod} evaluates to \code{\TRUE{}}.
 \item  \code{im'.memberName} evaluates to \code{\#noSuchMethod}.
 \item \code{im'.positionalArguments} evaluates to an immutable list whose sole element is  $im$.
 \item \code{im'.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
 \end{itemize}
 and the result of this latter invocation is the result of evaluating $i$.
 
 \LMHash{}
-It is a static type warning if $S$ does not have an accessible instance method or getter named $m$.  
+Let $S_{static}$ be the superclass of the immediately enclosing class. It is a static type warning if $S_{static}$ does not have an accessible instance method or getter named $m$.  
 
 The static type of $i$ is:
 \begin{itemize}
-\item The declared return type of $S.m$, if $S$ has an accessible instance getter named $m$.
-\item The static type of function $S.m$ if $S$ has an accessible instance method named $m$.
+\item The declared return type of $S_{static}.m$, if $S_{static}$ has an accessible instance getter named $m$.
+\item The static type of function $S_{static}.m$ if $S_{static}$ has an accessible instance method named $m$.
 \item The type  \DYNAMIC{} otherwise. 
 \end{itemize}
 
 
 \subsubsection{General Closurization}
 \LMLabel{generalClosurization}
 
 \LMHash{}
 Evaluation of a property extraction $i$ of the form $e\#m$ proceeds as follows:
 
@@ skipping 88 matching lines @@
 The static type of $i$ is the type of the constructor function $T()$, if $T$ denotes a class in the surrounding scope with an anonymous constructor $T()$. Otherwise the static type of $i$ is \DYNAMIC{}.
 
 \subsubsection{General Super Property Extraction}
 \LMLabel{generalSuperPropertyExtraction}
 
 
 \LMHash{}
 Evaluation of a property extraction $i$ of the form \SUPER$\#m$ proceeds as follows:
 
  \LMHash{}
-Let $S$ be the superclass of the immediately enclosing class.
+Let $g$ be the method currently executing, and let $C$ be the class in which $g$ was looked up.  Let $S_{dynamic}$ be the superclass of $C$. 
 
  \LMHash{}
-If $m$ is a setter name, let $f$ be the result of looking up setter $m$ in $S$ with respect to the current library $L$. If setter lookup succeeds then $i$ evaluates to the closurization of setter $f$  with respect to superclass $S$  (\ref{superClosurization}).  If setter lookup failed, a \cd{NoSuchMethodError} is thrown.
+If $m$ is a setter name, let $f$ be the result of looking up setter $m$ in $S_{dynamic}$ with respect to the current library $L$. If setter lookup succeeds then $i$ evaluates to the closurization of setter $f$  with respect to superclass $S_{dynamic}$  (\ref{superClosurization}).  If setter lookup failed, a \cd{NoSuchMethodError} is thrown.
 
-If $m$ is not a setter name, let $f$ be the result of looking up method $m$ in $S$ with respect to the current library $L$. If method lookup succeeds then $i$ evaluates to the closurization of method $m$ with respect to superclass $S$ (\ref{superClosurization}).
+If $m$ is not a setter name, let $f$ be the result of looking up method $m$ in $S_{dynamic}$ with respect to the current library $L$. If method lookup succeeds then $i$ evaluates to the closurization of method $m$ with respect to superclass $S_{dynamic}$ (\ref{superClosurization}).
 
 \LMHash{}
- Otherwise, let $f$ be the result of looking up getter $m$ in $S$ with respect to the current library $L$.  If getter lookup succeeds then $i$ evaluates to the closurization of getter $f$ with respect to superclass $S$ (\ref{superClosurization}).   If getter lookup failed, a \cd{NoSuchMethodError} is thrown.
+ Otherwise, let $f$ be the result of looking up getter $m$ in $S_{dynamic}$ with respect to the current library $L$.  If getter lookup succeeds then $i$ evaluates to the closurization of getter $f$ with respect to superclass $S_{dynamic}$ (\ref{superClosurization}).   If getter lookup failed, a \cd{NoSuchMethodError} is thrown.
 
 \LMHash{}
-It is a static type warning if $S$ does not have an accessible instance member named $m$.
+Let $S_{static}$ be the superclass of the immediately enclosing class.It is a static type warning if $S_{static}$ does not have an accessible instance member named $m$.
 
 \LMHash{}
-The static type of $i$ is the static type of the function $S.m$,  if $S$ has an accessible instance member named $m$. Otherwise the static type of $i$ is \DYNAMIC{}.
+The static type of $i$ is the static type of the function $S_{static}.m$,  if $S_{static}$ has an accessible instance member named $m$. Otherwise the static type of $i$ is \DYNAMIC{}.
 
 
 
 \subsubsection{Ordinary Member Closurization}
 \LMLabel{ordinaryMemberClosurization}
 
 
 \LMHash{}
 Let $o$ be an object, and let $u$ be a fresh final variable bound to $o$.
 The {\em closurization of method $f$ on object $o$} is defined to be equivalent to:
@@ skipping 241 matching lines @@
 
 
 
 \LMHash{}
 It is a static type warning 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$.
 
 \LMHash{}
 Evaluation of an assignment of the form $\SUPER.v$ \code{=} $e$ proceeds as follows:
 
 \LMHash{}
-Let $S$ be the superclass of the immediately enclosing class.
-The expression $e$ is evaluated to an object $o$.  Then, the setter $v=$ is looked up (\ref{getterAndSetterLookup}) in $S$ with respect to the current library.  The body  of $v=$ is executed with its formal parameter bound to $o$ and \THIS{} bound to \THIS{}. 
+Let $g$ be the method currently executing, 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{}. 
 
 \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 immutable list with the same values as \code{[$o$]}.
 \item \code{im.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
 \end{itemize}
 
 \LMHash{}
-Then the method \code{noSuchMethod()} is looked up in $S$ and invoked  with argument $im$. 
+Then the method \code{noSuchMethod()} is looked up in $S_{dynamic}$ and invoked  with argument $im$. 
 However, if the implementation found cannot be invoked with a single positional argument, the implementation  of \code{noSuchMethod()} in class \code{Object} is invoked on \THIS{} with argument $im'$, where $im'$ is an instance of \code{Invocation} such that :
 \begin{itemize}
 \item  \code{im'.isMethod} evaluates to \code{\TRUE{}}.
 \item  \code{im'.memberName} evaluates to \code{\#noSuchMethod}.
 \item \code{im'.positionalArguments} evaluates to an immutable list whose sole element is  $im$.
 \item \code{im'.namedArguments} evaluates to the value of \code{\CONST{} \{\}}.
 \end{itemize}
 
 \LMHash{}
 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 \NULL{} and the interface of the class of $o$ is not a subtype of the actual type of $S.v$.
 
 \LMHash{}
-It is a static type warning if $S$ does not have an accessible instance setter named $v=$ unless $S$ or a superinterface of $S$ is annotated with an annotation denoting a constant identical to the constant \code{@proxy} defined in \code{dart:core}. 
+Let $S_{static}$ be the superclass of the immediately enclosing class. It is a static type warning if $S_{static}$ does not have an accessible instance setter named $v=$ unless $S_{static}$ or a superinterface of $S_{static}$ is annotated with an annotation denoting a constant identical to the constant \code{@proxy} defined in \code{dart:core}. 
 
 \LMHash{}
 It is a static type warning 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{}
@@ skipping 3315 matching lines @@
 
 The invariant that each normative paragraph is associated with a line
 containing the text \LMHash{} should be maintained.  Extra occurrences
 of \LMHash{} can be added if needed, e.g., in order to make
 individual \item{}s in itemized lists addressable.  Each \LM.. command
 must occur on a separate line.  \LMHash{} must occur immediately
 before the associated paragraph, and \LMLabel must occur immediately
 after the associated \section{}, \subsection{} etc.
 
 ----------------------------------------------------------------------