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, 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. It carries its class—needed for dynamic dispatch, for match, and for convert—and a map from field names to values. 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 updated to \(v\); and \(s + \{\ell \mapsto o\}\), for \(\ell\) fresh, is \(s\) extended with a new object \(o\).

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, and so, standing alone, does super—the same object, since there is only one (rules 5.1, 5.3, 5.3a in Appendix D). The two differ once a member access follows: super.f and super.m(…) resolve against the direct superclass rather than the object’s own class, as Section 5.4 makes precise. 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. Equality comes in two kinds. Value equality \(=\) compares contents: two collections are equal when their elements are equal; two objects, 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. An operator evaluates both operands, threading the store, and applies the operation their classes associate with \(\odot\) (rule 5.4 in Appendix D).

When that association 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).

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. The 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\) of the object at the reference \(e\) denotes. The safe access \(e\,?.f\) yields nil when \(e\) is nil and reads the field 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.

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:

super.m(e_1,\dots,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.

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.

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. 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 the constructor 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; once 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,\dots,e_n), resolved from the enclosing class exactly as rule 4.7a requires:

Unlike (5.11), this rule allocates nothing—\(\ell\) already denotes the object under construction, reached through the same this binding the delegating constructor runs in—and checks no class invariant. 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. 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.

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 old \(f\) the current value of the field \(f\) 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 true, the value passes through unchanged (there is no wrapper, since \(R\) is represented as its base); if 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. Like every contract, these checks are elided under skip-contracts, after which a refinement value is indistinguishable from an ordinary value of its base type.

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 convert form attempts a cast and binds its variable to the converted value or to nil, yielding the boolean that the surrounding context (an if, say) may test.

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.

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.