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 (rules 5.1, 5.3 in Appendix D). 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).

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\).

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.

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.

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.