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, decimals, 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

\[ s,\,E \vdash e \;\Rightarrow\; v,\, s' \] “in the bindings \(E\) and store \(s\), the expression \(e\) evaluates to the value \(v\), leaving the store \(s'\).”

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

\[ s, E \vdash \mathit{scon} \Rightarrow \mathcal{V}(\mathit{scon}),\, s \tag{5.1} \] \[ \frac{E(x) = v}{s, E \vdash x \Rightarrow v,\, s} \tag{5.2} \qquad s, E \vdash \texttt{this} \Rightarrow E(\texttt{this}),\, s \tag{5.3} \]

Here \(\mathcal{V}\) maps a special constant to the value it denotes; a constant has no effect on the store. 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.

\[ \frac{s, E \vdash e_1 \Rightarrow v_1, s_1 \quad s_1, E \vdash e_2 \Rightarrow v_2, s_2}{s, E \vdash e_1 \odot e_2 \Rightarrow v_1 \mathbin{\widehat\odot} v_2,\, s_2} \tag{5.4} \]

where \(\widehat\odot\) is the operation the environment associates with \(\odot\) on the classes of \(v_1\) and \(v_2\).

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.

\[ \frac{s, E \vdash e_1 \Rightarrow \mathsf{false}, s_1}{s, E \vdash e_1 \;\texttt{and}\; e_2 \Rightarrow \mathsf{false},\, s_1} \tag{5.5} \qquad \frac{s, E \vdash e_1 \Rightarrow \mathsf{true}, s_1 \quad s_1, E \vdash e_2 \Rightarrow v, s_2}{s, E \vdash e_1 \;\texttt{and}\; e_2 \Rightarrow v,\, s_2} \tag{5.6} \]

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

\[ \frac{s, E \vdash e \Rightarrow \ell, s_1 \quad s_1(\ell) = o \quad o.f = v}{s, E \vdash e.f \Rightarrow v,\, s_1} \tag{5.7} \] \[ \frac{s, E \vdash e \Rightarrow \texttt{nil}, s_1}{s, E \vdash e\,?.f \Rightarrow \texttt{nil},\, s_1} \tag{5.8} \qquad \frac{s, E \vdash e \Rightarrow \ell, s_1 \quad \ell \ne \texttt{nil}}{s, E \vdash e\,?.f \Rightarrow s_1(\ell).f,\, s_1} \tag{5.9} \]

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.

\[ \frac{\begin{array}{c} s, E \vdash e \Rightarrow \ell, s_0 \quad s_0(\ell) = o \quad s_{i-1}, E \vdash e_i \Rightarrow v_i, s_i \;\;(1 \le i \le n) \\ \mathit{lookup}(\mathit{class}(o), m, n) = (x_1,\dots,x_n; \mathit{body}) \\ E' = E_0[\texttt{this} \mapsto \ell,\; x_i \mapsto v_i] \quad s_n, E' \vdash \mathit{body} \Rightarrow \mathit{ret},\, s' \end{array}}{s, E \vdash e.m(e_1,\dots,e_n) \Rightarrow \mathit{ret},\, s'} \tag{5.10} \]

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

Arguments are guaranteed by the static rule Because conformance for function types is contravariant in its parameters (Section 4.3), and overriding routines may only widen a parameter, a value reaching the selected routine through a conforming type is always of an acceptable class. Rule (5.10) therefore needs no residual argument check at the call: the safety that an Eiffel-style covariant rule would defer to a runtime test is, in Nex, established statically.

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 its declared initialiser if it has one; otherwise 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.

\[ \frac{\begin{array}{c} \ell \;\text{fresh} \quad o_0 = \mathit{initial}(A[\bar\tau]) \quad s_0 = s + \{\ell \mapsto o_0\} \\ s_{i-1}, E \vdash e_i \Rightarrow v_i, s_i \;\;(1 \le i \le n) \\ k = (x_1,\dots,x_n; \mathit{pre}; \mathit{body}; \mathit{post}) \in \mathit{constructors}(A) \\ \mathit{check}(\mathit{pre}) \quad s_n, E[\texttt{this} \mapsto \ell, x_i \mapsto v_i] \vdash \mathit{body} \Rightarrow s' \\ \mathit{check}(\mathit{post}) \quad \mathit{check}(\mathit{invariant}(A)\;\text{at}\;\ell) \end{array}}{s, E \vdash \texttt{create}\; A[\bar\tau].k(e_1,\dots,e_n) \Rightarrow \ell,\, s'} \tag{5.11} \]

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.

What old captures The snapshot of old \(f\) records the value the field held on entry. For a field of scalar or reference type this is exactly the pre-state value; but for a mutable object reached through the field, the snapshot is the reference, not a copy, so a later mutation of that object is visible through old. A postcondition that must speak of the prior size of a mutable collection should therefore record that size in a field of its own, and refer to old of that field. This is a consequence of (5.7) and the reference nature of objects, not a special rule.

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.

\[ \frac{s, E \vdash e \Rightarrow w, s_1}{s, E \vdash \texttt{raise}\; e \Rightarrow \mathbf{raise}\;w,\, s_1} \tag{5.12} \]

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

\[ \frac{s, E \vdash \mathit{block}_1 \Rightarrow E_1, s_1}{s, E \vdash \texttt{do}\;\mathit{block}_1\;\texttt{rescue}\;\mathit{block}_2\;\texttt{end} \Rightarrow E, s_1} \tag{5.13} \] \[ \frac{s, E \vdash \mathit{block}_1 \Rightarrow \mathbf{raise}\;w, s_1 \quad s_1, E[\texttt{exception} \mapsto w] \vdash \mathit{block}_2 \Rightarrow E_2, s_2}{s, E \vdash \texttt{do}\;\mathit{block}_1\;\texttt{rescue}\;\mathit{block}_2\;\texttt{end} \Rightarrow E, s_2} \tag{5.14} \]

Within a handler, the statement retry abandons the handler and re-runs \(\mathit{block}_1\) from the top, against the current store. This is the idiom for bounded retry: a handler that counts attempts and either retrys or gives up. retry has meaning only inside a rescue block (Section 2.9); elsewhere it is a static error.

\[ \frac{s, E[\texttt{exception} \mapsto w] \vdash \texttt{do}\;\mathit{block}_1\;\texttt{rescue}\;\mathit{block}_2\;\texttt{end} \Rightarrow R, s'}{s, E[\texttt{exception} \mapsto w] \vdash \texttt{retry} \;\text{within}\; \mathit{block}_2 \Rightarrow R, s'} \tag{5.15} \]

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

\[ \frac{s, E \vdash e \Rightarrow v, s_1}{s, E \vdash \texttt{let}\; x := e \Rightarrow E + \{x \mapsto v\},\, s_1} \tag{5.16} \] \[ \frac{s, E \vdash e \Rightarrow v, s_1}{s, E \vdash x := e \Rightarrow E\langle x \mapsto v\rangle,\, s_1} \tag{5.17} \] \[ \frac{s, E \vdash e_1 \Rightarrow \ell, s_1 \quad s_1, E \vdash e_2 \Rightarrow v, s_2}{s, E \vdash e_1.f := e_2 \Rightarrow E,\; s_2\langle \ell.f \mapsto v\rangle} \tag{5.18} \]

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.

\[ \frac{s, E \vdash \mathit{init} \Rightarrow E_1, s_1 \quad s_1, E_1 \vdash \texttt{loop}_{u,b} \Rightarrow E', s'}{s, E \vdash \texttt{from}\;\mathit{init}\;\texttt{until}\;u\;\texttt{do}\;b\;\texttt{end} \Rightarrow E', s'} \tag{5.19} \] \[ \frac{s, E \vdash u \Rightarrow \mathsf{true}, s_1}{s, E \vdash \texttt{loop}_{u,b} \Rightarrow E, s_1} \qquad \frac{s, E \vdash u \Rightarrow \mathsf{false}, s_1 \quad s_1, E \vdash b \Rightarrow E_2, s_2 \quad s_2, E_2 \vdash \texttt{loop}_{u,b} \Rightarrow E', s'}{s, E \vdash \texttt{loop}_{u,b} \Rightarrow E', s'} \tag{5.20} \]

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.

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.