Dynamic Semantics

The dynamic semantics describes what a statically valid program does when it is evaluated. Its judgements relate a phrase, against a background of bindings and a store, to the value it produces and the store it leaves behind. Where the static semantics abstracted away from values and kept only their types, here the types fall away and the values themselves take the stage.

5.1Values and Objects

A value is what an expression evaluates to. The values of Nex are:

• scalars—integers (including the fixed-width integers Byte, Integer16, and Integer32), reals, characters, booleans, and strings—each an immutable value of the corresponding scalar class;
• the null reference nil;
• object references, written \(\ell\): pointers into the store at which mutable objects—instances of user classes, arrays, maps, sets, tasks, and channels—reside;
• closures, the values of anonymous and named functions, pairing a parameter list and body with the bindings of definition.

An object is a mutable record held in the store, shaped by its class’s inherit clause the way the class itself is. It carries three things: its class (needed for dynamic dispatch, for match, and for convert); a map from the names of the fields its class declares directly to their values; and, for each parent named in that inherit clause, a reference to a further object, of that parent’s own shape, held at its own place in the store.

A field the class only inherits is never in this map. It lives in one of these nested objects, found by following the chain of parent references down to whichever one declares it (formalised as home, Section 4.9).

Two of a class’s parents can independently trace back to one further common ancestor, but they do not converge onto a single nested object for it. Composition follows the inherit graph outward from the object itself without ever rejoining, so each parent traces to its own separately allocated copy (Section 4.9, Repeated inheritance and shared ancestors). A write through one copy is never observed through the other.

This is why the object is a tree of nested objects, one per composition level, rather than a single flat record: acyclic inheritance (Section 4.9) guarantees the tree terminates, and the absence of rejoining guarantees no level is shared.

Scalars and nil are not objects and are not stored. Two scalar values are identical exactly when they are equal, which is why == and = coincide on them (Section 5.4).

5.2The Dynamic Environment

Evaluation takes place against a dynamic environment consisting of

• a set of bindings \(E\), mapping each identifier in scope to a value (or, for an assignable local or field, to the value it currently holds); these bindings also record the current object, the value of this, and within a routine with a result, the cell result;
• a store \(s\), mapping object references to objects.

We write \(E(x)\) for the value bound to \(x\), \(E\langle x \mapsto v\rangle\) for \(E\) with \(x\) rebound to \(v\), and \(E + \{x \mapsto v\}\) for \(E\) extended with a new binding.

For the store, \(s(\ell)\) is the object at \(\ell\). \(s\langle \ell.f \mapsto v\rangle\) is \(s\) with the field \(f\) of that object’s own map updated to \(v\) — a field the object holds directly, never one reached through a nested parent. And \(s + \{\ell \mapsto o\}\), for \(\ell\) fresh, is \(s\) extended with a new object \(o\).

Reaching a field an object only inherits means stepping through its nested parents first. Write \(\pi\) for a path, a sequence of parent names \(P_1 \cdots P_n\) (the empty path is \(\varepsilon\)), and define

This gives the reference reached by following \(\pi\)’s parent names, one nested object at a time, from \(\ell\).

\(\mathit{follow}(s,\ell,\varepsilon) = \ell\) is why an object with nothing to inherit, or a field it declares itself, needs no path at all: every rule below that reads or writes a field specialises to the familiar direct case (\(s(\ell).f\), \(s\langle \ell.f \mapsto v\rangle\)) exactly when the path involved is empty.

The principal judgement of the chapter is

Statements are evaluated by the analogous judgement \(s, E \vdash \mathit{stmt} \Rightarrow E', s'\), which may extend the bindings (with a new local) and alters the store. Evaluation may also terminate exceptionally; that mode is treated in Section 5.7. Because Nex is deterministic and sequential apart from explicit tasks (Chapter 6), the store is threaded strictly left to right through every rule.

5.3Evaluation of Expressions

Constants, variables, and the current object

A constant denotes its value and leaves the store untouched. this yields the current object (rule 5.1 in Appendix D). super and an explicit ancestor name do not, because each of an object’s inherited parts is its own nested object (Section 5.1).

Standing alone, super yields the current object’s own nested copy of its direct superclass — a genuinely different reference, one hop into \(\mathit{parents}\). A named ancestor \(P\) yields whichever nested copy \(\mathit{reach}\) (Section 4.9) finds, possibly several hops in when \(P\) is not a direct parent (rules 5.3a, 5.3b in Appendix D).

This is what makes super.f/super.m(…) and P.f/P.m(…) need no rules of their own beyond this: once super or \(P\) has evaluated to that nested reference, the ordinary member-access and call rules of Section 5.4 apply to it exactly as they would to any other reference. They resolve against the direct superclass, or the named ancestor, simply because that is now the object standing on the left of . — not because .f or .m(…) behave any differently.

All these nested objects belong to the one enclosing create, allocated and released together (Section 5.5), and never independently reachable from outside it. That is the sense in which there is still only one object, even though this and super are not, at the reference level, the same value.

A variable is looked up in the bindings:

The lookup walks the chain of enclosing scopes, so that a name resolves to its nearest binding (Section 5.8 on shadowing).

Operators

An arithmetic or comparison operator evaluates its operands left to right and then applies the operation of the operands’ class. An operator evaluates both operands, threading the store, and applies the operation their classes associate with \(\odot\) (rule 5.4 in Appendix D).

Equality comes in two kinds. Value equality \(=\) compares contents: two collections are equal when their elements are equal, and two objects are equal by the equals routine of their class, which user classes may override. Identity equality \(==\) compares references: two object values are identical exactly when they are the same reference \(\ell\). On scalars the two kinds agree.

When the association with \(\odot\) is one the programmer made — an arithmetic operator bound to a routine by an alias clause (Section 3.4) — the operator is the call. Having evaluated the operands, the operation proceeds exactly as the call \(v_1.m(v_2)\) would: the receiver’s dynamic class selects the implementation, the routine’s precondition is checked on entry and its postcondition on exit, and its rescue clause governs a failure within it. Nothing about an operator makes it a cheaper way into a routine than its own name. This is rule 5.4c of Appendix D.

let owed: Money := create Money.make(100, "USD")
let paid: Money := create Money.make(30, "EUR")
print(owed - paid)      -- Precondition violation: same_currency

let a: Integer := 7
let b: Real := 2.0
print(a + b)

The operands have different numeric classes; the Integer is admitted where a Real is wanted, the sum is taken as a Real, and the value printed is 9.0. This widening is the one implicit numeric coercion of the language (Section 4.3).

let b: Byte := 200u8
print(b + b)

An operand of a fixed-width type is first replaced by the Integer that has the same value, and the operation proceeds on Integer operands, so the sum is the Integer 400. The result is never a fixed-width value, and an operation cannot overflow the narrow type; the range of Byte, Integer16 or Integer32 is checked only where a value is converted back into one (§B.3). The operands of the equality operators are not replaced: a value of a fixed-width type equals only a value of its own type with the same number, so the Byte 65u8 is unequal to the Integer 65.

On Integer operands the operation is checked. Write \(\odot_{\mathbb{Z}}\) for the exact operation in \(\mathbb{Z}\); rule (5.4) applies precisely when its result lies in range. An arithmetic operation whose exact result overflows the 64-bit range raises Arithmetic_Overflow, and integer division or remainder by a zero divisor raises Division_by_Zero (rules 5.4a, 5.4b in Appendix D; §B.3).

On Real operands the operation is total: division by zero is not exceptional, but yields the IEEE 754 value \(\pm\infty\) or NaN through \(\widehat\odot\) in rule (5.4), as §B.3 records. This asymmetry — integer division by zero raises, real division by zero does not — is deliberate, and holds on every back end.

Short-circuit conjunction and disjunction

The operators and and or are not evaluated by (5.4): their second operand is evaluated only conditionally. This holds in every back end of Nex and is part of the language’s definition, not an optimisation. When \(e_1\) is false, \(e_1\) and \(e_2\) is false and \(e_2\) is never evaluated; otherwise the result is \(e_2\) (rules 5.5, 5.6 in Appendix D).

Disjunction is dual: in \(e_1\) or \(e_2\), the operand \(e_2\) is evaluated only when \(e_1\) is false. A consequence is that a guard such as x /= nil and x.f never evaluates x.f when x is nil, and is therefore safe.

Member access and the safe access

An ordinary access \(e.f\) reads the field \(f\) belonging to the object at the reference \(e\) denotes: its own, if \(e\)’s static type declares \(f\) directly, or otherwise the one held in whichever of its nested objects does (Section 5.1), found by following \(f\)’s home (Section 4.9) one composition level at a time.

The safe access \(e\,?.f\) yields nil when \(e\) is nil, and reads the field the same way otherwise (rules 5.7–5.9 in Appendix D).

An ordinary access \(e.f\) on a nil receiver has no rule: it raises an exception (Section 5.7). The safe access \(e\,?.f\) instead yields nil, which is why its static type is optional (Section 4.4).

5.4Calls and Dynamic Dispatch

A method call evaluates the receiver and the arguments, selects the routine by the runtime class of the receiver and the number of arguments, and evaluates its body in fresh bindings for the parameters and this.

this, there, is not always the receiver reference itself. When \(m\) is inherited rather than declared or overridden by the receiver’s own class, its body is text that belongs to whichever ancestor does declare it. A routine’s own this always names the class its text belongs to (Section 5.3), so the body runs against that ancestor’s own nested object, found the same way a field would be (\(\mathit{home}\), Section 4.9).

When \(m\) is declared or overridden by \(\mathit{class}(o)\) itself, \(\mathit{home}(\mathit{class}(o), m) = \varepsilon\) and \(\ell' = \ell\): dispatch reduces to running \(m\)’s body against the receiver directly, exactly as before.

class Shape
  create make() do end
  feature
    area(): Real do result := 0.0 end
end

class Square
  inherit Shape
  create make(s: Real) do side := s end
  feature
    side: Real
    area(): Real do result := side * side end
end

let sh: Shape := create Square.make(3.0)
print(sh.area())

Although sh has static type Shape, the object it denotes is a Square; \(\mathit{lookup}\) in (5.10) selects on \(\mathit{class}(o)\), so Square’s area runs and the result is 9.0, not 0.0. This is dynamic dispatch.

Three features of this rule deserve note.

The routine is chosen by \(\mathit{class}(o)\), the class of the actual object, not by the static type of \(e\): this is dynamic dispatch, and is how an overriding routine in a subclass takes effect.

The selection also depends on \(n\), realising overloading by arity (Section 4.4).

And \(E_0\) is the bindings of the routine’s definition extended with the parameter bindings — not the caller’s bindings — so a routine sees the fields of its object and its own parameters, and nothing of the caller’s locals.

The return value \(\mathit{ret}\) is the final contents of the result cell for a routine that declares a result, and the distinguished void value otherwise. A free-function call \(m(e_1,\dots,e_n)\) and the application of a closure are evaluated likewise, the closure supplying its captured bindings in place of \(E_0\).

Calling a named ancestor, and calling through super

A call may name its target class outright — Shape.describe, say, from within a subclass — rather than reaching it through a receiver expression. Such a call selects m from the named class \(P\) directly, on the current object, whatever that object’s own class is. It runs with this rebound to \(P\)’s own nested object (one hop into \(\mathit{parents}\), then \(\mathit{home}(P,m)\) further if \(P\) only inherits \(m\) in turn). That way, a bare field read inside \(m\)’s own body resolves against \(P\)’s own copies, not the current object’s outer ones:

super.m(e_1,...,e_n) is the same rule with \(P\) supplied implicitly rather than written: if the call occurs within the body of a routine declared in class \(A\), where — as rule 4.7a requires — \(A\) inherits exactly one class, \(P\) is that class.

Either way, the routine is selected from \(P\), not from the class of the current object: the opposite of (5.10)’s dynamic dispatch. \(\ell'\) is exactly what evaluating super or \(P\) alone would give (rules 5.3a, 5.3b). This rule could equally be read as evaluating the target first and then dispatching by (5.10) — it is just stated directly, the same way (4.16′) restates a special case of (4.16) rather than deriving it.

class Shape
  create make(c: String) do colour := c end
  feature
    colour: String
    describe(): String do result := colour end
end

class Square
  inherit Shape
  create make(c: String, s: Real) do
    super.make(c)
    side := s
  end
  feature
    side: Real
    describe(): String do result := super.describe + ", side " + side.to_string end
end

let sq := create Square.make("blue", 3.0)
print(sq.describe())

Square.make delegates to Shape.make (rule 5.11a, next section) to initialise colour before setting side itself; then describe calls super.describe, which by (5.10a) selects Shape’s describe—not Square’s own, which would simply call itself again—and appends to its result. The call prints "blue, side 3.0".

\(P\) is fixed once and for all by the class whose text contains the super occurrence, not by \(\mathit{class}(o)\) as in (5.10). This is what keeps it correct under inheritance: if a further subclass Cube inherited Square without overriding describe, calling cube.describe() would still run Square’s version by ordinary dynamic dispatch (5.10) — and that version’s own super.describe would still resolve to Shape, the ancestor its author meant, regardless of how far below Square the actual object sits.

A class inheriting more than one parent, or none, makes super ill-formed by (4.7a) before evaluation is ever reached. The intended ancestor must then be named explicitly, as Flyable.fly() does by the same rule (5.10a), with \(P\) written rather than resolved.

When \(P\) is an imported host interface or class (Section 3.6) rather than a Nex class — a class extending it, per the conditions of Section 4.9, may call it this way — (5.10a) again applies, with \(\mathit{lookup}(P, m, n)\) selecting the host’s own implementation of \(m\) rather than a Nex routine.

The point of this, as with the ordinary case above, is that the selected routine is fixed by \(P\), not by \(\mathit{class}(o)\). If the current class overrides \(m\) itself — so that its own routine occupies the same name that dynamic dispatch (5.10) would otherwise select on \(o\) — a call through super still reaches the host’s implementation, never recursing back into the override.

A call to a member the current class does not itself define needs no such distinction, and may be written on an ordinary receiver, o.m(…), resolving under (5.10) to the host’s implementation because no Nex override exists to compete with it.

5.5Object Creation and Constructors

Creation allocates a fresh object, gives each field its initial value, runs the named constructor, checks the precondition of the constructor and the class invariant, and yields the new reference.

Giving each field its initial value means building the whole nested shape at once (Section 5.1), not just \(A\)’s own fields: one further object, of its own shape, per parent named in \(A\)’s inherit clause, recursing the same way into their parents, all the way down (\(\mathit{initial}\), in Appendix D, spells this out).

Within each of these objects the initial value of a field is nil for an optional field, and the zero value for a field of scalar type. A non-optional reference field has no such default: by the attachment rule of Section 4.9, some constructor along the way must itself assign it, so that the object is fully attached when creation completes.

class Account
  create make(b: Real) do balance := b end
  feature
    balance: Real
  invariant
    non_negative: balance >= 0.0
end

let acct := create Account.make(100.0)
print(acct.balance)

Creation allocates a fresh object, runs make to set balance, then checks the invariant non_negative at the new reference before yielding it; the value printed is 100.0. Had the constructor left balance negative, (5.11) would raise a contract-violation at creation rather than return an inconsistent object.

A constructor may assign the once fields of its class; and after the constructor returns, those fields are fixed for the life of the object (Section 4.5 enforces this statically, and the store offers no rule to reassign them). When the create form names no constructor, an object with default field values is produced and only the invariant is checked.

Delegating to a named or superclass constructor

A constructor may call another constructor on the object already under construction, rather than allocating a new one — most often the superclass’s, to initialise the fields it declares before the subclass’s own constructor sets the rest.

As with (5.10a), the target class \(P\) may be named outright, or supplied implicitly by super.k(e_1,...,e_n), resolved from the enclosing class exactly as rule 4.7a requires. The static rule is (4.13a) in Section 4.4, which additionally requires \(P\) to declare \(k\) itself, unlike (5.11)’s own \(\mathit{constructors}(A)\).

\(P\)’s own object already exists — (5.11) allocated it, nested, when the outermost create began — so delegation just runs \(k\) with this switched to it:

Unlike (5.11), this rule allocates nothing: \(\ell'\), \(P\)’s own nested object, was already built by (5.11) when the outermost create began, one hop from \(\ell\) into \(\mathit{parents}\). It also checks no class invariant.

Running \(k\) with this switched to \(\ell'\) is why a bare field \(k\) assigns is attached on \(P\)’s own object, not the subclass’s outer one: the field lives there (Section 5.1), and by the time \(k\)’s own text runs, this names exactly the class that text belongs to, as it always does (Section 5.3).

The invariant checked is the outermost create’s own, by rule (5.11), once, when that constructor returns. By then every delegated constructor reached along the way, super-qualified or named outright, has already run, each against the specific nested object it was meant to attach. In the Square example above, this is exactly why super.make(c) is safe to run before side is set: no invariant is checked until Square.make itself returns, with both fields in place.

When a class extends a concrete host class rather than a Nex one (Section 4.9), delegation reaches the host’s own constructor instead of a named Nex one, and \(k\) is written new — a name reserved for exactly this purpose when \(P\) is such a host class, and an ordinary identifier everywhere else.

Two differences from (5.11a) follow from \(P\) naming a host constructor rather than a Nex one. First, the call must be the delegating constructor’s first statement: the host platform’s own object model requires the superclass’s construction to complete before anything else touches the object under construction, a requirement (5.11a) does not impose on delegation among Nex constructors, whose fields all begin at their default values regardless of ordering. Second, \(k\) is selected from the host constructors by argument count alone, since a host constructor’s parameters are not elaborated as Nex types (4.9).

When the delegating constructor contains no such call, one is supplied implicitly, with \(n = 0\) — which requires the host class to provide a constructor taking no arguments, precisely as (4.9)’s host superclass construction condition states.

5.6Contract Checking

Contracts are checked as the program runs, and their violation is an exceptional event distinct from an ordinary error. The auxiliary \(\mathit{check}(a)\) evaluates the assertion \(a\); if it yields true, evaluation proceeds; if false, a contract-violation exception is raised, carrying the assertion’s label and its position so that the failure can be reported as which condition failed on which line.

For a routine \(m\) with precondition \(\mathit{pre}\), postcondition \(\mathit{post}\), and enclosing class invariant \(I\):

• \(\mathit{pre}\) is checked on entry, after the parameters are bound but before the body runs; a failed precondition is the caller’s fault.
• The old expressions of \(\mathit{post}\) are snapshotted on entry: for each field an old expression reads, the current value of that field is recorded, to be supplied when \(\mathit{post}\) is later evaluated.
• \(\mathit{post}\) is checked on normal exit, with result bound and the recorded old values in scope; a failed postcondition is the routine’s fault.
• \(I\) is checked on exit from every routine and constructor that can be called from outside the object, so that an instance is consistent whenever it is observable.

class Account
  create make() do balance := 0.0 end
  feature
    balance: Real
    withdraw(amount: Real)
    require
      enough: amount <= balance
    do
      balance := balance - amount
    end
end

let acct := create Account.make()
acct.withdraw(50.0)

The precondition enough is checked on entry to withdraw, after amount is bound. Here the balance is 0.0, so the assertion is false and \(\mathit{check}\) raises a contract-violation that names the failing condition — reported as Precondition violation: enough. A failed precondition is the caller’s fault, and the label is what makes the report point to the cause.

The clauses above all speak at a boundary: entry, exit, or the span of a loop. The assert statement speaks at a point within a body, where no clause can reach. Executing assert applies \(\mathit{check}\) to each of its assertions in source order; the first that yields false raises a contract-violation and the statement does not complete, and if all yield true the statement completes normally with no effect on the store. The named form supplies the label \(\mathit{check}\) reports; the bare form supplies none, and the position stands in its place:

assert non_empty: items.length > 0   -- Assertion violation: non_empty
assert i < n                          -- Assertion violation (line 42)

A failed assert is a contract-violation of the same kind as a failed require or ensure, and is caught by a rescue on the same terms. Nothing distinguishes it at the point of failure but the clause it came from.

The predicate of a refinement type is checked by the same \(\mathit{check}\) mechanism. Wherever the static semantics marked a narrowing site (Section 4.3) — a base value flowing into a binding, parameter, field, or return typed \(R\), or a convert … to \(R\) — the value under test is bound to the predicate’s binder and the predicate is evaluated.

If it yields true, the value passes through unchanged (there is no wrapper, since \(R\) is represented as its base). If it yields false, a contract-violation is raised, as for a failed require.

The one exception is convert, whose whole purpose is to test rather than assert: a failed refinement predicate there makes the convert yield false rather than raise.

5.7Exceptions: raise, rescue, retry

Evaluation of a phrase either completes normally, yielding a value and a store, or terminates exceptionally, carrying an exception value and a store. An exception propagates outward through enclosing phrases—abandoning their pending work—until a rescue clause catches it. We write the exceptional outcome \(s, E \vdash e \Rightarrow \mathbf{raise}\;w,\, s'\).

The statement raise \(e\) evaluates \(e\) to a value \(w\) and raises it. A nil dereference, a failed contract, a failed runtime argument check, and a failed convert in a context requiring success all raise built-in exception values by the same mechanism (the raise statement is rule 5.12 in Appendix D).

A scoped block do \(\mathit{block}_1\) rescue \(\mathit{block}_2\) end runs \(\mathit{block}_1\); if it completes normally, the rescue is ignored (rule 5.13 in Appendix D); if it raises \(w\), the handler \(\mathit{block}_2\) is run with exception bound to \(w\):

class Worker
  create make() do attempts := 0 end
  feature
    attempts: Integer
    run()
    do
      do
        attempts := attempts + 1
        if attempts < 3 then
          raise "transient"
        end
        print(attempts)
      rescue
        if attempts < 3 then
          retry
        end
      end
    end
end

let w := create Worker.make()
w.run()

The first two attempts raise; each time (5.14) runs the handler, which retrys — abandoning the handler and re-running the block from the top against the current store (rule 5.15 in Appendix D). On the third attempt no exception is raised and 3 is printed. retry has meaning only inside a rescue block (Section 2.9); elsewhere it is a static error.

If a handler completes without retry, the scoped block completes normally and execution continues after it; an exception raised by the handler itself propagates outward in the ordinary way.

5.8Statements and Control Flow

Local declaration, assignment, and scope

A let adds a fresh binding and a field update writes through a reference into the store (rules 5.16, 5.18 in Appendix D); assignment rebinds an existing variable to a new value:

A let introduces a new binding in a fresh scope; an assignment updates an existing one. A scoped block do…end evaluates its statements in bindings that extend the enclosing ones, so that a let inside the block shadows an outer binding of the same name and the outer binding is restored on exit—the bindings made inside a block do not escape it.

Conditionals and loops

The if statement evaluates its condition and runs the corresponding branch; the conditional expression when… is its value-producing analogue. The general loop runs its from block once, then repeatedly tests the until condition, running the body while the condition is false (rules 5.19, 5.20 in Appendix D).

let sum: Integer := 0
from let i := 1 until i > 5 do
  sum := sum + i
  i := i + 1
end
print(sum)

The from block runs once, binding i; then while i > 5 is false the body runs, each iteration rebinding sum and i in the threaded store (5.17). After i reaches 6 the loop stops and 15 is printed.

A loop may carry an invariant, checked before the body on each iteration, and a variant — an integer expression that must strictly decrease and stay non-negative across iterations, checked likewise. These are contracts on the loop: a violated loop invariant or a non-decreasing variant raises a contract-violation exception.

The counted loop repeat \(n\) do \(b\) and the cursor loop across \(e\) as \(x\) do \(b\) are derived forms, expanded in Appendix C: the former into a general loop over a counter, the latter into iteration driven by the start/item/next/at_end protocol of the Cursor class (Appendix B).

Dispatch statements

The case statement compares the value of its scrutinee against the constants of each clause, by value equality, and runs the first matching clause, or the else clause if none matches.

The match statement inspects the runtime class of its scrutinee and runs the clause whose class the object conforms to, binding the clause variable to the object; its exhaustiveness over a sealed class was guaranteed statically (4.19).

The host block

The statement with \(s\) do \(b\) end, where \(s\) is a string literal naming a host facility, is the one construct whose behaviour is conditioned on the platform beneath the implementation.

When the implementation recognises \(s\), the statements of \(b\) are evaluated with name resolution extended to that facility: a class name or call within \(b\) that resolves to no Nex entity may resolve to an entity of the host. When the implementation does not recognise \(s\), the entire block is skipped — \(b\) is not evaluated and no error arises. A program may thus carry host-specific passages that execute only where their host is present.

The JVM implementation recognises the facility "java": within the block, imported Java classes may be instantiated and their methods called by the ordinary call syntax, while a call whose receiver is a Nex value dispatches by the rules of Section 5.4 as it would outside. Unlike the scoped block do…end, the host block does not open a scope: a let within it binds in the enclosing scope and remains visible after the block.

A class’s inherit clause is a declaration, elaborated with the rest of the static world (Section 3.1) rather than evaluated as a statement. So a class implementing a host interface or extending a host class (Sections 4.9, 5.4, 5.5) is not itself written inside a host block; only the ordinary construction and manipulation of a bare host object needs one.

The two facilities may also differ in which an implementation supports. A conforming implementation must recognise every host facility it claims to, but inheriting a host interface and inheriting a host class are independent capabilities, and an implementation may support one without the other — the JVM implementation’s tree-walking interpreter, for instance, supports the former but not the latter, reporting a static error rather than approximating it.

5.9Termination

A normal evaluation of a phrase yields a value and a store; an exceptional one yields a raised value and a store; a non-terminating one—a loop that never satisfies its until, an unbounded recursion—yields nothing, and the judgement simply has no derivation. The Definition makes no claim that evaluation terminates; it says only what the result is when it does. The remaining construct of the statement grammar, spawn, begins a concurrent evaluation and is the subject of Chapter 6.