Eliminated usages of "field" in the spec.

docs/language/dartLangSpec.tex

 \documentclass{article}
 \usepackage{epsfig}
 \usepackage{color}
 \usepackage{dart}
 \usepackage{bnf}
 \usepackage{hyperref}
 \usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \newcommand{\code}[1]{{\sf #1}}
 \title{Dart Programming Language  Specification  \\
@@ skipping 177 matching lines @@
 
 \subsection{Scoping}
 \LMLabel{scoping}
 
 \LMHash{}
 A {\em namespace} is a mapping of names denoting declarations to actual declarations.  Let $NS$ be a namespace. We say that a name $n$ {\em is in }$NS$ if $n$ is a key of $NS$. We say a declaration $d$ {\em is in }$NS$ if a key of $NS$ maps to $d$.
 
 \LMHash{}
 A scope $S_0$ induces a namespace $NS_0$ that maps the simple name of each variable, type or function declaration $d$ declared in $S_0$ to $d$. Labels are not included in the induced namespace of a scope; instead they have their own dedicated namespace.
 
-\commentary{It is therefore impossible, e.g.,  to define a class that declares a method and a field with the same name in Dart. Similarly one cannot declare a top-level function with the same name as a library variable or class.
-  }
+\commentary{
+It is therefore impossible, e.g., to define a class that declares a method and an instance variable with the same name in Dart.

[Lasse Reichstein Nielsen, 2017/01/09 08:55:12]

It doesn't have to be an instance variable - the existing text also covered a
"static variable", just as method covers both static and instance methods. So:
"(static or instance) variable". Or really, just "getter" - because instance
variables don't have names, their implicit getters do.

[eernst, 2017/01/09 10:16:52]

Actually, my reasoning was "it says `e.g.`, so we just need an example that
works, not a complete list".

I adjusted it to getter anyway, because that's just as good as an example, it
covers the inst/stat variables, we avoid the heavy 'instance or static' (I think
a bare `variable` will be too confusing to use it as `instance or static
variable`), and the reference to variables is present in the next sentence
anyway.

+Similarly one cannot declare a top-level function with the same name as a library variable or a class.
+}
 
 \LMHash{}
 It is a compile-time error if there is more than one entity with the same name declared in the same scope.
 
 \commentary{
 In some cases, the name of the declaration differs from the identifier used to declare it.  Setters have names that are distinct from the corresponding getters because they always have an = automatically added at the end, and unary minus has the special name unary-.
 }
 
 \LMHash{}
 Dart is lexically scoped.    Scopes may nest.  A name or declaration $d$ is {\em available in scope} $S$ if $d$ is in the namespace induced by $S$ or if $d$ is available in the lexically enclosing scope of $S$. We  say that a name or declaration $d$ is {\em in scope} if $d$ is available in the current scope.
@@ skipping 841 matching lines @@
 
 %It is a compile-time error if a getter`s formal parameter list is not empty.
 
 \LMHash{}
 The instance getters of a class $C$ are those instance getters declared by $C$, either implicitly or explicitly, and the instance getters inherited by $C$ from its superclass. The static getters of a class $C$ are those static getters declared by $C$.
 
 \LMHash{}
 It is a compile-time error if a class has both a getter and a method with the same name. This restriction holds regardless of whether the getter is defined explicitly or implicitly, or whether the getter or the method are inherited or not.
 
 \commentary{
-This implies that a getter can never override a method, and a method can never override a getter or field.
+This implies that a getter can never override a method, and a method can never override a getter or an instance variable.

[Lasse Reichstein Nielsen, 2017/01/09 08:55:12]

It's really not necessary to mention instance variables here - instance
variables/fields are anonymous, they just introduce an implicit getter with that
name, and we already mentioned getters.
(But, since it's commentary, it is allowed to repeat itself for pedagogical
reasons).

[eernst, 2017/01/09 10:16:52]

Right. I'll keep it to give the hint to readers who don't automatically see the
connection.

 }
 
 \LMHash{}
 It is a static warning if the return type of a getter is \VOID.
 It is a static warning if a getter $m_1$ overrides  (\ref{inheritanceAndOverriding}) a getter
 $m_2$ and the type of $m_1$ is not a subtype of the type of $m_2$.
 
 \LMHash{}
 It is a static warning if a class  declares a static getter named $v$ and also has a non-static setter named $v=$. It is a static warning if a class $C$ declares an instance getter named $v$ and an accessible static member named $v$ or $v=$ is declared in a superclass of $C$. These warnings must be issued regardless of whether the getters or setters are declared explicitly or implicitly.
 
@@ skipping 166 matching lines @@
 \begin{grammar}
 {\bf constructorSignature:}
       identifier (`{\escapegrammar .}' identifier)? formalParameterList
     .
  \end{grammar}
 
 \LMHash{}
 A {\em constructor parameter list} is a parenthesized, comma-separated list of formal constructor parameters. A {\em formal constructor parameter} is either a formal parameter (\ref{formalParameters}) or an initializing formal. An {\em initializing formal} has the form \code{\THIS{}.$id$}, where $id$ is the name of an instance variable of the immediately enclosing class.  It is a compile-time error if $id$ is not an instance variable of the immediately enclosing class. It is a compile-time error if an initializing formal is used by a function other than a non-redirecting generative constructor.
 
 \LMHash{}
-If an explicit type is attached to the initializing formal, that is its static type. Otherwise, the type of an initializing formal named $id$ is $T_{id}$, where $T_{id}$ is the type of the field named $id$ in the immediately enclosing class. It is a static warning if the static type of $id$ is not assignable to $T_{id}$.
+If an explicit type is attached to the initializing formal, that is its static type.
+Otherwise, the type of an initializing formal named $id$ is $T_{id}$, where $T_{id}$ is the type of the instance variable named $id$ in the immediately enclosing class.
+It is a static warning if the static type of $id$ is not assignable to $T_{id}$.
 
 \LMHash{}
 Initializing formals constitute an exception to the rule that every formal parameter introduces a local variable into the formal parameter scope (\ref{formalParameters}).
 When the formal parameter list of a non-redirecting generative constructor contains any initializing formals, a new scope is introduced, the {\em formal parameter initializer scope}, which is the current scope of the initializer list of the constructor, and which is enclosed in the scope where the constructor is declared.
 Each initializing formal in the formal parameter list introduces a final local variable into the formal parameter initializer scope, but not into the formal parameter scope; every other formal parameter introduces a local variable into both the formal parameter scope and the formal parameter initializer scope.
 
 \commentary{
 This means that formal parameters, including initializing formals, must have distinct names, and that initializing formals are in scope for the initializer list, but they are not in scope for the body of the constructor.
 When a formal parameter introduces a local variable into two scopes, it is still one variable and hence one storage location.
 The type of the constructor is defined in terms of its formal parameters, including the initializing formals.
 }
 
 \LMHash{}
-Initializing formals are executed during the execution of generative constructors detailed below. Executing an initializing formal  \code{\THIS{}.$id$} causes the field $id$ of the immediately surrounding class to be assigned the value of the corresponding actual parameter, unless $id$ is a final variable that has already been initialized, in which case a runtime error occurs.
-
+Initializing formals are executed during the execution of generative constructors detailed below.
+Executing an initializing formal \code{\THIS{}.$id$} causes the instance variable $id$ of the immediately surrounding class to be assigned the value of the corresponding actual parameter,
+unless $id$ is a final variable that has already been initialized, in which case a runtime error occurs.
 
 \commentary{
 The above rule allows initializing formals to be used as optional parameters:
 }
 
 \begin{dartCode}
 class A \{
   int x;
   A([this.x]);
 \}
@@ skipping 129 matching lines @@
 but the actual call always happens after all initializers have been processed.
 It is not equivalent to moving the super call to the end of the initializer list
 because the argument expressions may have visible side effects
 which must happen in the order the expressions occur in the program text.
 }
 
 \LMHash{}
 After the superinitializer has completed, the body of $k$ is executed in a scope where \THIS{} is bound to $i$.
 
 \rationale{
-This process ensures that no uninitialized final field is ever seen by code. Note that \THIS{} is not in scope on the right hand side of an initializer (see \ref{this}) so no instance method can execute during initialization: an instance method cannot be directly invoked, nor can \THIS{} be passed into any other code being invoked in the initializer.
+This process ensures that no uninitialized final instance variable is ever seen by code.
+Note that \THIS{} is not in scope on the right hand side of an initializer (see \ref{this}) so no instance method can execute during initialization:
+an instance method cannot be directly invoked, nor can \THIS{} be passed into any other code being invoked in the initializer.
 }
 
 \LMHash{}
 During the execution of a generative constructor to initialize an instance $i$,
 execution of an initializer of the form \code{\THIS{}.$v$ = $e$}
 proceeds as follows:
 
 \LMHash{}
-First, the expression $e$ is evaluated to an object $o$. Then, the instance variable $v$ of $i$ is bound to $o$, unless $v$ is a final variable that has already been initialized, in which case a runtime error occurs. In checked mode, it is a dynamic type error if $o$ is not \NULL{} and the interface of the class of $o$ is not a subtype of the actual type of the field $v$.
+First, the expression $e$ is evaluated to an object $o$.
+Then, the instance variable $v$ of $i$ is bound to $o$, unless $v$ is a final variable that has already been initialized, in which case a runtime error occurs.

[Lasse Reichstein Nielsen, 2017/01/09 08:55:12]

This is statically detectable, so in Strong Mode we should ensure that it's a
compile-time error (if we don't already).

[eernst, 2017/01/09 10:16:52]

Agreed: We should be able to detect statically precisely when that will occur.

I added a comment "%%STRONG_MODE: ..". We could use that to put in reminders
about locations where strong mode (or 2.0) requires updates.

+In checked mode, it is a dynamic type error if $o$ is not \NULL{} and the interface of the class of $o$ is not a subtype of the actual type of the instance variable $v$.
 
 \LMHash{}
 An initializer of the form \code{$v$ = $e$} is equivalent to an initializer of the form \code{\THIS{}.$v$ = $e$}.
 
 \LMHash{}
 Execution of a superinitializer of the form
 
 \SUPER{}$(a_1, \ldots, a_n,  x_{n+1}: a_{n+1}, \ldots, x_{n+k}: a_{n+k})$
 
 (respectively  \SUPER{}$.id(a_1, \ldots, a_n, x_{n+1}: a_{n+1}, \ldots, x_{n+k}: a_{n+k})$
@@ skipping 388 matching lines @@
 \rationale {
 It would be  more attractive to give a purely local definition of inheritance, that depended only on the members of the direct superclass $S$. However, a class $C$ can inherit a member $m$ that  is not a member of its superclass  $S$. This can occur when the member $m$ is private
 to the library $L_1$ of $C$, whereas $S$ comes from a different library $L_2$, but
 the superclass chain of $S$ includes a class declared in $L_1$.
 }
 
 \LMHash{}
 A class may override instance members that would otherwise have been inherited from its superclass.
 
 \LMHash{}
-Let $C = S_0$ be a class declared in library $L$, and let $\{S_1 \ldots S_k\}$ be the set of all superclasses of $C$, where $S_i$ is the superclass of $S_{i-1}$ for $i \in 1 .. k$. Let $C$ declare a member $m$, and let  $m^\prime$ be a member of $S_j, j  \in 1 .. k$,  that has the same name as $m$, such that $m^\prime$ is accessible to $L$.  Then $m$ overrides $m^\prime$ if $m^\prime$ is not already overridden by a member of at least one of $S_1 \ldots S_{j-1}$ and neither $m$ nor $m^\prime$ are fields.
+Let $C = S_0$ be a class declared in library $L$, and let $\{S_1 \ldots S_k\}$ be the set of all superclasses of $C$, where $S_i$ is the superclass of $S_{i-1}$ for $i \in 1 .. k$.
+Let $C$ declare a member $m$, and let  $m^\prime$ be a member of $S_j, j  \in 1 .. k$,  that has the same name as $m$, such that $m^\prime$ is accessible to $L$.
+Then $m$ overrides $m^\prime$ if $m^\prime$ is not already overridden by a member of at least one of $S_1 \ldots S_{j-1}$ and neither $m$ nor $m^\prime$ are instance variables.

[Lasse Reichstein Nielsen, 2017/01/09 08:55:11]

We are still being inconsistent. Fields are not really *members*. They are
*member declarations* and they introduce /getter/ and (potentially) /setter/
*members*.

That's why we get paragraphs like this that have to say that you override unless
one of them is an instance variable - but doesn't mention that the implicit
getter/setter does override (leaving that for the commentary below).
Maybe we can find a way to do the distinction properly (but that's for another
CL).

[eernst, 2017/01/09 10:16:52]

Acknowledged.

 
 %Let $C$ be a class declared in library $L$, with superclass $S$ and let $C$ declare an instance member $m$, and  assume $S$ declares an instance member $m^\prime$ with the same name as $m$. Then $m$ {\em overrides} $m^\prime$ iff $m^\prime$ is accessible (\ref{privacy}) to $L$, $m$ has the same name as  $m^\prime$  and neither $m$ nor $m^\prime$ are fields.
 
-\commentary{Fields never override each other. The getters and setters induced by fields do.}
+\commentary{Instance variables never override each other. The getters and setters induced by instance variables do.}
 
 \rationale{Again, a local definition of overriding would be preferable, but fails to account for library privacy.
 }
 
 \LMHash{}
 Whether an override is legal or not is described elsewhere in this specification (see \ref{instanceMethods}, \ref{getters} and \ref{setters}).
 
 \commentary{For example getters may not legally override methods and vice versa. Setters never override methods or getters, and vice versa, because their names always differ.
 }
 
 \rationale{
 It is nevertheless convenient to define the override relation between members in this way, so that we can concisely describe the illegal cases.
 }
 
 \commentary{
 Note that instance variables do not participate in the override relation, but the getters and setters they induce do. Also, getters don't override setters and vice versa.  Finally, static members never override anything.
 }
 
 \LMHash{}
 It is a static warning if a non-abstract class inherits an abstract method.
 
 \commentary {
 For convenience, here is a summary of the relevant rules. Remember that this is not normative. The controlling language is in the relevant sections of the specification.
 
 \begin{enumerate}
 
-\item There is only one namespace for getters, setters, methods and constructors (\ref{scoping}). A field $f$ introduces a getter $f$ and a non-final field $f$ also introduces a setter $f=$ (\ref{instanceVariables}, \ref{staticVariables}). When we speak of members here, we mean accessible fields, getters, setters and methods (\ref{classes}).
+\item There is only one namespace for getters, setters, methods and constructors (\ref{scoping}).
+  An instance or static variable $f$ introduces a getter $f$ and a non-final instance or static variable $f$ also introduces a setter $f=$ (\ref{instanceVariables}, \ref{staticVariables}).
+  When we speak of members here, we mean accessible instance or static variables, getters, setters, and methods (\ref{classes}).

[Lasse Reichstein Nielsen, 2017/01/09 08:55:12]

Yep, inconsistent! We do "member lookup" elsewhere and won't find variables
because they are not really members.
Again, OK for now, should fix later.

[eernst, 2017/01/09 10:16:52]

Acknowledged.

 \item You cannot have two  members with the same name in the same class - be they declared or inherited (\ref{scoping}, \ref{classes}).
 \item Static members are never inherited.
 \item It is a warning if you have an  static member named $m$ in your class or any superclass (even though it is not inherited) and an  instance member of the same name (\ref{instanceMethods}, \ref{getters}, \ref{setters}).
 \item It is a warning if you have a static setter $v=$, and an instance member $v$ (\ref{setters}).
 \item It is a warning if you have a static getter $v$ and an instance setter $v=$ (\ref{getters}).
 \item If you define an instance member named $m$, and your superclass has an  instance member of the same name, they override each other. This may or may not be legal.
 \item \label{typeSigAssignable}
 If two members override each other, it is a static warning if their type signatures are not assignable to each other (\ref{instanceMethods}, \ref{getters}, \ref{setters}) (and  since these are function types, this means the same as "subtypes of each other").
 \item \label{requiredParams}
 If two members override each other, it is a static warning if the overriding member has more required parameters  than the overridden one (\ref{instanceMethods}).
@@ skipping 232 matching lines @@
     .
 \end{grammar}
 
 \LMHash{}
 A  mixin application of the form  \code{$S$ \WITH{} $M$;} defines a class  $C$ with superclass  $S$.
 
 \LMHash{}
 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$.
 
 \LMHash{}
-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$.
+In both cases above, $C$ declares the same instance members as $M$ (respectively, $M_k$).
+If any of the instance variables of $M$ (respectively, $M_k$) have initializers, they are executed in the scope of $M$ (respectively, $M_k$) to initialize the corresponding instance variables of $C$.
 
 \LMHash{}
 Let $L_M$ be the library in which $M$ is declared.
 For each generative constructor named $q_i(T_{i1}$ $ a_{i1}, \ldots , T_{ik_i}$ $ a_{ik_i}), i \in 1..n$ of $S$ that is accessible to $L_M$, $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});$.
 
 %super.id
 
@@ skipping 247 matching lines @@
 
 \rationale{
 It is important that no runtime overhead be incurred by the introduction of metadata that is not actually used. Because metadata only involves constants, the time at which it is computed is irrelevant so that implementations may skip the metadata during ordinary parsing and execution and evaluate it lazily.
 }
 
 \commentary{
 It is possible to associate metadata with constructs that may not be accessible via reflection, such as local variables (though it is conceivable that in the future, richer reflective libraries might provide access to these as well).  This is not as useless as it might seem. As noted above, the data can be retrieved statically if source code is available.
 }
 
 \LMHash{}
-Metadata can appear before a library, part header, class, typedef, type parameter, constructor, factory, function, field, parameter, or variable declaration and before an import, export or part directive.
+Metadata can appear before a library, part header, class, typedef, type parameter, constructor, factory, function, parameter, or variable declaration and before an import, export or part directive.
 
 \LMHash{}
 The constant expression given in an annotation  is type checked and evaluated in the scope surrounding the declaration being annotated.
 
 
 \section{Expressions}
 \LMLabel{expressions}
 
 \LMHash{}
 \label{evaluation}
@@ skipping 61 matching lines @@
  \item $c_1$  and $c_2$  are instances of \cd{double} and  one of the following holds:
  \begin{itemize}
    \item $c_1$ and $c_2$ are non-zero and \code{$c_1$ == $c_2$}.
    \item  Both $c_1$ and $c_2$ are $+0.0$.
    \item Both  $c_1$ and $c_2$ are $-0.0$.
    \item Both $c_1$ and $c_2$ represent a NaN value with the same underlying bit pattern.
  \end{itemize}
  OR
  \item $c_1$ and $c_2$ are constant lists that are defined to be identical in the specification of literal list expressions (\ref{lists}), OR
  \item $c_1$ and $c_2$ are constant maps that are defined to be identical in the specification of literal map expressions (\ref{maps}), OR
- \item $c_1$ and $c_2$ are constant objects of the same class $C$ and each member field of $c_1$ is identical to the corresponding field of $c_2$. OR
+ \item $c_1$ and $c_2$ are constant objects of the same class $C$ and each instance variable of $c_1$ is identical to the corresponding instance variable of $c_2$. OR

[Lasse Reichstein Nielsen, 2017/01/09 08:55:12]

... and the value of each instance variable of ... is identical to the value of
the corresponding instance variable ... 

(an "instance variable" is not an object, it's value is).

[eernst, 2017/01/09 10:16:52]

Indeed, done!

 \item $c_1$ and $c_2$ are the same object.
 \end{itemize}
 
 \commentary{
 The definition of \cd{identity} for doubles differs from that of equality in that a NaN is identical to itself, and that negative and positive zero are distinct.
 }
 
 \rationale{
 The definition of equality for doubles is dictated by the IEEE 754 standard, which posits that NaNs do not obey the law of reflexivity.  Given that hardware implements these rules, it is necessary to support them for reasons of efficiency.
 
@@ skipping 1052 matching lines @@
 
 in which case let $i$ be the result of evaluating
 
 \NEW{} $T(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
 
 \LMHash{}
 Then:
 \begin{itemize}
 \item If during execution of the program, a constant object expression has already evaluated to an instance $j$ of class $R$ with type arguments $V_i, 1 \le i \le m$, then:
 \begin{itemize}
-\item For each instance variable $f$ of $i$, let $v_{if}$ be the value of the field $f$ in $i$, and let $v_{jf}$ be the value of the field $f$ in $j$. If  \code{identical($v_{if}$, $v_{jf}$)} for all fields $f$ in $i$, then the value of $e$ is $j$, otherwise the value of $e$ is $i$.
+\item For each instance variable $f$ of $i$, let $v_{if}$ be the value of the instance variable $f$ in $i$, and let $v_{jf}$ be the value of the instance variable $f$ in $j$.
+  If \code{identical($v_{if}$, $v_{jf}$)} for all instance variables $f$ in $i$ then the value of $e$ is $j$, otherwise the value of $e$ is $i$.
 \end{itemize}
 \item Otherwise the value of $e$ is $i$.
 \end{itemize}
 
 \commentary{
-In other words, constant objects are canonicalized.  In order to determine if an object is actually new, one has to compute it; then it can be compared to any cached instances. If an equivalent object exists in the cache, we throw away the newly created object and use the cached one. Objects are equivalent if they have identical fields and identical type arguments. Since the constructor cannot induce any side effects, the execution of the constructor is unobservable.  The constructor need only be executed once per call site, at compile-time.
+In other words, constant objects are canonicalized.
+In order to determine if an object is actually new, one has to compute it; then it can be compared to any cached instances.
+If an equivalent object exists in the cache, we throw away the newly created object and use the cached one.
+Objects are equivalent if they have identical type arguments and identical instance variables.
+Since the constructor cannot induce any side effects, the execution of the constructor is unobservable.
+The constructor need only be executed once per call site, at compile-time.
 }
 
 \LMHash{}
 The static type of a constant object expression of either 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})$
@@ skipping 1506 matching lines @@
 Evaluation of a postfix expression $e$ of the form \code{$v$++}, where $v$ is an identifier, proceeds as follows:
 
 \LMHash{}
 Evaluate $v$ to an object $r$ and let $y$ be a fresh variable bound to $r$.
 Evaluate \code{$v$ = $y$ + 1}.
 Then $e$ evaluates to $r$.
 
 \LMHash{}
 The static type of such an expression is the static type of $v$.
 
-
-\rationale{The above ensures that if $v$ is a field, the getter gets called exactly once. Likewise in the cases below.
+\rationale{
+The above ensures that if $v$ is a variable, the getter gets called exactly once.
+Likewise in the cases below.
 }
 
 \LMHash{}
 Evaluation of a postfix expression $e$ of the form \code{$C$.$v$++}
 proceeds as follows:
 
 \LMHash{}
 Evaluate \code{$C$.$v$} to a value $r$
 and let $y$ be a fresh variable bound to $r$.
 Evaluate \code{$C$.$v$ = $y$ + 1}.
@@ skipping 344 matching lines @@
 \LMHash{}
 The is-expression \code{$e$ \IS{}! $T$} is equivalent to \code{!($e$ \IS{} $T$)}.
 
 % Add flow dependent types
 
 
 \LMHash{}
 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 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.
+The rule only applies to locals and parameters, as instance or static variables 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).
+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$.
+We do not want to refine the type of a variable of type \DYNAMIC{}, as this could lead to more warnings rather than fewer.
+The opposite requirement, that $T \ne \DYNAMIC{}$ is a safeguard lest $S$ ever be $\bot$.
 }
 
 \LMHash{}
 The static type of an is-expression is \code{bool}.
 
 
 \subsection{ Type Cast}
 \LMLabel{typeCast}
 
 \LMHash{}
@@ skipping 2552 matching lines @@
 
 The invariant that each normative paragraph is associated with a line
 containing the text \LMHash{} should be maintained.  Extra occurrences
 of \LMHash{} can be added if needed, e.g., in order to make
 individual \item{}s in itemized lists addressable.  Each \LM.. command
 must occur on a separate line.  \LMHash{} must occur immediately
 before the associated paragraph, and \LMLabel must occur immediately
 after the associated \section{}, \subsection{} etc.
 
 ----------------------------------------------------------------------