Update spec for 0.8: Malformed types cause runtime errors for as, is and catch clauses, as well as …

docs/language/dartLangSpec.tex

 \documentclass{article}
 \usepackage{epsfig}
 \usepackage{dart}
 \usepackage{bnf}
 \usepackage{hyperref}
 \newcommand{\code}[1]{{\sf #1}}
 \title{Dart Programming Language  Specification \\
-{\large Draft Version 0.71}}
+{\large Draft Version 0.8}}
 \author{The Dart Team}
 \begin{document}
 \maketitle
 
 \tableofcontents
 
 \newpage
 
 \pagestyle{myheadings}
 \markright{{\bf Draft}  Dart Programming Language Specification {\bf Draft}}
@@ skipping 488 matching lines @@
 
 \ref{typePromotion}: Added notion of type promotion.
 
 \ref{typedef}: Banned all recursion in typedefs.
 
 \subsubsection{Changes Since Version 0.7}
 
 
 \ref{variables}: Final variables no longer introduce setters.
 
+\ref{superinterfaces}: Described \cd{@proxy} annotation's effects on typechecking.
+
+\ref{metadata}: Banned use of types as metadata.
+
 \ref{new}: Instantiating subclasses of malbounded types is a dynamic error.
 
+\ref{typeTest}, \ref{typeCast}, \ref{try}: Use of malformed type in casts, type tests and catch clauses is a dynamic error.
+
+\ref{scripts}: Corrected rules for running scripts.
+
+\ref{dynamicTypeSystem}: In checked mode, subtype tests against malbounded types are dynamic errors.
+
 \ref{leastUpperBounds}:  Extended LUBs to all types.
 
 
 
 \section{Notation}
 \label{notation}
 
 We distinguish between normative and non-normative text. Normative text defines the rules of Dart. It is given in this font. At this time, non-normative text includes:
 \begin{itemize}
 \item[Rationale] Discussion of the motivation for language design decisions appears in italics. \rationale{Distinguishing normative from non-normative helps clarify what part of the text is binding and what part is merely expository.}
@@ skipping 1544 matching lines @@
 
 It is a compile-time error if  the \IMPLEMENTS{}  clause of a class $C$ specifies a type variable as a superinterface. It is a compile-time error if  the  \IMPLEMENTS{} clause of a class $C$ specifies  a malformed type as a superinterface  It is a compile-time error if the \IMPLEMENTS{} clause of a class $C$ specifies type \DYNAMIC{} as a superinterface. It is a compile-time error if  the  \IMPLEMENTS{} clause of a class $C$ specifies  a type $T$ as a superinterface more than once.
 It is a compile-time error if the superclass of a class $C$ is specified as a superinterface of $C$.
 
 \rationale{
 One might argue that it is harmless to repeat a type in the superinterface list, so why make it an error? The issue is not so much that the situation described in program source is erroneous, but that it is pointless. As such, it is an indication that the programmer may very well have meant to say something else - and that is a mistake that should be called to her or his attention.  Nevertheless, we could simply issue a warning; and perhaps we should and will. That said, problems like these are local and easily corrected on the spot, so we feel justified in taking a harder line. 
 }
 
 It is a compile-time error if the interface of a class $C$ is a superinterface of itself.
 
-Let $C$ be a concrete class that does not declare its own \code{noSuchMethod()} method.
+Let $C$ be a concrete class that does not declare its own \code{noSuchMethod()} method and is not annotated with a metadata declaration of the form \cd{@proxy}, where \cd{proxy} is declared in \cd{dart:core}.
 It is a static warning if the implicit interface of  $C$ includes an instance member $m$ of type $F$ and $C$ does not declare or inherit a corresponding instance member $m$ of type $F'$ such that $F' <: F$. 
 
 \commentary{A class does not inherit members from its superinterfaces. However, its implicit interface does.
 }
 
 
 \rationale {
 We choose to issue these warnings only for concrete classes; an abstract class might legitimately be designed with the expectation that concrete subclasses will implement part of  the interface.
 We also disable these warnings if a \code{noSuchMethod()} declaration is present. In such cases, the supported interface is going to be implemented via \code{noSuchMethod()} and no actual declarations of the implemented interface's members are needed. This allows proxy classes for specific types to be implemented without provoking type warnings.
+
+In addition, it may be useful to suppress these warnings if \code{noSuchMethod} is inherited, However, this may suppress meaningful warnings and so we choose not to do so by default. Instead, a special annotation is defined in \cd{dart:core} for this purpose.
 }
 
 It is a static warning if the implicit interface of  a class $C$ includes an instance member $m$ of type $F$ and $C$ declares or inherits a corresponding instance member $m$ of type $F'$ if  $F'$ is not a subtype of $F$. 
 
 \rationale{
 However, if a class does explicitly declare a member that conflicts with its superinterface, this always yields a static warning.
 
 }
 %It is a static warning if an imported superinterface of a class $C$ declares private members.
 
@@ skipping 144 matching lines @@
 
 A  mixin application of the form  \code{$S$ \WITH{} $M_1, \ldots, M_k$;} defines a class  $C$ whose superclass is the application of the mixin composition (\ref{mixinComposition}) $M_{k-1} * \ldots * M_1$ to $S$. 
 
 In both cases above, $C$ declares the same instance members as $M$ (respectively, $M_k$). If any of the instance fields of $M$ (respectively, $M_k$) have initializers, they are executed in the scope of $M$ (respectively, $M_k$) to initialize the corresponding fields of $C$. 
 
 For each generative constructor named $q_i(T_{i1}$ $ a_{i1}, \ldots , T_{ik_i}$ $ a_{ik_i}), i \in 1..n$ of $S$, $C$ has an implicitly declared constructor named
 $q'_i = [C/S]q_i$ of the form 
 
 $q'_i(a_{i1}, \ldots , a_{ik_i}):\SUPER(a_{i1}, \ldots , a_{ik_i});$.
 
-% The types must be given in the copied constructor. It was tempting to elide them; after all, checked mode will catch things in the
-% super call - but this may be a problem for tools. 
-% We  interpret this instead as S includes the generic parameters, so the signature has already substituted them.
-% Default values may not be replicable for optional params due to scoping/privacy.
-% How to describe and implement
-
-%The class $C$ has an implicitly declared nullary generative constructor with no initializer list and no body. 
-
 If the mixin application declares support for interfaces, the resulting class implements those interfaces.
 
 It is a compile-time error if $S$ is a malformed type. It is a compile-time error if $M$ (respectively, any of $M_1, \ldots, M_k$) is a malformed type. It is a compile time error if a well formed mixin cannot be derived from $M$ (respectively, from each of $M_1, \ldots, M_k$). 
 
 Let $K$ be a class declaration  with the same constructors, superclass and interfaces as $C$,  and the instance members declared by $M$ (respectively $M_1, \ldots, M_k$). It is a static warning if the declaration of $K$ would cause a static warning.  It is a compile-time error if the declaration of $K$ would cause a compile-time error.
 
 \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$.
 
-%Another implication of this definition is that one cannot apply a mixin to a superclass that does not provide a nullary constructor.
 }
 
 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.
  
 
 \subsection{Mixin Composition}
 \label{mixinComposition}
 
 \rationale{
@@ skipping 117 matching lines @@
 
 \begin{grammar}
 {\bf metadata:}
       (`@' qualified ({\escapegrammar `.'} identifier)? (arguments)?)*
     .
 \end{grammar}
 
 Metadata consists of a series of annotations, each of which begin with the character @, followed by  a constant expression that starts with an identifier. It is a compile time error if the expression is not one of the following:
 \begin{itemize}
 \item A reference to a compile-time constant variable.
-\item The name of a class.
 \item A call to a constant constructor.
 \end{itemize}
 
 Metadata is associated with the abstract syntax tree of the program construct $p$ that immediately follows the metadata, assuming $p$ is not itself metadata or a comment. Metadata can be retrieved at runtime via a reflective call, provided the annotated program construct $p$ is accessible via reflection.
 
 \commentary{
 Obviously, metadata can also be retrieved statically by parsing the program and evaluating the constants via a suitable interpreter. In fact many if not most uses of metadata are entirely static.
 }
 
 \rationale{
@@ skipping 93 matching lines @@
 A {\em constant expression} is an expression whose value can never change, and that can be evaluated entirely at compile time. 
 
 A constant expression is one of the following:
 \begin{itemize}
 \item A literal number (\ref{numbers}).
 \item A literal boolean (\ref{booleans}).
 \item A literal string (\ref{strings}) where any interpolated expression  (\ref{stringInterpolation}) is a compile-time constant that evaluates to a numeric, string or boolean value or to \NULL{}.
 \rationale{It would be tempting to allow string interpolation where the interpolated value is any compile-time constant.  However, this would require running the \code{toString()} method for constant objects, which could contain arbitrary code.}
 \item A literal symbol (\ref{symbols}).
 \item \NULL{} (\ref{null}).
-\item A qualified reference to a static constant variable (\ref{variables}). \commentary {For example, If class C declares a constant static 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.
+\item A qualified reference to a static constant variable (\ref{variables}). 
+\commentary {For example, If class C declares a constant static 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.
 }
-\item An identifier expression that denotes a constant variable, class or a type alias.
+\item An identifier expression that denotes a constant variable. %CHANGE in googledoc
+\item A simple or qualified identifier denoting a class or a type alias. 
+\commentary {For example, if C is a class or typedef C is a constant, and if C is imported with a prefix p,  p.C is a constant.
+}
 \item A constant constructor invocation (\ref{const}).  
 \item A constant list literal (\ref{lists}).
 \item A constant map literal (\ref{maps}).
 \item A simple or qualified identifier denoting a top-level function (\ref{functions}) or a static method (\ref{staticMethods}).
 \item A parenthesized expression \code{($e$)} where $e$ is a constant expression.
 \item An expression of the form \code{identical($e_1$, $e_2$)} where $e_1$ and $e_2$ are constant expressions  and \code{identical()} is statically bound to the predefined dart function   \code{identical()} discussed above (\ref{objectIdentity}).
 \item An expression of one of the forms  \code{$e_1$ == $e_2$} or  \code{$e_1$ != $e_2$} where $e_1$ and $e_2$ are constant expressions that evaluate to a numeric, string or boolean value or to \NULL{}.
 \item An expression of one of the forms \code{!$e$}, \code{$e_1$ \&\& $e_2$} or \code{$e_1 || e_2$}, where  $e$, $e_1$ and $e_2$ are constant expressions that evaluate to a boolean value.
 \item An expression of one of the forms \~{}$e$, $e_1$ \^{} $e_2$, \code{$e_1$ \& $e_2$}, $e_1 | e_2$, $e_1 >> e_2$ or $e_1 <<  e_2$, where  $e$, $e_1$ and $e_2$ are constant expressions that evaluate to an integer value  or to \NULL{}.
 \item An expression of one of the forms \code{$-e$},  \code{$e_1 + e_2$}, \code{$e_1$ - $e_2$}, \code{$e_1$ * $e_2$}, \code{$e_1$ / $e_2$,} \code{$e_1$ \~{}/ $e_2$},  \code{$e_1  >  e_2$}, \code{$e_1  <  e_2$}, \code{$e_1$ $>$= $e_2$}, \code{$e_1$ $<$= $e_2$} or \code{$e_1$ \% $e_2$},  where $e$, $e_1$ and $e_2$ are constant expressions that evaluate to a numeric value  or to \NULL{}.
@@ skipping 411 matching lines @@
 The value of a constant list literal  \CONST{} $<E>[e_1\ldots e_n]$ is an object $a$ whose class implements the built-in class $List<E>$. The $i$th element of $a$ is $v_{i+1}$, where $v_i$ is the value of the compile-time expression $e_i$.  The value of a constant list literal  \CONST{} $[e_1 \ldots e_n]$ is defined as the value of the constant list literal \CONST{}$ < \DYNAMIC{}>[e_1\ldots e_n]$.
 
 Let $list_1 =$ \CONST{} $<V>[e_{11} \ldots e_{1n}]$ and $list_2 =$  \CONST{} $<U>[e_{21} \ldots e_{2n}]$ be two constant list literals and let the  elements of $list_1$ and $list_2$  evaluate to  $o_{11} \ldots o_{1n}$ and $o_{21} \ldots o_{2n}$ respectively. Iff \code{identical($o_{1i}$, $o_{2i}$)} for $i \in 1.. n$ and $V = U$ then \code{identical($list_1$, $list_2$)}. 
 
 \commentary{In other words, constant list literals are canonicalized.}
 
 A run-time list literal $<E>[e_1 \ldots e_n]$  is evaluated as follows:
 \begin{itemize}
 \item
 First, the expressions $e_1 \ldots e_n$ are evaluated in order they appear in the program, yielding objects $o_1 \ldots o_n$.
-\item
-A fresh instance  (\ref{generativeConstructors}) $a$, of size $n$,  whose class implements the built-in class $List<E>$ is allocated. 
+\item A fresh instance  (\ref{generativeConstructors}) $a$, of size $n$,  whose class implements the built-in class $List<E>$ is allocated. 
 \item
 
 The operator \code{[]=} is invoked on $a$ with  first  argument $i$ and second argument
 %The $i$th element of $a$ is set to 
 $o_{i+1}, 0 \le i < n$.
 \item
 The result of the evaluation is $a$.
 \end{itemize}
 
 
@@ skipping 44 matching lines @@
 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>$. The entries of $m$ are $u_i:v_i, i \in 1 .. n$, where $u_i$ is the value of the compile-time expression $k_i$ and $v_i$ is the value of the compile-time expression $e_i$.  The value of a constant map literal  \CONST{} $\{k_1:e_1\ldots k_n :e_n\}$ is defined as the value of a constant map literal \CONST{} $<\DYNAMIC{}, \DYNAMIC{}>\{k_1:e_1\ldots k_n :e_n\}$.
 
 Let $map_1 =$ \CONST{}$ <K, V>\{k_{11}:e_{11} \ldots k_{1n} :e_{1n}\}$ and  $map_2 =$  \CONST{}$ <J, U>\{k_{21}:e_{21} \ldots k_{2n} :e_{2n}\}$ be two constant map literals. Let the keys of $map_1$ and $map_2$ evaluate to  $s_{11} \ldots  s_{1n}$  and   $s_{21} \ldots  s_{2n}$ respectively, and let the elements of $map_1$ and $map_2$ evaluate to $o_{11} \ldots  o_{1n}$ and $o_{21} \ldots  o_{2n}$ respectively. Iff \code{identical($o_{1i}$, $o_{2i}$)}  and \code{identical($s_{1i}$, $s_{2i}$)} for $i \in 1.. n$, and $K = J, V = U$ then \code{identical($map_1$, $map_2$)}. 
 
 \commentary{In other words, constant map literals are canonicalized.}
 
 A runtime map literal $<K, V>\{k_1:e_1\ldots k_n :e_n\}$  is evaluated as follows:
 \begin{itemize}
 \item
 First, the expression $k_i$ is evaluated yielding object $u_i$, the $e_i$ is vaulted yielding object $o_i$, for $i \in 1..n$ in left to right order, yielding objects $u_1, o_1\ldots u_n, o_n$.
-\item 
-A fresh instance (\ref{generativeConstructors}) $m$ whose class implements the built-in class $Map<K, V>$ is allocated. 
+\item  A fresh instance (\ref{generativeConstructors}) $m$ whose class implements the built-in class $Map<K, V>$ is allocated. 
 \item
 The operator \code{[]=} is invoked on $m$ with  first  argument $u_i$ and second argument $o_i,  i \in 1.. n$.
 \item
 The result of the evaluation is $m$.
 \end{itemize}
 
 
 A runtime map literal  $\{k_1:e_1\ldots k_n :e_n\}$ is evaluated as  $<\DYNAMIC{},  \DYNAMIC{}>\{k_1:e_1\ldots k_n :e_n\}$.
 
 Iff all the keys in a map literal are compile-time constants, it is a static warning if the values of any two keys in a map literal are equal.
@@ skipping 165 matching lines @@
 
 First, the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated. 
 
 Then, if $q$ is a non-factory constructor of an abstract class then an \code{AbstractClassInstantiationError} is thrown.
 
 If $T$  is malformed or if $T$ is a type variable a dynamic error occurs. In checked mode, if $T$ or any of its superclasses is malbounded a dynamic error occurs.
  Otherwise, if $q$ is not defined or not accessible, a \code{NoSuchMethodError} is thrown.  If $q$ has  less than $n$ positional parameters or more than $n$ required parameters, or if $q$ lacks any of the keyword parameters $\{ x_{n+1}, \ldots, x_{n+k}\}$ a \code{NoSuchMethodError} is thrown.
 
 Otherwise, if $q$ is a generative constructor (\ref{generativeConstructors}), then:
 
-%Let $T_i$ be the type parameters of $R$ (if any) and let $B_i$ be the bound of $T_i, 1 \le i \le l$.
-%In checked mode, it is a dynamic type error if  $V_i$ is not a subtype of  $[V_1,  \ldots, V_l/T_1,  \ldots, T_l]B_i,  i \in 1.. l$.
-
 \commentary{Note that it this point we are assured that the number of actual type arguments match the number of formal type parameters.}
 
 A fresh instance (\ref{generativeConstructors}), $i$,  of class $R$ is allocated. For each instance variable $f$ of $i$,  if the variable declaration of $f$ has an initializer expression $e_f$, then $e_f$ is evaluated to an object $o_f$ and $f$ is bound to $o_f$. Otherwise $f$ is bound to \NULL{}.
 
 \commentary{
 Observe that \THIS{} is not in scope in $e_f$. Hence, the initialization cannot depend on other properties of the object being instantiated.
 }
 
 Next,  $q$ is executed  with \THIS{} bound to $i$,  the type parameters (if any) of $R$ bound to the actual type arguments $V_1, \ldots, V_l$ and the formal parameter bindings that resulted from the evaluation of the argument list. The result of the evaluation of $e$ is $i$.
 
 Otherwise, $q$ is a factory constructor (\ref{factories}). Then:
 
-%Let $T_i$ be the type parameters of $R$ (if any) and let $B_i$ be the bound of $T_i, 1 \le i \le l$.
-%In checked mode, it is a dynamic type error if  $V_i$ is not a subtype of  $[V_1,  \ldots, V_l/T_1,  \ldots, T_l]B_i, i \in 1.. l$.
-
 If $q$ is a redirecting factory constructor of the form $T(p_1, \ldots, p_{n+k}) = c;$ or of the form  $T.id(p_1, \ldots, p_{n+k}) = c;$ then the result of the evaluation of $e$ is equivalent to evaluating the expression $[V_1,  \ldots, V_m/T_1,  \ldots, T_m]($\code{\NEW{} $c(a_1, \ldots, a_n, x_{n+1}: a_{n+1}, \ldots, x_{n+k}: a_{n+k}))$}.
 
 Otherwise, the body of $q$ is executed with respect to the bindings that resulted from the evaluation of the argument list and the type parameters (if any) of $q$ bound to the actual type arguments $V_1, \ldots, V_l$ resulting in an object $i$. The result of the evaluation of $e$ is $i$.
 
 It is a static warning 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 a warning. 
 A similar clause applies to constant object creation in the next section.
 } 
 
@@ skipping 204 matching lines @@
 
 {\bf argumentList:}namedArgument (`,' namedArgument)*;
   %    expressionList ',' spreadArgument;
       expressionList (`,' namedArgument)*
 %      spreadArgument
     .
 
 {\bf namedArgument:}
       label expression % could be top level expression?
     .
-
-%spreadArgument:
-%     '...' expression
- %   .
  \end{grammar}
 
 Evaluation of an actual argument list of the form $(a_1, \ldots, a_m, q_1: a_{m+1}, \ldots, q_l: a_{m+l})$ proceeds as follows:
 
-%Furthermore, if $p_k$ is a rest parameter, then one of the following cases holds:
-%\begin{enumerate}
-%\item $m = k-1$. Then $p_k$ is bound to a freshly allocated empty list. \Q{cant we share it? identity?}
-%\item $m = k$, and $a_k$ is a spread argument ...$e_k$. Then $p_k$ is bound to the value of $e_k$.  In checked mode, it is a dynamic type error if  the type of $p_k$ is not a supertype of the value of $e_k$.
-%\item $m \ge k$.  A freshly allocated list $r$ of the type of $p_k$ with size $m - k + 1$ is allocated. and initialized such that $r_j = a_{k+j}, 0 \le j \le m - k$. Then $p_k$ is bound to $r$.
-%\end{enumerate}
-
-%Otherwise, i
 The arguments $a_1, \ldots, a_{m+l}$ are evaluated in the order they appear in the program, yielding objects $o_1, \ldots, o_{m+l}$.
 
 \commentary{Simply stated, an argument list consisting of $m$ positional arguments and $l$ named arguments is evaluated from left to right.
 }
 
 
 \subsubsection{ Binding Actuals to Formals}
 \label{bindingActualsToFormals}
 
 Let $f$ be a function with $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$.
@@ skipping 903 matching lines @@
  .
  
  
 {\bf isOperator:}
 \IS{} `!'?
     .
  \end{grammar}
  
  Evaluation of the is-expression \code{$e$ \IS{} $T$} proceeds as follows:
 
-The expression $e$ is evaluated to a value $v$. Then, if the interface of the class of $v$ is a subtype of $T$, the is-expression evaluates to true. Otherwise it evaluates to false.
+The expression $e$ is evaluated to a value $v$. Then, if $T$ is malformed, a dynamic error occurs. Otherwise, if the interface of the class of $v$ is a subtype of $T$, the is-expression evaluates to true. Otherwise it evaluates to false.
 
 \commentary{It follows that \code{$e$ \IS{} Object} is always true. This makes sense in a language where everything is an object. 
 
 Also note that \code{\NULL{} \IS{} $T$} is false unless $T = \code{Object}$, $T = \code{\DYNAMIC{}}$ or $T = \code{Null}$.  The former two are useless, as is anything of the form \code{$e$ \IS{} Object} or \code{$e$ \IS{} \DYNAMIC{}}.  Users should test for a null value directly rather than via type tests.
 }
 
 The is-expression \code{$e$ \IS{}! $T$} is equivalent to \code{!($e$ \IS{} $T$)}.
 
 % Add flow dependent types
 
-\commentary{
-If $T$ is malformed the test always succeeds. This is a consequence of the rule that malformed types are treated as \DYNAMIC{}
-}
-%does not denote a type available in the current lexical scope. It is a %compile-time error % CHANGED
-%run-time error
-%if $T$ is a parameterized type of the form $G<T_1, \ldots, T_n>$ and $G$ is not a generic type with $n$ type parameters.
-
-%Note, that, in checked mode, it is a dynamic type error if a malformed type is used in a type test as specified in \ref{dynamicTypeSystem}.
-
-%It is a static warning if $T$ is malformed or malbounded.
-%does not denote a type available in the current lexical scope. 
 
 Let $v$  be a local variable or a formal parameter. An is-expression of the form \code{$v$ \IS{} $T$} shows that $v$  has type $T$ iff $T$ is more specific than the type $S$ of the expression $v$ and  both $T \ne \DYNAMIC{}$ and $S \ne \DYNAMIC{}$.
 
 \rationale{
 The motivation for the ``shows that v has type T" relation is to reduce spurious warnings thereby enabling a more natural coding style. 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 warning, but not reject any code now warning-free.
 
 The rule only applies to locals and parameters, as fields 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. Hence the requirement that $T << S$ (we use $<<$ rather than subtyping because subtyping is not a partial order).
 
 We do not want to refine the type of a variable of type \DYNAMIC{}, as this could lead to more warnings rather than less.  The opposite requirement, that $T \ne \DYNAMIC{}$ is a safeguard lest $S$ ever be $\bot$.
 }
 
 The static type of an is-expression is \code{bool}. 
-%It is a static warning if if $T$ is a parameterized type of the form $G<T_1, \ldots, T_n>$ and $G$ is not a generic type with $n$ type parameters. 
-
 
 
 \subsection{ Type Cast}
 \label{typeCast}
 
 The {\em cast expression} ensures that an object is a member of a type.
 
  \begin{grammar}
  {\bf typeCast:}
  asOperator type
  .
  
  
 {\bf asOperator:}
 \AS{}
     .
  \end{grammar}
  
  Evaluation of the cast expression \code{$e$ \AS{} $T$} proceeds as follows:
 
-The expression $e$ is evaluated to a value $v$. Then, if the interface of the class of $v$ is a subtype of $T$, the cast expression evaluates to $v$. Otherwise, if $v$ is \NULL{}, the cast expression evaluates to $v$. 
+The expression $e$ is evaluated to a value $v$. Then, if $T$ is malformed, a dynamic error occurs. Otherwise, if the interface of the class of $v$ is a subtype of $T$, the cast expression evaluates to $v$. Otherwise, if $v$ is \NULL{}, the cast expression evaluates to $v$. 
 In all other cases,  a \code{CastError} is thrown.
-
-\commentary{
-If $T$ is malformed the cast always succeeds. This is a consequence of the rule that malformed types are treated as \DYNAMIC{}
-}
-
-%does not denote a type available in the current lexical scope. It is a %compile-time error ; CHANGED 
-%run-time error
-%if $T$ is a parameterized type of the form $G<T_1, \ldots, T_n>$ and $G$ is not a generic type with $n$ type parameters.
-
-%Note, that, in checked mode, it is a dynamic type error if a malformed type is used in a type cast as specified in \ref{dynamicTypeSystem}.
-
-%It is a static warning if $T$ is malformed or malbounded.
-%does not denote a type available in the current lexical scope. 
+ 
 The static type of a cast expression  \code{$e$ \AS{} $T$}  is $T$. 
-%It is a static warning if if $T$ is a parameterized type of the form $G<T_1, \ldots, T_n>$ and $G$ is not a generic type with $n$ type parameters. 
 
 
 \section{Statements}
 \label{statements}
 
  \begin{grammar}
 {\bf statements:}
       statement*
     .
 
@@ skipping 350 matching lines @@
  
  \rationale{
  The prohibition on user defined equality allows us to implement the switch efficiently for user defined types. We could formulate matching in terms of identity instead with the same efficiency. However, if a type defines an equality operator, programmers would find it quite surprising that equal objects did not match.
  
  }
 
 \commentary{
 The \SWITCH{}  statement should only be used in very limited situations (e.g., interpreters or scanners).  
 }
 
-%A switch statement {\SWITCH{} ($e$)  \{ $label_{11} \ldots label_{1j_1}$ \CASE{} $e_1: s_1 \ldots$ $label_{n1} \ldots label_{nj_n}$  \CASE{} $e_n: s_n$ \}} is equivalent to switch statement \code{\SWITCH{} ($e$) \{ $label_{11} \ldots label_{1j_1}$ \CASE{}  $e_1: s_1 \ldots$ $label_{n1} \ldots label_{nj_n}$ \CASE{}  $e_n: s_n$ \DEFAULT{}: \}}
-
 Execution of a switch statement of the form \code{\SWITCH{} ($e$) \{ \CASE{} $label_{11} \ldots label_{1j_1}$ $e_1: s_1 \ldots$  \CASE{} $label_{n1} \ldots label_{nj_n}$ $e_n: s_n$ \DEFAULT{}: $s_{n+1}$ \}} or the form \code{\SWITCH{} ($e$) \{ \CASE{} $label_{11} \ldots label_{1j_1}$ $e_1: s_1 \ldots$  \CASE{} $label_{n1} \ldots label_{nj_n}$ $e_n: s_n$ \}} proceeds as follows:
 
 The statement \code{\VAR{} id = $e$;} is evaluated, where \code{id} is a variable whose name is distinct from any other variable in the program. In checked mode, it is a run time error if the value of $e$ is not an instance of the same class as the constants $e_1 \ldots e_n$. 
 
 \commentary{Note that if there are no case clauses ($n = 0$), the type of $e$ does not matter.}
 
 Next, the case clause \CASE{} $e_{1}: s_{1}$ is executed if it exists. If \CASE{} $e_{1}: s_{1}$ does not exist, then if there is a  \DEFAULT{} clause it is executed by executing $s_{n+1}$.
 
 A case clause introduces a new scope, nested in the lexically surrounding scope. The scope of a case clause ends immediately after the case clause's statement list.
 
@@ skipping 86 matching lines @@
  \item
 A set of \ON{}-\CATCH{} clauses, each of which specifies  (either explicitly or implicitly) the type of exception object to be handled, one or two exception parameters and a block statement.
 \item
 A \FINALLY{} clause, which consists of a block statement. 
 \end{enumerate}
 
 \rationale{
 The syntax is designed to be upward compatible with existing Javascript programs. The \ON{} clause can be omitted, leaving what looks like a Javascript catch clause.
 }
 
-An \ON{}-\CATCH{} clause of   the form   \code{\ON{} $T$ \CATCH{} ($p_1, p_2$) $s$}  {\em matches} an object $o$  if the type of $o$ is a subtype of $T$. 
+An \ON{}-\CATCH{} clause of   the form   \code{\ON{} $T$ \CATCH{} ($p_1, p_2$) $s$}  {\em matches} an object $o$  if the type of $o$ is a subtype of $T$.  If $T$ is a malformed type, then performing a match causes a run time error.
 
 \commentary {
 It is of course a static warning if $T$ is a malformed type (\ref{staticTypes}).
 }
 
 An \ON{}-\CATCH{} clause of the form  \code{\ON{} $T$ \CATCH{} ($p_1$) $s$} is equivalent to an \ON{}-\CATCH{} clause  \code{\ON{} $T$ \CATCH{} ($p_1, p_2$) $s$} where $p_2$ is an identifier that does not occur anywhere else in the program. 
 
 
 An \ON{}-\CATCH{} clause of the form  \code{\CATCH{} ($p$) $s$} is equivalent to an \ON{}-\CATCH{} clause  \code{\ON{} \DYNAMIC{} \CATCH{} ($p$) $s$}. An \ON{}-\CATCH{} clause of the form  \code{\CATCH{} ($p_1, p_2$) $s$} is equivalent to an \ON{}-\CATCH{} clause  \code{\ON{} \DYNAMIC{} \CATCH{} ($p_1, p_2$) $s$}
 
@@ skipping 517 matching lines @@
     .
 \end{grammar}
 
 A {\em part header} begins with  \PART{} \OF{}  followed by the name of the library the part belongs to.  A part declaration consists of a part header followed by a sequence of top-level declarations.
 
 Compiling a part directive of the form \code{\PART{} $s$;} causes the Dart system to attempt to compile the contents of the URI that is the value of $s$. The top-level declarations at that URI are then compiled by the Dart compiler in the scope of the current library. It is a compile-time error if the contents of the URI are not a valid part declaration. It is a static warning if the referenced part declaration $p$ names a library other than the current library as the library to which $p$ belongs.
 
 \subsection{Scripts}
 \label{scripts}
 
-A {\em script} is a library with a top-level function \code{main()}. 
+A {\em script} is a library whose exported namespace  (\ref{exports}) includes a top-level function \code{main()}. 
 A script $S$ may be executed as follows:
 
-First, $S$ is compiled as a library as specified above. Then, the top-level function \code{main()} that is in scope in $S$ is invoked with no arguments. It is a run time error if $S$ does not declare or import a top-level function \code{main()}.
+First, $S$ is compiled as a library as specified above. Then, the top-level function \code{main()} that is in the exported namespace of $S$ is invoked with no arguments. It is a run time error if $S$ does not declare or import a top-level function \code{main()}.
 
 \rationale{
 The names of scripts are optional, in the interests of interactive, informal use. However, any script of long term value should be given a name as a matter of good practice. 
 }
 
+\commentary {
+A Dart program will typically be executed by executing a script.
+}
+
 \subsection{URIs}
 \label{uris}
 
 URIs are specified by means of string literals:
 
 \begin{grammar}
 {\bf uri:}
       stringLiteral
     .
 \end{grammar}
@@ skipping 70 matching lines @@
 \item $T$ has the form $id$ or the form $prefix.id$, and in the enclosing lexical scope, the name $id$ (respectively $prefix.id$) does not denote a type.
 \item $T$ denotes a type variable in the enclosing lexical scope, but occurs in the signature or body of a static member.
 \item $T$ is a parameterized type of the form $G<S_1, \ldots , S_n>$, and  $G$ is malformed. 
 \item $T$ denotes declarations that were imported from multiple imports clauses.
 %Either $G$ or $S_i,  i \in 1.. n$ are malformed. 
  % \item  $G$ is not a generic type with $n$ type parameters.
 %  \item Let $T_i$ be the type parameters of $G$ (if any) and let $B_i$ be the bound of $T_i,  i \in 1.. n$, and $S_i$ is not a subtype of $[S_1,  \ldots, S_n/T_1, \ldots, T_n]B_i,   i \in 1.. n$. 
 %  \end{itemize}
 \end{itemize}
 
- Any use of a malformed  type gives rise to a static warning. A malformed type is then interpreted as \DYNAMIC{} by the static type checker and the runtime.
- 
+ Any use of a malformed  type gives rise to a static warning. A malformed type is then interpreted as \DYNAMIC{} by the static type checker and the runtime unless explicitly specified otherwise.
+  
  \rationale{
 This ensures that the developer is spared a series of cascading warnings as the malformed type interacts with other types.
 }
 
+
 \subsubsection{Type Promotion}
 \label{typePromotion}
 
 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. 
 
 We say that a variable $v$ is known to have type $T$ whenever we allow the type of $v$ to be promoted. The exact circumstances when type promotion is allowed are given in the relevant sections of the specification (\ref{logicalBooleanExpressions}, \ref{conditional} and \ref{if}).
 
 Type promotion for a variable $v$ is allowed only when we can deduce that such promotion is valid based on an analysis of certain boolean expressions. In such cases, we say that the boolean expression $b$ shows that $v$ has type $T$. As a rule, for all variables $v$ and types $T$, a boolean expression does not show that $v$ has type $T$. Those situations where an expression does show that a variable has a type are mentioned explicitly in the relevant sections of this specification (\ref{typeTest} and \ref{logicalBooleanExpressions}).
 
 
 \subsection{Dynamic Type System}
 \label{dynamicTypeSystem}
 
 A Dart implementation must support execution in both {\em production mode} and {\em checked mode}.  Those dynamic checks specified as occurring specifically in checked mode must be performed iff the code is executed in checked mode.
 
 %It is a run-time type error to access an undeclared type outside .
 
 %It is a dynamic type error if a malformed type is used in a subtype test.  
-In checked mode, it is a dynamic type error if  a malbounded (\ref{parameterizedTypes}) 
+In checked mode, it is a dynamic type error if a malformed or malbounded (\ref{parameterizedTypes}) 
 type is used in a subtype test.  
 
 %In production mode, an undeclared type is treated as an instance of type \DYNAMIC{}. 
 
 \commentary{Consider the following program}
 
 \begin{dartCode}
 \TYPEDEF{} F(bool x);
 f(foo x) $=>$ x;
 main() \{
@@ skipping 11 matching lines @@
 
 \begin{dartCode}
 \VAR{} i;
 i  j; //  a variable j of type i (supposedly)
 main() \{
      j =  'I am not an i'; 
 \}
 \end{dartCode}
 
 \commentary{
-Since $i$ is not a type, a static warning will be issue at the declaration of $j$. However, the program can be executed without incident.  The undeclared type $i$ is treated as \DYNAMIC{}, so even in checked mode, the implicit subtype test at the assignment  succeeds.
+Since $i$ is not a type, a static warning will be issue at the declaration of $j$. However, the program can be executed without incident in production mode because he undeclared type $i$ is treated as \DYNAMIC{}. However, in checked mode, the implicit subtype test at the assignment will trigger an error at runtime.

[Johnni Winther, 2013/11/04 12:34:49]

'because he undeclared' -> 'because the undeclared'.

 }
 
-\rationale{
-We have chosen to treat malformed types  as type \DYNAMIC{}. Earlier versions of this specification did so in some cases but not in others. We found the rules to be too complex, and have opted to harmonize the specification. Given that a static warning is issued, there is no need for the runtime to deal with extra complexity by treating malformed types specially.
-
-
-%as is done in production mode. After all, a static warning has already been given. That is a legitimate design option, and it is ultimately a judgement call as to whether checked mode should be more or less aggressive in dealing with such a situation.
-
-%Likewise, we could opt to ignore malformed types entirely in checked mode.
-
-%For now, we have opted to treat a malformed type as an error type that has no subtypes or supertypes, and which causes a runtime error when tested against any other type.
-}
 
 \commentary{
 Here is an example involving malbounded types:
 }
 
 \begin{dartCode}
 \CLASS{} I$<$T \EXTENDS{} num$>$ \{\}
 \CLASS{} J \{\}
 
 \CLASS{} A$<$T$>$ \IMPLEMENTS{} J,  I$<$T$>$ // type warning: T is not a subtype of num
@@ skipping 498 matching lines @@
 \item The names of compile time constant variables never use lower case letters. If they consist of multiple words, those words are separated by underscores. Examples: PI,  I\_AM\_A\_CONSTANT.
 \item The names of functions (including getters, setters, methods and local or library functions) and non-constant variables begin with a lowercase letter. If the name consists of multiple words, each  word (except the first) begins with an uppercase letter.  No other uppercase letters are used. Examples: camlCase, dart4TheWorld
 \item The names of types (including classes and type aliases) begin with an upper case letter.  If the name consists of multiple words, each  word  begins with an uppercase letter.  No other uppercase letters are used. Examples: CamlCase, Dart4TheWorld.
 \item The names of type variables are short (preferably single letter). Examples: T, S, K, V , E.
 \item The names of libraries or library prefixes never use upper case letters. If they consist of multiple words, those words are separated by underscores. Example: my\_favorite\_library.
 \end{itemize}
 }
 
 
 \end{document}