Update spec to 0.7. Remove obsolete/redundant rules for local variable initialization.

docs/language/dartLangSpec.tex

Index: docs/language/dartLangSpec.tex
===================================================================
--- docs/language/dartLangSpec.tex	(revision 28540)
+++ docs/language/dartLangSpec.tex	(working copy)
@@ -5,7 +5,7 @@
 \usepackage{hyperref}
 \newcommand{\code}[1]{{\sf #1}}
 \title{Dart Programming Language  Specification \\
-{\large Draft Version 0.61}}
+{\large Draft Version 0.70}}
 \author{The Dart Team}
 \begin{document}
 \maketitle
@@ -485,6 +485,8 @@
 
 \ref{strings}: Allow adjacent single and multiline strings to concatenate. Allow escaped newlines in multiline strings.
 
+\ref{const}: Allow parameterized types in const instance creation.
+
 \ref{conditional}: Type promotion support added.
 
 \ref{logicalBooleanExpressions}: Type promotion support added.
@@ -497,6 +499,8 @@
 
 \ref{if}: Type promotion support added.
 
+\ref{try}: \ON{} with no \CATCH{} implies \DYNAMIC{}, not \cd{Object}.
+
 \ref{return}: Added warning if \RETURN{} without expression mixed with \RETURN{} with an expression.
 
 \ref{exports}: Ensure that exports treat \code{dart:} libs specially, like imports do.
@@ -3212,8 +3216,12 @@
 .
 \end{grammar}
 
-Let $e$ be a constant object expression of the form  \CONST{} $T.id(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ or the form  \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$ is not a class accessible in the current scope.  It is a compile-time error if $T$ is a parameterized type.
+Let $e$ be a constant object expression of the form  \CONST{} $T.id(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ or the form  \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. 
 
+\commentary{In particular, $T$ may not be a type variable.}
+
+If $T$ is a parameterized type, it is a compile-time error if $T$ includes a type variable among its type arguments.
+
 If $e$ is of the form \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 $T.id$ is not the name of a constant constructor declared by the type $T$. If $e$ is of the form  \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$. 
 
 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.
@@ -3846,7 +3854,7 @@
 If all of the following hold:
 \begin{itemize}
 \item $e_1$ shows that a variable $v$ has type $T$.
-\item $v$ is not potentially mutated in either $e_1$, $e_2$ or within a closure.
+\item $v$ is not potentially mutated in $e_2$ or within a closure.
 \item If the variable $v$ is accessed by a closure in $e_2$ then the variable $v$ is not potentially mutated anywhere in the scope of $v$.
 \end{itemize}
 
@@ -3884,7 +3892,7 @@
 \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 either $e_1$ or $e_2$ or within a closure.
+\item The variable $v$ is not mutated in $e_2$ or within a closure.
 \end{itemize}
 
 Furthermore, if all of the following hold:
@@ -4301,7 +4309,7 @@
 
 \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 a subtype of any other type $S$ such that $v$ is known to have type $S$. 
+\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 static method, top-level function or local function the static type of $e$ the function type defined by $d$.
 \item If $d$ is the declaration of a static variable or static getter declared in class $C$, the static type of $e$ the static type of the getter invocation (\ref{getterInvocation}) $C.id$. 
 \item If $d$ is the declaration of a library variable or top-level getter, the static type of $e$  is the static type of the getter invocation $id$. 
@@ -4352,8 +4360,18 @@
 %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{}$.
+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).

[Johnni Winther, 2013/10/14 07:23:34]

It is not only weaker (less specific) types that leads to multiple types being
associated with a variable. Unrelated types also introduce it:

class I {}
class J {}

Object o = ...
if (o is I && o is J) {
  // o should now be known to have both type I and J.
}

+
+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. 
 
@@ -4497,34 +4515,7 @@
  %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.
 %}
 
-%In all of the above cases,  it 
-It is a compile-time error if $e$ refers to the name $v$ or the name $v=$.
 
-\commentary{
-This rule may seem redundant in light of the scoping rules above. After all:
-}
-
-\begin{dartCode}
-f() \{ // a top level function
-  \VAR{} v = v* 2;
-\}
-\end{dartCode}
-
-\commentary{
-is already an error since $v$ is not yet in scope in its own initializer. However, consider the more insidious:
-}
-
-\begin{dartCode}
-\VAR v = 0; // top level variable
-
-f() \{ // a top level function
-  \VAR{} v = v* 2; // compile-time error
-\}
-\end{dartCode}
-
-
-
-
 \subsection{Local Function Declaration}
 
 \label{localFunctionDeclaration}
@@ -4620,7 +4611,7 @@
 If:
 \begin{itemize}
 \item  $b$ shows that a variable $v$ has type $T$.
-\item  $v$ is not potentially mutated in either $b$, $s_1$ or within a closure.
+\item  $v$ is not potentially mutated in $s_1$ or within a closure.
 \item If the variable $v$ is accessed by a closure in $s_1$ then the variable $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$.  
@@ -4908,7 +4899,7 @@
 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{} Object \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{} Object \CATCH{} ($p_1, p_2$) $s$}
+An \ON{}-\CATCH{} clause of the form  \code{\CATCH{} ($p$) $s$} is equivalent to an \ON{}-\CATCH{} clause  \code{\ON{} \DYNAMIC{} \CATCH{} ($p$) $s$}. An \ON{}-\CATCH{} clause of the form  \code{\CATCH{} ($p_1, p_2$) $s$} is equivalent to an \ON{}-\CATCH{} clause  \code{\ON{} \DYNAMIC{} \CATCH{} ($p_1, p_2$) $s$}
 
 
 %If an explicit type is associated with of $p_2$, it is a static warning if that type is not \code{Object} or \DYNAMIC{}.
@@ -5116,7 +5107,7 @@
 
  It is a static type warning if the type of $e$ may not be assigned to either  \code{bool} or $() \rightarrow$ \code{bool}.  
 
-\rationale{Why is this a statement, not a built in function call? Because it is handled magically so it has no effect and no overhead in production mode. Also, in the absence of final methods. one could not prevent it being overridden (though there is no real harm in that). Overall, perhaps it could be defined as a function, and the overhead issue could be viewed as an optimization.
+\rationale{Why is this a statement, not a built in function call? Because it is handled magically so it has no effect and no overhead in production mode. Also, in the absence of final methods. one could not prevent it being overridden (though there is no real harm in that).  It cannot be viewed as a function call that is being optimized away because the argument might have side effects.
 }
 
 %If a lexically visible declaration named \code{assert} is in scope, an assert statement 
@@ -5394,7 +5385,7 @@
 For each
 entry mapping key $k$ to declaration $d$ in $NS_n$ an entry mapping $k$ to $d$ is added to the exported namespace of $L$ unless a  top-level declaration with the name $k$ exists in $L$.  
 
-If a name $N$ is referenced by a library $L$ and $N$ would be introduced into the exported namespace of $L$ by an export from a library whose URI begins with \code{dart:} and an export from a library whose name does not begin with \code{dart:}:
+If a name $N$ is referenced by a library $L$ and $N$ would be introduced into the exported namespace of $L$ by an export from a library whose URI begins with \code{dart:} and an export from a library whose URI does not begin with \code{dart:}:
 \begin{itemize}
 \item The export from \code{dart:} is implicitly extended by a \code{\HIDE{} $N$} clause.
 \item A static warning is issued.
@@ -5723,6 +5714,7 @@
 \item $T$ is of the form $I<T_1, \ldots, T_n>$ and $S$ is of the form $I<S_1, \ldots, S_n>$ and:
 $T_i << S_i, 1 \le i \le n$
 \item $T$ and $S$ are both function types, and $T << S$ under the rules of section \ref{functionTypes}.
+\item $T$ is a function type and $S$ is \cd{Function}.
 \item $T << U$ and $U << S$.
 \end{itemize}
 
@@ -5938,7 +5930,7 @@
 
 Let $T$ be a parameterized type  $G<S_1,  \ldots, S_n>$. If $G$ is not a generic type, the type arguments $S_i$, $1 \le i \le n$ are discarded. If $G$ has $m \ne n$ type parameters, $T$ is treated as as a parameterized type with $m$ arguments, all of which are \DYNAMIC{}. 
 
-\commentary{In short, any arity mismatch results in all type arguments being dropped, and replaced with the correct number of type arguments, all set to \DYNAMIC{}. Of course, a static warning will be issued. This behavior is not yet implemented.
+\commentary{In short, any arity mismatch results in all type arguments being dropped, and replaced with the correct number of type arguments, all set to \DYNAMIC{}. Of course, a static warning will be issued. 
 }
 
 Otherwise, let