Static Semantics

The static semantics describes what can be known about a program before it runs: the type of every expression, the conformance of every class to its parents, and the well-formedness of every contract. A program that passes these checks is elaborated; one that fails is rejected, and never reaches the dynamic semantics of Chapter 5.

We proceed in this manner: first the semantic objects—the types and bindings the rules manipulate; then the relations among them—conformance and lookup; then the inference rules that assign types to phrases.

4.1Types

A type is one of the following.

Here \(A\) ranges over class names. A class type with no arguments is written \(A\) rather than \(A[\,]\). The scalar types, \(\mathsf{Any}\), \(\mathsf{Function}\) and the collection classes are not primitive in any deep sense: they are the classes of the standard environment (Appendix B), and \(\texttt{Integer}\) and the rest are abbreviations for particular class types. We keep them syntactically distinct only because the lexer does.

\(\mathsf{Any}\) is the type of which every type is a subtype; it is the elaborated form of the root class Any. \(\mathsf{Void}\) is the type assigned to a statement, and to a routine with no declared return type: it is not a value type and may not be the type of a field or parameter. \(\mathsf{Nil}\) is the type of the constant nil; it is a subtype of every optional type and of no other.

4.2The Static Environment

Elaboration takes place against a static environment, written \(C\), comprising three components:

• a class bindings \(\Sigma\), mapping each class name \(A\) in scope to its class signature — its generic parameters and their constraints, its modifiers (deferred, sealed), its parents, the typed fields it declares, and the typed signatures of its routines and constructors;
• a variable bindings \(\Gamma\), mapping each identifier in scope (parameters, locals, fields of the current object) to its type;
• a set \(\Delta\) of type variables currently in scope, introduced by the generic parameters of the enclosing class or routine.

We write \(C(x) = \tau\) for the lookup of an ordinary variable, \(C \oplus \{x : \tau\}\) for the environment \(C\) extended with the binding \(x:\tau\) (shadowing any earlier binding of \(x\)), and \(C(A)\) for the signature of class \(A\). The functions \(\mathit{fields}(C, A)\) and \(\mathit{routine}(C, A, m)\) collect, respectively, the fields and the named routine \(m\) visible in \(A\)—those declared in \(A\) together with those inherited from its parents, with \(A\)’s own declarations overriding inherited ones of the same name.

4.2.1Qualified Names and Ambiguity

\(\Sigma\) is built from two sources: the classes the current compilation unit declares itself, and those brought in by each of its intern declarations (Section 3.6), each entered under both its bare and its qualified name (Section 3.6.1). The current unit’s own declarations take precedence over anything interned: if the unit itself declares a class \(A\), \(\Sigma(A)\) is that declaration, regardless of what any interned unit also declares under the bare name \(A\). A qualified name is always well-defined in \(\Sigma\), and always denotes the one declaration it names, however many other units happen to share its bare spelling. Two intern declarations that name the same underlying compilation unit—directly, or transitively through what each in turn interns— contribute one declaration to \(\Sigma\), not two: the elaboration procedure of Section 7.2 visits each compilation unit at most once, so this is never a source of ambiguity.

A bare name \(A\) that the current unit does not declare itself is well-defined in \(\Sigma\) only when at most one interned unit declares a class of that name. When more than one does, \(A\) is an ambiguous reference: \(C(A)\) is undefined by ambiguity rather than by absence, and a program is rejected wherever such an \(A\) is written, unqualified, in a \(\mathit{ty}\), \(\mathit{parent}\), \(\mathit{createexp}\), or \(\mathit{pattern}\)—before any of the conditions of the rules below that read \(C(A)\) are checked. Writing the class in its qualified form is always well-defined and sidesteps the condition entirely, as does renaming the interned unit with as (Section 3.6), provided the renamed intern is itself path-qualified: an alias of a bare, unpathed intern has no qualified spelling to fall back on, and merely renames access to whichever single class that bare name already denotes.

4.3Conformance

The central relation of the static semantics is conformance, written \(\tau \preceq \tau'\) and read “\(\tau\) conforms to \(\tau'\)” or “\(\tau\) is a subtype of \(\tau'\).” A value of a conforming type may be used wherever the wider type is expected. Conformance is reflexive and transitive, and makes \(\mathsf{Any}\) a top to which every type conforms (rules C-Refl, C-Trans, C-Top in Appendix D). Its one substantive rule is inheritance: a class type conforms to its parents, with type arguments substituted through the inheritance clause. If \(A\) is declared inherit \(B[\sigma_1,\dots]\) under generic parameters \(\alpha_1,\dots,\alpha_n\), then

class Animal
  create make() do end
  feature
    speak(): String do result := "..." end
end

class Dog
  inherit Animal
  create make() do end
  feature
    speak(): String do result := "woof" end
end

let a: Animal := create Dog.make()
print(a.speak())

The binding type-checks because Dog conforms to Animal by (C-Inherit), so a Dog may stand where an Animal is expected; the access a.speak() elaborates to String. (At run time it prints woof: the call dispatches on the object’s actual class, Section 5.4.)

(C-Inherit) makes no distinction between a Nex parent and an imported host interface or class (Section 4.9): the latter is a class type like any other in \(\Sigma\), so a class implementing a host interface conforms to it, and a class extending a host class conforms to that class, exactly as Dog conforms to Animal above. A value of such a class may therefore be bound to a variable typed by the host interface or class it inherits, whether or not the surrounding code lies within a with "java" block (Section 5.8).

There are exactly two numeric types, \(\texttt{Integer}\) and \(\texttt{Real}\), and a widening chain \(\texttt{Integer} \preceq \texttt{Real}\) is not assumed here as a conformance; numeric conversions in Nex are explicit except where the standard environment provides a coercion. The one implicit numeric rule the language relies upon is that integer operands are admitted where a real is required by the arithmetic of the standard environment—so that \(\texttt{Integer} \sqcup \texttt{Real} = \texttt{Real}\) in rule (4.8). This is recorded with the arithmetic operators in Appendix B rather than as a conformance.

Optional types

An optional type \(\tau\,?\) is inhabited by the values of \(\tau\) together with nil. Hence \(\tau\) conforms to \(\tau\,?\), and \(\mathsf{Nil}\) conforms to every optional type; but \(\tau\,?\) does not conform to \(\tau\) (rules C-Opt, C-Nil, C-OptMono in Appendix D).

Function types

A function type conforms to another when it accepts at least the arguments the other accepts and returns at most what the other promises: its parameters vary contravariantly and its result covariantly, and the unconstrained type \(\mathsf{Fun}\) is a supertype of every function type (rules C-Fun, C-FunTop in Appendix D). The direction is the crux: for the subtype, each parameter type must be a supertype of the other’s, while the result must be a subtype. Thus a Function(a: Animal) conforms to a Function(a: Dog) — a handler for any animal may stand in wherever a dog-handler is wanted — but not the reverse.

Refinement types

A refinement type \(R\), declared declare type R = B where n: p (Section 3.5.1), conforms to its base: \(R \preceq B\) (rule C-Refine in Appendix D). Widening is therefore free—an \(R\) flows into any context that expects \(B\). The reverse direction is not a conformance: a \(B\) does not conform to \(R\), because not every \(B\) satisfies \(p\). Instead a base value enters a refinement only at a narrowing site—a binding, parameter, field, or return typed \(R\), or an explicit convert … to —where the elaboration attaches the predicate \(p\) as a contract to be checked at run time (Section 5.6). The refinement name is not erased during elaboration, so these narrowing sites remain visible to the checker; it is erased only in the value representation, where an \(R\) is exactly a \(B\). Consequently an operation on refinement values has the base type: q1 + q2 for two Quantity operands is an Integer, and is re-checked only if it flows back into a Quantity-typed target.

4.4Elaboration of Expressions

The judgement \(C \vdash e \Rightarrow \tau\) asserts that, in the static environment \(C\), the expression \(e\) is well-typed with type \(\tau\). The rules follow the grammar of Section 2.7.

Constants and variables

A literal takes the type of its scalar class — an integer literal is Integer, a real Real, and so for String, Char, and Boolean; nil has the type \(\mathsf{Nil}\); and a variable has the type \(C\) records for it (rules 4.1–4.7 in Appendix D). The constant this has the type of the current class, available in \(C\) within the body of a routine. The constant super is available there too, with the type of that class’s direct superclass—provided it has exactly one. A class declaring no inherit clause, or one naming more than one parent (Section 3.2), makes every occurrence of super within it ill-formed; the intended ancestor must then be named explicitly, as in Shape.describe (rule 4.7a in Appendix D). result has the declared return type of the enclosing routine, and is in \(C\) only there (Section 2.9).

Operators

An infix operator denotes a routine of the operand’s class. The arithmetic and comparison operators are elaborated through the signatures recorded in the standard environment; we summarise their effect. For an arithmetic operator \(\odot\) — one of + - * / % ^ — on numeric operands the result is the wider of the two operand types; comparison operators yield Boolean; the equality operators \(=\), \(/\!=\), \(==\), \(!\!=\) yield Boolean for any operands of conforming type; and the logical operators require and yield Boolean. Formally these are rules 4.8–4.10 of Appendix D, where \(\tau_1 \sqcup \tau_2\) is the wider of two numeric types; disjunction and negation are analogous to the conjunction rule.

That an infix operator denotes a routine of the operand’s class—stated at the top of this section—is meant literally, and a class may make it so for itself. Write \(\mathrm{alias}_\tau(\odot) = m\) when the class \(\tau\), or an ancestor of it, declares a one-argument routine \(m\) bound to \(\odot\) by an alias clause (Section 3.4). Where the operands of an arithmetic operator are not numeric—so that rule 4.8 does not apply—the operator elaborates as the call it abbreviates: the right operand must conform to the parameter of \(m\), and the type of the operator expression is the return type of \(m\). This is rule 4.8a of Appendix D. The numeric rule is tried first, so an alias can never displace built-in arithmetic; and where neither applies the expression is ill-typed, as before.

Member access and calls

A member access \(e.f\) requires that the static type of \(e\) be a class type possessing an accessible field or routine named \(f\). If \(f\) is a field, its type is the result; if \(f\) is a nullary routine, its return type is the result; if \(f\) is applied to arguments, the argument types must conform to the parameter types of the routine.

Field access \(e.f\) has the field’s type (rule 4.11 in Appendix D); the call rule is the keystone of the chapter:

class Counter
  create make() do count := 0 end
  feature
    count: Integer
    bump(n: Integer): Integer do result := count + n end
end

let c := create Counter.make()
print(c.bump(5))

The receiver c has type Counter, the routine bump takes one Integer and returns one, and the argument 5 conforms; so by (4.12) the call c.bump(5) elaborates to Integer (and evaluates to 5). An argument of the wrong type, or the wrong number of arguments, is rejected here.

The accessibility condition is that \(f\) is not declared in a private feature section of \(A\), unless the access occurs textually within \(A\). A bare call \(m(e_1,\dots,e_n)\) is elaborated as a call on this if \(m\) is a routine of the current class, and otherwise as a call of the free function \(m\) (Section 4.8).

Object creation

The expression create \(A[\bar\tau].k(e_1,\dots,e_n)\) requires that \(A\) be a non-deferred class, that \(k\) be one of its constructors, and that the arguments conform to \(k\)’s parameters; its type is \(A[\bar\tau]\). When the constructor and argument list are omitted, \(A\) must have a constructor taking no arguments, or none at all. The type of the expression is the class type created (rule 4.13 in Appendix D).

Conditional and anonymous-function expressions

The conditional expression requires a boolean condition and two branches; its type is the join—the least common supertype—of the branch types, written \(\tau_1 \sqcup \tau_2\) and always defined because \(\mathsf{Any}\) is a top. An anonymous function fn… has the function type built from its parameter and result types, its body checked under the parameters (rules 4.14–4.15 in Appendix D).

4.5Elaboration of Statements

A statement is elaborated by the judgement \(C \vdash \mathit{stmt} \Rightarrow C'\), producing a possibly extended environment \(C'\); a statement that binds no new name produces \(C\) unchanged. A block is elaborated by threading the environment through its statements.

let x: Integer := 10
if x > 5 then
  let y: Integer := x * 2
  print(y)
else
  print(0)
end

The let extends the environment with \(x : \texttt{Integer}\) by (4.16), and that environment is threaded into the if; the then block extends it further with \(y\), which is in scope only within the block (it does not leak to the statements after the if). Assignment requires the value to conform to the variable’s type and leaves the environment unchanged; the if checks each branch under the environment it is given (rules 4.17–4.18 in Appendix D).

Self- and mutually recursive closures

Rule (4.16) has one exception, symmetric with §4.8’s treatment of free functions: when \(e\) is itself an anonymous function fn…, \(x\) is bound in the environment under which \(e\) is elaborated, not withheld from it.

let fact: Function(n: Integer): Integer := fn(n: Integer): Integer do
  if n <= 1 then
    result := 1
  else
    result := n * fact(n - 1)
  end
end
print(fact(5))                       -- 120

A closure so bound may therefore call itself, exactly as a named function already could under §4.8. The same widening extends to a run of consecutive closure-literal lets within one block: every name so introduced is added to the environment together, before any of their bodies is elaborated, so two or more such closures may call one another regardless of which is written first—the closure-literal analogue of §4.8’s “any function may call any other regardless of textual order,” needing no declare function-style forecast because the whole run is elaborated as one unit.

let is_even := fn(n: Integer): Boolean do
  if n = 0 then result := true else result := is_odd(n - 1) end
end
let is_odd := fn(n: Integer): Boolean do
  if n = 0 then result := false else result := is_even(n - 1) end
end
print(is_even(10))                   -- true

This widening is withdrawn—falling back to the ordinary rule (4.16), under which the name is simply not yet visible—for any name that is also introduced a second time within reach of the closures involved: by another let in the same block, or as a parameter of one of the closures themselves. A program that relies on self- or mutual reference should therefore give each such closure, and every name it closes over, a name found nowhere else in the enclosing block.

A let with no type annotation takes \(\sigma\) to be the inferred type \(\tau\) of its initialiser. The premise “\(x\) not a once field outside a constructor” in (4.17) is the static enforcement of immutability: assigning a once field anywhere but in a constructor of its class is rejected. The loop, case, match, across, and do/rescue statements elaborate their constituent blocks under the environment extended with any variable they introduce (the cursor variable of across, the bound variable of a match clause), and produce the original environment: a block does not leak its locals to the statements that follow it.

Type dispatch and exhaustiveness

A match on an expression of class type \(A\) dispatches on the runtime class. Each clause when \(B\) as \(x\) then \(\mathit{block}\) requires \(B \preceq A\) and elaborates its block with \(x\) bound to \(B\) (rule 4.19 in Appendix D). A destructuring clause when \(B(\ldots)\) additionally binds each named field of the matched variant in the block, at that field’s declared type; a guard if \(g\) requires \(g\) to elaborate to Boolean in the scope of those bindings.

When \(A\) is sealed, the set of clause classes must exhaust \(\mathit{subclasses}(C, A)\), unless an else clause is present to cover the remainder. A clause class is identified by the declaration \(C(B)\) it names, not by the spelling \(B\) is written with: a clause naming a variant by its qualified name (Section 4.2.1) covers the same member of \(\mathit{subclasses}(C, A)\) a bare-named clause for it would, never an additional one. A missing variant is a compile-time error. A clause that can fail after its class matches—one carrying a guard, a literal field, or a nested pattern—does not count toward this coverage, since it may fall through; a variant whose only clause is so qualified therefore still requires an unguarded clause, a wildcard, or an else. This exhaustiveness check is the whole purpose of the sealed modifier, and is why a sealed class is required to be deferred (Section 4.9).

Type conversion

The form convert \(e\) to \(x{:}\sigma\) is a boolean expression that attempts a downward or upward cast: it succeeds, binding \(x\) of type \(\sigma\), when the runtime type of \(e\) is related to \(\sigma\) (a supertype or subtype), and otherwise yields false with \(x\) bound to nil. Statically it requires that the type of \(e\) and \(\sigma\) be related by conformance in one direction or the other; the form has type Boolean and binds \(x : \sigma\,?\) (rule 4.20 in Appendix D).

4.6Contract Formation

Every assertion—in a require, an ensure, an invariant, a loop invariant, or an assert—must elaborate to Boolean. A precondition is elaborated in the environment of the routine’s entry (parameters and fields in scope); a postcondition in that environment extended with result and with the old forms; an invariant in the environment of the class’s fields. An assert is elaborated in the environment holding at the point it appears, which is the environment of an ordinary statement in that body; the bare form, carrying no label, is elaborated exactly as the named one.

Every assertion must elaborate to Boolean (rule 4.21 in Appendix D). The keystone is the typing of old, which is admitted only in a postcondition and whose operand is elaborated over the fields of the current object alone. Writing \(C^{\mathsf{fields}}\) for the environment holding just those fields — the one an invariant elaborates in — the operand \(e\) may be any expression well-typed there, and old \(e\) carries its type:

class Counter
  create make() do count := 0 end
  feature
    count: Integer
    bump()
    do
      count := count + 1
    ensure
      advanced: count = old count + 1
    end
end

let c := create Counter.make()
c.bump()
print(c.count)

The postcondition advanced elaborates because count is a field of the current class, so old count has type Integer by (4.22); the assertion as a whole is Boolean by (4.21). At run time old count is the value held on entry, so after one bump the count is 1 and the postcondition holds. The operand need not be a bare field: old items.length elaborates just as well, since every name it reads is a field, and its value is the length the collection had on entry (Section 5.6). Writing old on a parameter, or outside an ensure, is a compile-time error.

Rule (4.22) records the restriction of Section 2.9: beneath old only the fields of the current object are in scope — not the parameters, the locals, or result — and old itself may stand only within a postcondition (the superscript \(\mathsf{ensure}\) marks that environment). The label of an assertion has no effect on its type; it is carried into the dynamic semantics solely to name the condition in a violation report.

4.7Generic Elaboration

A generic class \(A[\alpha_1{\to}K_1,\dots]\) is elaborated once, with its parameters \(\alpha_i\) added to \(\Delta\) and constrained so that any actual argument must conform to \(K_i\). An application \(A[\tau_1,\dots,\tau_n]\) is well-formed when each \(\tau_i\) conforms to the constraint \(K_i\) of the corresponding parameter; its fields and routine signatures are those of \(A\) with \(\tau_i\) substituted for \(\alpha_i\) throughout.

A constraint is not merely a gate on the actual argument; it is what the body of the generic may rely on. Within the scope of \(\alpha \to K\), a value of type \(\alpha\) has the features of \(K\): its fields may be read and its routines called, and the call is elaborated against \(K\)’s signature. A routine deferred in \(K\) may be called on an \(\alpha\) even though no implementation is known statically—the receiver’s dynamic class supplies one (Section 5.5). An unconstrained parameter has no features beyond those of Any.

function total_area[T -> Shape](xs: Array[T]): Integer do
  result := 0
  across xs as s do
    result := result + s.area()   -- area is deferred in Shape
  end
end

class Box [G]
  create make(x: G) do value := x end
  feature
    value: G
    get(): G do result := value end
end

let b: Box[Integer] := create Box.make(42)
print(b.get())

The application Box[Integer] is a well-formed type by (4.23) — the unconstrained parameter G admits any argument — and within it G stands for Integer, so get() returns an Integer. Had G carried a constraint such as [G -> Comparable], the argument would have to conform to it.

A parameter written \(?\alpha\) additionally permits \(\mathsf{Nil}\) as an argument. A generic routine is elaborated in the same way, its type parameters local to the routine. Because elaboration substitutes rather than erases, the type \(\texttt{Array[Integer]}\) and the type \(\texttt{Array[String]}\) are distinct types with distinct field and routine signatures, and a value of one does not conform to the other.

4.8Free Functions and the Static World

The free functions of a program are elaborated together with its classes, so that any function may call any other regardless of textual order — this alone is what admits mutual recursion among them, needing no forecast of a callee’s signature ahead of its own definition. A bare application \(m(e_1,\dots,e_n)\), where \(m\) is not a routine of the current class, is elaborated against the signature of the free function \(m\), gathered from wherever in the program \(m\) is defined. A declare function signature (Section 3.4) is a separate, optional device: it pins \(m\)’s signature explicitly, at the point a reader (or a much later definition) most wants to see it, and its later definition must then match it exactly — a self-check on the declaration, not a precondition for calling \(m\) before that definition is reached. Free functions, unlike methods, may not be overloaded: each free function name is meant to be unique, and a definition matching an earlier declare function must agree with it in full. Both rules are enforced: a repeated definition, and a definition whose signature disagrees with its declaration, are each rejected, naming the function.

4.8.1Qualified Calls and Ambiguous References

The collision Section 4.2.1 describes among classes can arise among free functions too: two units interned into the same program may each declare a function under the same bare name. A bare name \(m\) that no routine of the current class and no function declared directly in the current unit supplies is well-defined only when at most one interned unit declares a free function of that name; when more than one does, \(m\) is an ambiguous reference, and \(m(e_1,\dots,e_n)\) is rejected wherever it is written, before the call rule of Section 4.8 is ever reached. A function declared directly in the current unit is, like a class, never part of such an ambiguity: it shadows an interned function of the same bare name outright.

Unlike a class, a free function has no qid spelling to fall back on (Section 3.6.2). The escape is instead a qualified call, \(p.m(e_1,\dots,e_n)\), written in the ordinary member-access/call form of Section 2.7—syntactically the same as a method call on a variable named \(p\). It is elaborated by this rule, rather than by (4.12), precisely when \(p\)’s leading identifier is undefined in \(\Gamma\) and names no class in \(\Sigma\): an ordinary binding of that name always takes precedence, exactly as a class declared in the current unit always takes precedence over a same-named interned one (Section 4.2.1). Only once that binding is confirmed undefined does \(p.m(e_1,\dots,e_n)\) elaborate as a call to the free function whose interned unit path and own name, joined by ., spell \(p.m\): the argument types must conform to that function’s parameters, and the type of the expression is its return type, exactly as for the ordinary call of Section 4.8. A multi-segment chain (a.b.m(…)) is resolved the same way, against the one dotted name its own .-structure spells: everything before the final, argument-bearing step is the unit path, unambiguously, since the syntax of Section 2.7 admits no other member-access boundary for a chain to have split at.

4.9Well-Formedness of Classes

Beyond the typing of expressions, a program must satisfy conditions on its class structure. These are checked once, over the whole static world.

• Acyclic inheritance. The relation “\(A\) inherits \(B\)” must be acyclic; its reflexive-transitive closure is the conformance among class types of (C-Inherit).
• Attachment (void safety). Every constructor of a class must leave each of the class’s fields attached—holding a value of its declared type rather than nil—unless the field is of an optional type \(\tau\,?\), which admits nil. A constructor that returns with a non-optional reference field still unattached is rejected. Scalar fields are attached by their zero value and so need no explicit assignment; optional fields are attached to nil by default. It is this discipline that makes the absence of a rule for nil-dereference (Section 5.3) a guarantee rather than a hazard: a non-optional reference is never observed to be nil.
• Conformant overriding. When \(A\) inherits \(B\) and redefines a routine \(m\) of \(B\), the signature of \(A\)’s \(m\) must conform to that of \(B\)’s \(m\) under (C-Fun): each parameter may be widened but not narrowed (contravariant), and the return may be narrowed but not widened (covariant). A field of \(B\) may not be redeclared with a non-conforming type. This is checked at the override; a routine that narrows a parameter or returns a non-conforming type is rejected there, naming the routine and the offending position.
• Complete deferral. A non-deferred class must supply a body for every routine declared deferred in any of its ancestors; a class with an unimplemented deferred routine is itself deferred and may not be instantiated.
• Host-type conformance. When a parent named in inherit is an imported host interface or class rather than a Nex class, the inheriting class must supply a routine for every member the host type declares without an implementation—matched by name and parameter count against the host type’s own declaration of it, spelled exactly as the host declares it, since no correspondence between Nex’s naming convention and the host’s is assumed. This is the host-facing analogue of Complete deferral above, and is checked the same way: a class missing such a routine is rejected, naming the member it fails to supply.
• Single host-class extension. At most one parent named in a class’s inherit—counting the whole ancestor chain—may name a concrete (non-interface) host class; a second is rejected. A host platform’s object model may permit only single extension of a concrete class, and this condition holds regardless of which platform a given implementation targets.
• Host superclass construction. A class that extends a concrete host class by the previous condition must, in each of its own constructors, either open with a call to the host superclass’s own constructor—super.new(…), or the parent named explicitly in place of super, as the constructor’s first statement and nowhere else—or declare no such call at all, in which case the host superclass must itself be constructible with no arguments. The first form must name an argument list the host superclass actually accepts, by argument count. new is reserved for this one purpose when the target is a host superclass; it is otherwise an ordinary identifier (Section 5.8).
• Sealed implies deferred. A sealed class must be deferred. Were a sealed class instantiable, a bare instance of the parent would be a runtime value that an exhaustive match over the parent’s subclasses (4.19) would fail to cover; requiring deferral removes that value and so keeps exhaustiveness meaningful.
• Once discipline. A once field is assigned only in constructors of its class (the premise of (4.17)).

A program all of whose phrases elaborate, and all of whose classes are well-formed, is statically valid. The dynamic semantics of the next chapter is defined only for statically valid programs.