[go: nahoru, domu]

Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Specify null safety #2605

Open
wants to merge 81 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
81 commits
Select commit Hold shift + click to select a range
d0811cc
Rebasing
eernstg Oct 7, 2021
ae53185
Typos: Escaping braces meant to be code
eernstg Oct 8, 2021
f3d8507
Eliminated text about migration features, adapted the remaining text …
eernstg Oct 8, 2021
bff6027
Rebasing
eernstg Oct 13, 2021
92fc551
Reorganized material on null/Null
eernstg Oct 14, 2021
8ccded9
Rebase
eernstg Oct 18, 2021
3987b3d
Rebasing
eernstg Oct 27, 2021
c98f437
Rebase
eernstg Nov 1, 2021
ed58b61
WIP
eernstg Nov 9, 2021
c111ceb
Corrected last part of section Variables
eernstg Nov 10, 2021
dfd590e
Did expression typing, spread element, i2b
eernstg Nov 11, 2021
75e7023
Super-bounded types, least and greatest closure
eernstg Nov 12, 2021
5575f29
Assignability, generics
eernstg Nov 12, 2021
53a9967
Extreme types
eernstg Nov 12, 2021
e6cdb97
Extreme types, helper functions
eernstg Nov 15, 2021
7afdc38
Rebase
eernstg Nov 16, 2021
de15537
.call insertion on nullable type; clean up BlindDefineSymbol
eernstg Nov 16, 2021
c0910cd
Rebase
eernstg Nov 16, 2021
f27f86b
Main
eernstg Nov 16, 2021
40ef209
Type Type
eernstg Nov 17, 2021
7f8413e
Type Type fixes
eernstg Nov 17, 2021
4d867c0
More typeType fixes
eernstg Nov 17, 2021
644986a
Constant instances (in particular: about canonical instances)
eernstg Nov 18, 2021
074db1d
Corrected variable initialization specification ("has been stored" ra…
eernstg Nov 19, 2021
68d87ae
Small adjustments to Variables
eernstg Nov 19, 2021
a2bb6ca
Rebase
eernstg Nov 26, 2021
b583f3f
Boolean conversion; type test; made true/false terminology consistent…
eernstg Nov 29, 2021
053e09e
Constant types; type variable elimination in constants
eernstg Nov 29, 2021
ecabd43
Conditional expression; operators && and ||; `if` statements; delete …
eernstg Nov 30, 2021
0199748
Integrate Null Promotion; put v==null rules into Type Promotion, and …
eernstg Dec 1, 2021
d4a5c67
Null shorting
eernstg Dec 1, 2021
015d020
Small fixes in section Null Shorting
eernstg Dec 1, 2021
7faffb0
Revisiting all occurrences of \NULL/Null/null
eernstg Dec 2, 2021
01cb5a1
Did much of Standard ... Bounds
eernstg Dec 3, 2021
91c126d
Standard bounds
eernstg Dec 7, 2021
455630c
Fixed the "SUB issues" section
eernstg Dec 8, 2021
a261360
Rebase
eernstg Dec 8, 2021
81de15f
Rebase
eernstg Dec 8, 2021
0dc2b83
Rebase
eernstg Dec 8, 2021
ee90d78
Rebase
eernstg Dec 9, 2021
729e261
Rebase
eernstg Dec 10, 2021
38a6921
Clarified and corrected Canonical Syntax
eernstg Dec 10, 2021
649c437
Fixed subsubsection --> subsection, 2*
eernstg Dec 10, 2021
c008ec2
Typos
eernstg Jan 5, 2022
fc613cb
Whitespace
eernstg Jan 6, 2022
0f8e0ee
Interface type fixes
eernstg Jan 6, 2022
f1e186f
Sync with specify_null_safety_new_sections_dec21
eernstg Jan 7, 2022
23dfe70
Mark a subtype rule as redundant, in a TODO comment
eernstg Jan 7, 2022
46e277d
Adjust no-loops-in-noSuchMethod example
eernstg Feb 7, 2022
0dec511
Adjust no-loops-in-noSuchMethod example
eernstg Feb 8, 2022
ea9f425
Corrected function type subtype rule (bounds); corrected "math" index…
eernstg May 3, 2022
98ec8de
Adjust class building types
eernstg May 9, 2022
e0fbf25
Adjust examples declaring non-nullable positional optional parameters…
eernstg Jul 26, 2022
e3f7804
Add a TODO to introduce `Any`
eernstg Nov 2, 2022
1df466b
Correct example in section about super-bounded types
eernstg Nov 3, 2022
6e91dc5
Correction based on https://github.com/dart-lang/language/issues/2679
eernstg Dec 2, 2022
e7970ad
Specify erasure of intersection types for the semantics of await expr…
eernstg Dec 9, 2022
c06d9b7
Typo
eernstg Jan 20, 2023
21920b7
Introduce \DynamicError, marking all dynamic errors just like compile…
eernstg Feb 2, 2023
8b1f9b3
Changed the error margin markers to use red text
eernstg Feb 2, 2023
52728d9
Correct dynamic type of tear-off with covariant parameter
eernstg May 31, 2023
5d8d8c9
Clarified tear-offs of methods with covariant parameters
eernstg May 31, 2023
ca38e1d
Correct a typo about closurization
eernstg May 31, 2023
9025186
Correction: Add definition of normalizedType/topMergeType for member …
eernstg Jun 16, 2023
4db16fb
Correction: Update dynamic type of covariant parameter to Object?
eernstg Jun 22, 2023
a090cb5
Typo
eernstg Jun 29, 2023
91d205a
Add commentary to emphasize that `new`/`const` can be implicit, and `…
eernstg Jul 5, 2023
54d35bd
Add missing updates in section typeVoid
eernstg Jul 6, 2023
dc8a1b5
Add missing error: default values must be type correct
eernstg Jul 13, 2023
76e5654
Add a paragraph explaining that the given section is about both optio…
eernstg Jul 13, 2023
0d40956
Post-rebase error correction
eernstg Jul 21, 2023
97e0128
Correct usages of "final variable" and "constant variable"
eernstg Jul 21, 2023
da08c68
Add missing declaration kind about getter/setter type error
eernstg Sep 11, 2023
2e8051b
Remove obsolete reference to "mixin composition" from section Supercl…
eernstg Sep 29, 2023
7731e25
Add comment about default values of noSuchMethod forwarders being und…
eernstg Sep 29, 2023
eb352ca
Correct rule about the interface of T?
eernstg Jan 10, 2024
55e362d
Correct rule about interfaces of bounded types
eernstg Jan 10, 2024
35ff04d
Corrected many occurrences of "string" to "string literal"
eernstg Feb 22, 2024
79258a0
Update the "parameter name `_...`" error
eernstg Apr 30, 2024
8c9fe27
Restore the index marker, define a command for it
eernstg Jun 17, 2024
3f3003c
Corrected the huge rebase operation (removed TODO material)
eernstg Jun 17, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Introduce \DynamicError, marking all dynamic errors just like compile…
…-time errors have been for a while
  • Loading branch information
eernstg committed Jun 19, 2024
commit 21920b7eaf2a6c732e1e7228360333234f5a3a53
10 changes: 7 additions & 3 deletions specification/dart.sty
Original file line number Diff line number Diff line change
Expand Up @@ -175,7 +175,7 @@

% Used for defining occurrence of phrase, with customized index entry.
\newcommand{\IndexCustom}[2]{%
\leavevmode\marginpar{\ensuremath{_{^\vartriangle}}}\emph{#1}\index{#2}}
\leavevmode\marginpar{\ensuremath{\vartriangle}}\emph{#1}\index{#2}}

% Used for the defining occurrence of a local symbol.
\newcommand{\DefineSymbol}[1]{%
Expand All @@ -196,11 +196,15 @@

% Same appearance, but not adding an entry to the index.
\newcommand{\NoIndex}[1]{%
\leavevmode\marginpar{\ensuremath{_{^\vartriangle}}}\emph{#1}}
\leavevmode\marginpar{\ensuremath{\vartriangle}}\emph{#1}}

% Mark a compile-time error in the margin.
\newcommand{\Error}[1]{%
\leavevmode\marginpar{\ensuremath{_{^\ominus}}}{#1}}
\leavevmode\marginpar{\ensuremath{\ominus}}{#1}}

% Mark a dynamic error in the margin.
\newcommand{\DynamicError}[1]{%
\leavevmode\marginpar{\Lightning}{#1}}

% Used to specify comma separated lists of similar symbols.
\newcommand{\List}[3]{\ensuremath{{#1}_{#2},\,\ldots,\ {#1}_{#3}}}
Expand Down
86 changes: 53 additions & 33 deletions specification/dartLangSpec.tex
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
\usepackage[T1]{fontenc}
\usepackage{makeidx}
\usepackage{enumitem}
\usepackage{marvosym}
\makeindex
\title{Dart Programming Language Specification\\
{6th edition draft}\\
Expand Down Expand Up @@ -97,9 +98,11 @@
% error anyway; change extension names to `typeIdentifier`, avoiding
% built-in identifiers).
%
% Feb 2023
% Jan, Feb 2023
% - Change the specification of constant expressions of the form `e1 == e2`
% to use primitive equality.
% - Introduce `\DynamicError{}`, thus marking every introduction (definition)
% of a dynamic error by a lightning symbol in the right margin.
%
% Dec 2022
% - Change the definition of the type function 'flatten' to resolve soundness
Expand Down Expand Up @@ -1614,7 +1617,7 @@ \subsection{Implicitly Induced Getters and Setters}
will bind \id{} to the object that the argument $x$ is bound to.
An execution of the setter
in a situation where the variable \id{} has been bound to an object
will incur a dynamic error.
will incur a \DynamicError{dynamic error}.
\EndCase

\LMHash{}%
Expand Down Expand Up @@ -4207,7 +4210,7 @@ \subsubsection{Generative Constructors}
% This can occur due to a failing implicit cast.
unless the assigned object has a dynamic type
which is not a subtype of the declared type of the instance variable \id,
in which case a dynamic error occurs.
in which case a \DynamicError{dynamic error} occurs.

\commentary{%
The above rule allows initializing formals to be used as optional parameters:%
Expand Down Expand Up @@ -10563,7 +10566,7 @@ \subsubsection{Collection Literal Element Evaluation}
or the given \code{value} does not have the type \code{Value},
but it cannot occur after the pair has been appended to $s$.
\item
Otherwise, a dynamic error occurs.
Otherwise, a \DynamicError{dynamic error} occurs.

\commentary{%
This occurs when the target is an iterable respectively a map,
Expand Down Expand Up @@ -10618,7 +10621,8 @@ \subsubsection{Collection Literal Element Evaluation}
and if $\ell_2$ is not present then
$\EvaluateElement{\ell} := \LiteralSequence{}$.
% $o_b$ can have type \DYNAMIC.
If $o_b$ is neither \TRUE{} nor \FALSE{} then a dynamic error occurs.
If $o_b$ is neither \TRUE{} nor \FALSE{}
then a \DynamicError{dynamic error} occurs.
\EndCase

\LMHash{}%
Expand Down Expand Up @@ -10849,7 +10853,7 @@ \subsubsection{Lists}
An empty list has an empty set of indices.
A non-empty list has the index set $\{0, \ldots, n - 1\}$
where $n$ is the size of the list.
It is a dynamic error to attempt to access a list
It is a \DynamicError{dynamic error} to attempt to access a list
using an index that is not a member of its set of indices.

\rationale{%
Expand All @@ -10873,7 +10877,8 @@ \subsubsection{Lists}
Only run-time list literals can be mutated
after they are created.
% This error can occur because being constant is a dynamic property.
Attempting to mutate a constant list literal will result in a dynamic error.
Attempting to mutate a constant list literal
will result in a \DynamicError{dynamic error}.

\commentary{%
% The following is true either directly or indirectly: There is a \CONST{}
Expand Down Expand Up @@ -11642,7 +11647,7 @@ \subsubsection{Sets}
\LMHash{}%
A set may contain zero or more objects.
Sets have a method which can be used to insert objects;
this will incur a dynamic error if the set is not modifiable.
this will incur a \DynamicError{dynamic error} if the set is not modifiable.
Otherwise, when inserting an object $o_{\metavar{new}}$ into a set $s$,
if an object $o_{\metavar{old}}$ exists in $s$ such that
\code{$o_{\metavar{old}}$ == $o_{\metavar{new}}$} evaluates to \TRUE{}
Expand Down Expand Up @@ -11682,7 +11687,8 @@ \subsubsection{Sets}
and it is evaluated at run time.
Only run-time set literals can be mutated after they are created.
% This error can occur because being constant is a dynamic property, here.
Attempting to mutate a constant set literal will result in a dynamic error.
Attempting to mutate a constant set literal
will result in a \DynamicError{dynamic error}.

\commentary{%
% The following is true either directly or indirectly: There is a \CONST{}
Expand Down Expand Up @@ -11888,7 +11894,8 @@ \subsubsection{Maps}
and it is evaluated at run time.
Only run-time map literals can be mutated after they are created.
% This error can occur because being constant is a dynamic property, here.
Attempting to mutate a constant map literal will result in a dynamic error.
Attempting to mutate a constant map literal
will result in a \DynamicError{dynamic error}.

\commentary{%
% The following is true either directly or indirectly: There is a \CONST{}
Expand Down Expand Up @@ -12029,7 +12036,8 @@ \subsection{Throw}
}

\LMHash{}%
If $v$ is the null object (\ref{null}), then a dynamic error occurs.
If $v$ is the null object (\ref{null})
then a \DynamicError{dynamic error} occurs.
Otherwise let $t$ be a stack trace corresponding to the current execution state,
and the \THROW{} statement throws with $v$ as exception object
and $t$ as stack trace (\ref{expressionEvaluation}).
Expand Down Expand Up @@ -12571,7 +12579,7 @@ \subsubsection{New}
% This error can occur because being-loaded is a dynamic property.
If $T$ is a deferred type with prefix $p$,
then if $p$ has not been successfully loaded,
a dynamic error occurs.
a \DynamicError{dynamic error} occurs.
\EndCase

\LMHash{}%
Expand Down Expand Up @@ -13500,7 +13508,7 @@ \subsubsection{Binding Actuals to Formals}
If $r = 0$ and $s > 0$ then
if $f$ does not have default type arguments
(\ref{instantiationToBound})
then a dynamic error occurs.
then a \DynamicError{dynamic error} occurs.
Otherwise replace the actual type argument list:
Let $r$ be $s$ and let $t_i$ for $i \in 1 .. s$ be the result of
instantiation to bound
Expand Down Expand Up @@ -16569,7 +16577,8 @@ \subsection{Assignment}
in which case $v$ has no initializer and is not definitely assigned,
or a compile-time error would have occurred%
}).
If $v$ has previously been bound to an object then a dynamic error occurs.
If $v$ has previously been bound to an object
then a \DynamicError{dynamic error} occurs.
Otherwise, $v$ is bound to $o$, and then $a$ evaluates to $o$
(\ref{expressionEvaluation}).
\item
Expand Down Expand Up @@ -17121,7 +17130,8 @@ \subsection{Conditional}
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}.
It is a \DynamicError{dynamic error}
if the run-time type of $o_1$ is not \code{bool}.
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$.
Expand Down Expand Up @@ -17189,23 +17199,27 @@ \subsection{Logical Boolean Expressions}
\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}.
It is a \DynamicError{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,
otherwise $e_2$ is evaluated to an object $o_2$.
% This error can occur due to an implicit downcast from \DYNAMIC.
It is a dynamic error if the run-time type of $o_2$ is not \code{bool}.
It is a \DynamicError{dynamic error}
if the run-time type of $o_2$ is not \code{bool}.
Otherwise the result of evaluating $b$ is $o_2$.

\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}.
It is a \DynamicError{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,
otherwise $e_2$ is evaluated to an object $o_2$.
% This error can occur due to an implicit downcast from \DYNAMIC.
It is a dynamic error if the run-time type of $o_2$ is not \code{bool}.
It is a \DynamicError{dynamic error}
if the run-time type of $o_2$ is not \code{bool}.
Otherwise the result of evaluating $b$ is $o_2$.


Expand Down Expand Up @@ -17790,7 +17804,7 @@ \subsection{Postfix Expressions}

\LMHash{}%
$e$ is evaluated as follows: $e_1$ is evaluated to an object $o$.
If $o$ is the null object then a dynamic error occurs,
If $o$ is the null object then a \DynamicError{dynamic error} occurs,
otherwise $e$ evaluates to $o$.
\EndCase

Expand Down Expand Up @@ -19128,7 +19142,7 @@ \subsection{Local Variable Declaration}
then $v$ is bound to $o$.
If an object $o$ is assigned to $v$
in a situation where $v$ is bound to an object $o'$
then a dynamic error occurs
then a \DynamicError{dynamic error} occurs
(\commentary{it does not matter whether $o$ is the same object as $o'$}).

\commentary{%
Expand Down Expand Up @@ -19289,7 +19303,8 @@ \subsection{If}
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}.
It is a \DynamicError{dynamic error}
if the run-time type of $o$ is not \code{bool}.
If $o$ is \TRUE, then execute the block statement $S_1$,
otherwise execute the block statement $S_2$.

Expand Down Expand Up @@ -19374,7 +19389,8 @@ \subsubsection{For Loop}
\item
The expression $[v'/v]c$ is evaluated 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}.
It is a \DynamicError{dynamic error}
if the run-time type of $o$ is not \code{bool}.
If $o$ is \FALSE, the for loop completes normally.
Otherwise, execution continues at step \ref{beginIteration}.
\item
Expand Down Expand Up @@ -19587,7 +19603,8 @@ \subsection{While}
\LMHash{}%
The expression $e$ is evaluated 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}.
It is a \DynamicError{dynamic error}
if the run-time type of $o$ is not \code{bool}.

\LMHash{}%
If $o$ is \FALSE, then execution of the while statement completes normally
Expand Down Expand Up @@ -19638,7 +19655,8 @@ \subsection{Do}
\LMHash{}%
Then, the expression $e$ is evaluated 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}.
It is a \DynamicError{dynamic error}
if the run-time type of $o$ is not \code{bool}.
If $o$ is \FALSE, execution of the do statement completes normally
(\ref{statementCompletion}).
If $o$ is \TRUE, then the do statement is re-executed.
Expand Down Expand Up @@ -20329,7 +20347,8 @@ \subsection{Return}

\LMHash{}%
The expression $e$ is evaluated to an object $o$.
A dynamic error occurs unless the dynamic type of $o$ is a subtype of
A \DynamicError{dynamic error} occurs
unless the dynamic type of $o$ is a subtype of
the actual return type of $f$
(\ref{actualTypes}).
Then the return statement $s$ completes returning $o$
Expand All @@ -20356,7 +20375,8 @@ \subsection{Return}
let \code{v} be a fresh variable bound to $o$ and
evaluate \code{\AWAIT{} v} to an object $r$;
otherwise let $r$ be $o$.
A dynamic error occurs unless the dynamic type of $r$
A \DynamicError{dynamic error} occurs
unless the dynamic type of $r$
is a subtype of the actual value of $T_v$
(\ref{actualTypes}).
Then the return statement $s$ completes returning $r$
Expand Down Expand Up @@ -21253,21 +21273,21 @@ \subsubsection{Semantics of Imports}
\NamespaceName{\metavar{import},i},
a corresponding getter named \id{} with the same function header as $g$.
% This error can occur because being-loaded is a dynamic property.
Calling the getter results in a dynamic error.
Calling the getter results in a \DynamicError{dynamic error}.
\item
For every top level setter $s$ named \code{\id=} in
\NamespaceName{\metavar{import},i},
a corresponding setter named \code{\id=} with
the same function header as $s$.
% This error can occur because being-loaded is a dynamic property.
Calling the setter results in a dynamic error that occurs before
the actual argument is evaluated.
Calling the setter results in a \DynamicError{dynamic error}
that occurs before the actual argument is evaluated.
\item
For every class, mixin, enum, and type alias declaration named \id{} in
\NamespaceName{\metavar{import},i},
a corresponding getter named \id{} with return type \code{Type}.
% This error can occur because being-loaded is a dynamic property.
Calling the getter results in a dynamic error.
Calling the getter results in a \DynamicError{dynamic error}.
\end{itemize}

\rationale{%
Expand Down Expand Up @@ -21801,7 +21821,7 @@ \subsection{Scripts}
that spawned $i$%
}),
or the null object if no such object was supplied.
A dynamic error occurs if
A \DynamicError{dynamic error} occurs if
the run-time type of this object is not a subtype of
the declared type of the corresponding parameter of \code{main}.
\end{itemize}
Expand All @@ -21824,7 +21844,7 @@ \subsection{Scripts}
(\commentary{%
the above rules ensure that the corresponding parameters are optional%
}).
But the implementation must ensure that a dynamic error occurs
But the implementation must ensure that a \DynamicError{dynamic error} occurs
if an actual argument does not have a run-time type which is
a subtype of the declared type of the parameter.

Expand Down