Proposed spec for DEP for assert with messages.

docs/language/dartLangSpec.tex

Index: docs/language/dartLangSpec.tex
diff --git a/docs/language/dartLangSpec.tex b/docs/language/dartLangSpec.tex
index 3850f200dfcfc00dea26f2a7b80fdf71a2c7f3a8..7271f8cb7898c199a411f12dd7ee898890226826 100644
--- a/docs/language/dartLangSpec.tex
+++ b/docs/language/dartLangSpec.tex
@@ -7,8 +7,7 @@
 \usepackage{lmodern}
 \newcommand{\code}[1]{{\sf #1}}
 \title{Dart Programming Language  Specification  \\
-(4th edition draft)\\
-{\large Version 1.11}}
+{\large Version 1.13}}
 
 % For information about Location Markers (and in particular the
 % commands \LMHash and \LMLabel), see the long comment at the
@@ -3874,7 +3873,7 @@ Let $T$ be the  static type of $o$. It is a static type warning if $T$ does not
 \item
 $T$ or a superinterface of $T$ is annotated with an annotation denoting a constant identical to the constant \code{@proxy} defined in \code{dart:core}.  Or
 \item  $T$ is \code{Type}, $e$ is a constant type literal and the class corresponding to $e$ has a static getter named $m$.
-\item $T$ is \code{Function} and $m$ is \CALL. \rationale {The type \code{Function} is treated as if it has a \code{call} method for any possible signature of \CALL. The expectation is that any concrete subclass of \code{Function} will implement \CALL. Note that a warning will be issue if this is not the case. Furthermore, any use of \CALL{} on a subclass of \code{Function} that fails to implement \CALL{} will also provoke a a warning, as this exemption is limited to type \code{Function}, and does not apply to its subtypes. 
+\item $T$ is \code{Function} and $m$ is \CALL. \rationale {The type \code{Function} is treated as if it has a \code{call} method for any possible signature of \CALL. The expectation is that any concrete subclass of \code{Function} will implement \CALL. Note that a warning will be issue if this is not the case. Furthermore, any use of \CALL{} on a subclass of \code{Function} that fails to implement \CALL{} will also provoke a warning, as this exemption is limited to type \code{Function}, and does not apply to its subtypes. 
 }
 \end{itemize}
 
@@ -6457,24 +6456,38 @@ An {\em assert statement} is used to disrupt normal execution if a given boolean
 
 \begin{grammar}
 {\bf assertStatement:}
-   assert `(' conditionalExpression `)' `{\escapegrammar ;}'
+   assert `(' conditionalExpression (`,' expression)?  `)' `{\escapegrammar ;}'
       .
 \end{grammar}
       
 \LMHash{}
-The assert statement has no effect in production mode. In checked mode, execution of an assert statement \code{\ASSERT{}($e$);} proceeds as follows:
+The assert statement has no effect in production mode. In checked mode, execution of an assert statement \code{\ASSERT{}($e$);} or \code{\ASSERT{}($e$, $s$);} proceeds as follows:
 
 \LMHash{}
 The conditional expression $e$ is evaluated to an object $o$. If the class of $o$ is a subtype of \code{Function} then let $r$ be the result of invoking $o$ with no arguments. Otherwise, let $r$ be $o$. 
-It is a dynamic type error if $o$ is not of type \code{bool} or of type \code{Function}, or if $r$ is not of type \code{bool}.  If $r$ is \FALSE{}, we say that the assertion failed. If $r$ is \TRUE{}, we say that the assertion succeeded. If the assertion succeeded, execution of the assert statement is complete. If the assertion failed, an \code{AssertionError} is thrown.
+It is a dynamic type error if $o$ is not of type \code{bool} or of type \code{Function}, or if $r$ is not of type \code{bool}.  If $r$ is \FALSE{}, we say that the assertion failed. If $r$ is \TRUE{}, we say that the assertion succeeded. If the assertion succeeded, execution of the assert statement is complete. 
+
+\LMHash{}
+If the assertion failed, and the assertion is of the form \code{\ASSERT{}($e$);} an \cd{AssertionError} is thrown.
+
+If the assertion failed and the assertion is of the form \code{\ASSERT{}($e$, $s$);} then the expression $s$ is evaluated to a value $o_s$. If evaluation of $s$ fails, an \cd{AssertionError} is thrown. Otherwise, the \cd{toString()} method is invoked on $o_s$ resulting in a string object $m$. If the invocation of \cd{toString()} throws an exception, an \cd{AssertionError} is thrown. Otherwise, 

[Lasse Reichstein Nielsen, 2015/11/05 16:22:25]

Calling o_s.toString is not guaranteed to result in a String object. Even in
checked mode, toString can be overwritten to return a non-string.
We need to handle this somehow, perhaps by considering it a failure, or by
allowing the non-string to end up in the AssertionError.

[Brian Wilkerson, 2015/11/05 17:04:37]

True. We have the same problem for string interpolation. I don't see any
discussion in the spec about what we do in that case. The VM handles this by
throwing an exception of type ArgumentError. Perhaps we should just do the same
here.

[Bob Nystrom, 2015/11/05 17:50:04]

       fails, an \cd{AssertionError} is thrown.

I don't think we should mask the original error here. If the message fails to
evaluate, that's a more significant error than my invariant failing. I want to
know that error *first* so I can fix it. Then I'll get back to fixing my
invariant failing.

If we throw an AssertionError then it will guide users down the wrong path. They
will spend their time figuring out why the assertion invariant is failing (which
is certainly an issue). If they fix that *first* then the error will go away
completely before they get a chance to fix the message failure.

I think the right thing to do is just let the original error propagate.
      is invoked on $o_s$ resulting in a string object $m$.

I don't think shouldn't be done here. Instead, just store the original message
object—whatever its type—in the AssertionError object. When the AssertionError
is printed, *then* that will stringify it.

[gbracha, 2015/11/05 19:25:01]

Interestingly, the original spec would ensure that behavior, but people argued
the opposite. If there is a clear consensus, I'm happy to change it. 
This amounts to leaving the semantics to the AssertionError class. It will have
to decide how to print the object (and it should use that object's toString
anyway). And it will decide how to catch any error in toString including whether
it returned a string or not. I don't see any advantage to that. We might as well
decide that behavior here.

[Paul Berry, 2015/11/05 19:35:26]

Personally, I feel the opposite way.  I use assert to verify design invariants
which may be relied upon by other code, possibly including code inside the
implementation of toString().  So if one of my assertions fires, that means that
some invariant has been invalidated, and that *may* cause toString() to fail
(but usually won't).  If violating an invariant causes toString() to fail, I
don't consider that a bug in toString().

So to me, when an invariant is violated, the most important thing is that I want
to be pointed to the line of code where the violation was discovered.  Second
priority is to get my custom assertion message, since that will help me in
debugging.  But if the custom assertion message can't be computed due to an
exception, I don't want to have to go "fix" toString() to harden it against all
possible invariant violations.  I just want to be pointed to the failing assert
statement so I can fix it and get on with my life.

[floitsch, 2015/11/18 21:16:36]

Late to the party...
I'm not going to make this easier, but I think this is too complicated.
Imho asserts should be simple:
if (!assert-condition) throw new AssertionError(s);

Except that I don't want to force a specific assertion-error constructor.
Basically, I want the VM/dart2js to have the most flexibility in how it
constructs the assertion error.
It would be considered good practice to have `s` as `reason` field in the
AssertionError, but I don't think that needs to be specified in the language
spec.

I don't think that we should do a toString here. The AssertionError can do that
it its own 'toString' method. (most likely using a 'safeToString').

Something like:
===
If the assertion failed and the assertion is of the form \code{\ASSERT{}($e$,
$r$);} then the expression $r$ is evaluated to a value $o$. If the evaluation of
$o$ succeeds (i.e. no exception), then an \cd{AssertionError} with $o$ as reason
is thrown.

\commentary{
The definition above implies that $r$ is not evaluated if the assertion
succeeded.

The definition above does not specify how the AssertionError is constructed.
This gives embedders the freedom to store more helpful information in the thrown
instance.
===

[gbracha, 2015/11/24 20:26:04]

So we are going around in circles. The original specification was given terms of
calling a constructor. It ensures consistent semantics and a minimum of
implementation effort, since everything is done in terms of existing mechanism. 
After endless discussion, it boils down to exactly that except that you don't
want to commit to having a constructor in the library.

As for toString, the whole purpose of it is to allow people to customize how an
object appears. They don't want some generic description generated by the
system. 

Of course, it  is all a tempest in a teapot, because in reality s will be a
string and it would be better to statically check that, but we've given up on
that. I think we should leave it as is at this point and get on with our lives.

+an \cd{AssertionError} $x$ is created with error message $m$.

[Lasse Reichstein Nielsen, 2015/11/05 16:22:25]

Maybe if evaluation of $s$ fails, we should let the object $o_s$ be the object
thrown by the failed evaluation. That way it isn't lost, and the user has a
chance to figure out why the message is wrong.

Likewise, if $o_s.toString()$ fails, let $m$ be a string derived from the thrown
object (don't specify that too much, then we can use safeToString).

[gbracha, 2015/11/05 19:25:01]

So if we go back to propagating failures in message evaluation, why not specify
that we do a throw(new AssertionError(s)) and be done?

+ 
+\rationale {
+The optional argument $s$ is intended to allow a suitable message to be associated with the assertion. An implementation should endeavor to display the message $m$ in a manner that is useful to the developer.
+}
+
+\commentary{
+The definition above implies  that $s$ is not evaluated if the assertion succeeded.
+}
 
 %\Q{Might be cleaner to define it as \code{if (!$e$) \{\THROW{} \NEW{} AssertionError();\}} (in checked mode only).
 %What about an error message as part of the assert?}
 
 \LMHash{}
- It is a static type warning if the type of $e$ may not be assigned to either  \code{bool} or $() \rightarrow$ \code{bool}.  
+ 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).  It cannot be viewed as a function call that is being optimized away because the argument might have side effects.
+\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. And lastly, the optional message would have to be evaluated in all cases if \ASSERT{} were a function.
 }
 
 %If a lexically visible declaration named \code{assert} is in scope, an assert statement 
@@ -7321,7 +7334,7 @@ A function type $(T_1, \ldots T_n, \{T_{x_1}$ $x_1, \ldots, T_{x_k}$ $x_k\}) \ri
 \item $\forall i \in 1 .. n, T_i \Longleftrightarrow S_i$.
 \item $k \ge m$ and $y_i \in \{x_1,  \ldots, x_k\}, i \in 1 .. m$.
 %\{x_1,  \ldots, x_k\}$ is a superset of $\{y_1,  \ldots, y_m\}$.
-\item For all $y_i \in \{y_1,  \ldots, y_m\}, y_i = x_j \Rightarrow T_j \Longleftrightarrow S_i$
+\item For all $y_i \in \{y_1,  \ldots, y_m\}, y_i = x_j \Rightarrow T_{x_j} \Longleftrightarrow S_{y_i}$
 \end{enumerate}
 
 %In addition, a function type $(T_1, \ldots, Tn, [T_{n+1} x_{n+1}, \ldots, T_{n+k} x_{n+k}]) \rightarrow T$ is a subtype of the function type $(T_1, \ldots, T_n, T_{n+1} , [T_{n+2} x_{n+2}, \ldots, T_{n+k} x_{n+k}]) \rightarrow T$.