Conditional expression; operators && and ||; if statements; delete old section about promotion

Author: eernstg

specification/dartLangSpec.tex

@@ -16166,7 +16166,7 @@ \subsection{Conditional}
 \LMLabel{conditional}
 
 \LMHash{}%
-A \Index{conditional expression} evaluates one of two expressions
+A \Index{conditional expression} evaluates one of two expressions,
 based on a boolean condition.
 
 \begin{grammar}
@@ -16175,34 +16175,23 @@ \subsection{Conditional}
 \end{grammar}
 
 \LMHash{}%
-Evaluation of a conditional expression $c$ of the form $e_1 ? e_2 : e_3$
-proceeds as follows:
+Consider a conditional expression $c$ of the form
+\code{$e_1$\,\,?\,\,$e_2$\,\,:\,\,$e_3$}.
+It is a \Error{compile-time error} if
+the static type of $e_1$ may not be assigned to \code{bool}.
+The static type of $c$ is the least upper bound (\ref{leastUpperBounds}) of
+the static type of $e_2$ and the static type of $e_3$.
 
 \LMHash{}%
-First, $e_1$ is evaluated to an object $o_1$.
+Evaluation of a conditional expression $c$ of the form
+\code{$e_1$\,\,?\,\,$e_2$\,\,:\,\,$e_3$}
+proceeds as follows:
+Evaluate $e_1$ to an object $o_1$.
 % This error can occur due to an implicit cast from \DYNAMIC.
 It is a dynamic error if the run-time type of $o_1$ is not \code{bool}.
-If $r$ is \TRUE, then the value of $c$ is
+If $o_1$ is the \TRUE{} object, then the value of $c$ is
 the result of evaluating the expression $e_2$.
-Otherwise the value of $c$ is the result of evaluating the expression $e_3$.
-
-\LMHash{}%
-If $e_1$ shows that a local variable $v$ has type $T$,
-then the type of $v$ is known to be $T$ in $e_2$,
-unless any of the following are true:
-\begin{itemize}
-\item $v$ is potentially mutated in $e_2$,
-\item $v$ is potentially mutated within a function other
-  than the one where $v$ is declared, or
-\item $v$ is accessed by a function defined in $e_2$ and
-  $v$ is potentially mutated anywhere in the scope of $v$.
-\end{itemize}
-
-\LMHash{}%
-It is a \Error{compile-time error} if
-the static type of $e_1$ may not be assigned to \code{bool}.
-The static type of $c$ is the least upper bound (\ref{leastUpperBounds}) of
-the static type of $e_2$ and the static type of $e_3$.
+Otherwise, the value of $c$ is the result of evaluating the expression $e_3$.
 
 
 \subsection{If-null Expressions}
@@ -16257,8 +16246,15 @@ \subsection{Logical Boolean Expressions}
 an expression $e_1$ with argument $e_2$.
 
 \LMHash{}%
-Evaluation of a logical boolean expression $b$ of the form $e_1 || e_2$ causes
-the evaluation of $e_1$ to an object $o_1$.
+It is a \Error{compile-time error} if
+the static type of $e_1$ may not be assigned to \code{bool}
+or if the static type of $e_2$ may not be assigned to \code{bool}.
+The static type of a logical boolean expression is \code{bool}.
+
+\LMHash{}%
+Evaluation of a logical boolean expression $b$ of the form
+\code{$e_1$\,\,||\,\,$e_2$}
+causes the evaluation of $e_1$ to an object $o_1$.
 % This error can occur due to an implicit downcast from \DYNAMIC.
 It is a dynamic error if the run-time type of $o_1$ is not \code{bool}.
 If $o_1$ is \TRUE, the result of evaluating $b$ is \TRUE,
@@ -16268,8 +16264,9 @@ \subsection{Logical Boolean Expressions}
 Otherwise the result of evaluating $b$ is $o_2$.
 
 \LMHash{}%
-Evaluation of a logical boolean expression $b$ of the form $e_1 \&\& e_2$
-causes the evaluation of $e_1$ producing an object $o_1$.
+Evaluation of a logical boolean expression $b$ of the form
+\code{$e_1$\,\,\&\&\,\,$e_2$}
+causes the evaluation of $e_1$ to an object $o_1$.
 % This error can occur due to an implicit downcast from \DYNAMIC.
 It is a dynamic error if the run-time type of $o_1$ is not \code{bool}.
 If $o_1$ is \FALSE, the result of evaluating $b$ is \FALSE,
@@ -16278,45 +16275,6 @@ \subsection{Logical Boolean Expressions}
 It is a dynamic error if the run-time type of $o_2$ is not \code{bool}.
 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 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 not mutated in $e_2$ or within a function
-  other than the one where $v$ is declared.
-\end{itemize}
-
-\LMHash{}%
-If $e_1$ shows that a local variable $v$ has type $T$,
-then the type of $v$ is known to be $T$ in $e_2$,
-unless any of the following are true:
-\begin{itemize}
-%% The first item here is unnecessary for soundness,
-%% and is retained mainly for backwards compatibility.
-%% If $e_1$ shows that $v$ has type $T$, then any assignment
-%% in $e_1$ does not invalidate that.
-%% Removing the line is visible in the semantics, though, because:
-%%  num x;
-%%  (x ??= 42) != null && x is int & x.toRadixString(16) != ""
-%% is allowed without the line, and disallowed with.
-%% At time of writing, the analyzer disallows the code.
-\item $v$ is potentially mutated in $e_1$,
-\item $v$ is potentially mutated in $e_2$,
-\item $v$ is potentially mutated within a function other
-  than the one where $v$ is declared, or
-\item $v$ is accessed by a function defined in $e_2$ and
-  $v$ is potentially mutated anywhere in the scope of $v$.
-\end{itemize}
-
-\LMHash{}%
-It is a \Error{compile-time error} if
-the static type of $e_1$ may not be assigned to \code{bool}
-or if the static type of $e_2$ may not be assigned to \code{bool}.
-The static type of a logical boolean expression is \code{bool}.
-
 
 \subsection{Equality}
 \LMLabel{equality}
@@ -18251,37 +18209,41 @@ \subsection{If}
 \LMLabel{if}
 
 \LMHash{}%
-The \Index{if statement} allows for conditional execution of statements.
+The \Index{\IF{} statement} allows for conditional execution of statements.
 
 \begin{grammar}
 <ifStatement> ::= \IF{} `(' <expression> `)' <statement> (\ELSE{} <statement>)?
 \end{grammar}
 
 \LMHash{}%
-An if statement of the form
-\code{\IF{} ($e$) $s_1$ \ELSE{} $s_2$}
-where $s_1$ is not a block statement is equivalent to the statement
-\code{\IF{} ($e$) \{$s_1$\} \ELSE{} $s_2$}.
-An if statement of the form
-\code{\IF{} ($e$) $s_1$ \ELSE{} $s_2$}
-where $s_2$ is not a block statement is equivalent to the statement
-\code{\IF{} ($e$) $s_1$ \ELSE{} \{$s_2$\}}.
+An \IF{} statement of the form
+\code{\IF\,\,($e$)\,\,$S$}
+is treated as
+(\ref{overview})
+\code{\IF\,\,($e$)\,\,$S$\,\,\ELSE\,\,\{\}}.
+An \IF{} statement of the form
+\code{\IF\,\,($e$)\,\,$S_1$\,\,\ELSE\,\,$S_2$}
+where $S_1$ is not a block statement is treated as
+\code{\IF\,\,($e$)\,\,\{\,$S_1$\,\}\,\,\ELSE\,\,$S_2$}.
+An \IF{} statement of the form
+\code{\IF\,\,($e$)\,\,$S_1$\,\,\ELSE\,\,$S_2$}
+where $S_2$ is not a block statement is treated as
+\code{\IF\,\,($e$)\,\,$S_1$\,\,\ELSE\,\,\{\,$S_2$\,\}}.
 
 \rationale{%
 The reason for this equivalence is to catch errors such as%
 }
 
 \begin{dartCode}
 \VOID{} main() \{
-  \IF{} (somePredicate)
-    \VAR{} v = 2;
+  \IF{} (somePredicate) \VAR{} v = 2;
   print(v);
 \}
 \end{dartCode}
 
 \rationale{%
 Under reasonable scope rules such code is problematic.
-If we assume that \code{v} is declared
+If we specify that \code{v} is declared
 in the scope of the method \code{main()},
 then when \code{somePredicate} evaluates to the \FALSE{} object,
 \code{v} will be uninitialized when accessed.
@@ -18300,37 +18262,21 @@ \subsection{If}
 }
 
 \LMHash{}%
-Execution of an if statement of the form
-\code{\IF{} ($b$) $s_1$ \ELSE{} $s_2$}
-where $s_1$ and $s_2$ are block statements,
-proceeds as follows:
+Consider an \IF{} statement of any of the forms mentioned above
+(\commentary{the statement then starts with \code{\IF\,\,($e$)}}).
+It is a \Error{compile-time error} if the type of the expression $e$
+is not assignable to \code{bool}.
 
 \LMHash{}%
-First, the expression $b$ is evaluated to an object $o$.
+Execution of an \IF{} statement of the form
+\code{\IF\,\,($e$)\,\,$S_1$\,\,\ELSE\,\,$S_2$}
+where $S_1$ and $S_2$ are block statements
+proceeds as follows:
+Evaluate the expression $e$ to an object $o$.
 % This error can occur due to an implicit downcast from \DYNAMIC.
 It is a dynamic error if the run-time type of $o$ is not \code{bool}.
-If $o$ is \TRUE, then the block statement $s_1$ is executed,
-otherwise the block statement $s_2$ is executed.
-
-\LMHash{}%
-It is a \Error{compile-time error} if the type of the expression $b$
-may not be assigned to \code{bool}.
-
-\LMHash{}%
-If $b$ shows that a local variable $v$ has type $T$,
-then the type of $v$ is known to be $T$ in $s_1$,
-unless any of the following are true
-\begin{itemize}
-\item $v$ is potentially mutated in $s_1$,
-\item $v$ is potentially mutated within a function other
-  than the one where $v$ is declared, or
-\item $v$ is accessed by a function defined in $s_1$ and
-  $v$ is potentially mutated anywhere in the scope of $v$.
-\end{itemize}
-
-\LMHash{}%
-An if statement of the form \code{\IF{} ($e$) $s$} is equivalent to
-the if statement \code{\IF{} ($e$) $s$ \ELSE{} \{\}}.
+If $o$ is \TRUE, then execute the block statement $S_1$,
+otherwise execute the block statement $S_2$.
 
 
 \subsection{For}
@@ -21166,34 +21112,6 @@ \subsection{Static Types}
 % objects in constructor args - these cannot represent parameterized types.
 
 
-\subsubsection{Local Variable Type Promotion}
-\LMLabel{typePromotion}
-
-\LMHash{}%
-The static type system ascribes a static type to every expression.
-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.
-The exact circumstances when type promotion is allowed are given in
-the relevant sections of the specification
-(\ref{logicalBooleanExpressions}, \ref{conditional} and \ref{if}).
-
-\LMHash{}%
-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}
 \LMLabel{dynamicTypeSystem}