Programs

The preceding chapters define the elaboration and evaluation of the phrases of Nex. This short chapter assembles them into the meaning of a whole program: how its declarations and statements are processed, and in what order.

7.1The Two Worlds of a Program

Recall from Section 3.1 that a program is a sequence of top-level items in any order, and that these fall into two kinds. The declarations—the classes, free functions, and type aliases, together with the module links that bring further declarations into scope—form the static world. The top-level statements form the dynamic world. A program is processed by first building the static world in full, and then executing the dynamic world against it.

This order is not the textual order of the items but a reordering imposed by the Definition: every declaration is in scope throughout every other, so that classes and functions may refer to one another freely, while a top-level statement runs only after the entire static world exists. The benefit is that the programmer need not arrange declarations in dependency order, and that forward reference among classes and functions is always available.

The two worlds are not wholly sealed from one another: a function or class body may read a top-level let binding—a global—though it may not assign to one. Section 7.4 gives the rule that keeps such reads well-defined.

7.2Building the Static World

The static world is built in stages, against the standard environment \(E_0\) of Appendix B—the classes and values that exist before any user code.

1. Module links. Each import declaration adds a host class to the environment; each intern declaration elaborates the named unit—recursively, by this same procedure—and adds its declarations under the given name or alias. A unit is elaborated once however often it is interned.
2. Class and function registration. The names of all classes and all functions (including the signatures announced by declare) are entered into the class bindings \(\Sigma\), so that every later step sees every name.
3. Elaboration. Each class is elaborated—its parents resolved, its fields and routines typed, its contracts checked for well-formedness—and each function body is typed against the registered signatures. The class well-formedness conditions of Section 4.9 (acyclic inheritance, conformant overriding, complete deferral, sealed-implies-deferred) are verified here.

If any step fails, the program is rejected and nothing is executed. A program that survives all three stages is statically valid, and yields a static environment \(C\) together with the initial dynamic bindings \(E_1\) and store \(s_0\), extending the standard environment \(E_0\) with the elaborated classes and the function and constructor closures.

7.3Executing the Dynamic World

The top-level statements are then evaluated in source order, against \(E_1\), by the statement judgement of Chapter 5. The bindings thread from one statement to the next, so a top-level let is visible to the statements that follow it; the store threads likewise. The program’s observable behaviour—its output, the host effects of its imported classes, the final store—is the cumulative effect of this evaluation.

Here \(\mathit{decs}\) are the declarations of the program and \(\mathit{stmts}\) its top-level statements; the relation \(\leadsto\) is the construction of Section 7.2, \(E_1\) and \(s_0\) the initial dynamic bindings and store, and \(\Downarrow\) the evaluation of the whole program to a final store.

An uncaught exception raised by a top-level statement terminates the program; its value and position are reported, and no further statement runs. A program that spawns tasks (Chapter 6) completes when its top-level statements have been evaluated and the policy of the host for outstanding tasks has been applied; the Definition fixes the meaning of each communication but, as in Section 6.4, leaves the disposal of unawaited tasks to the realisation.

7.4Readable Globals

A top-level let binds a global. Within the static world—the body of any free function or class routine—a global is readable: an otherwise-unbound name that matches a global denotes that global’s current value. A global is not assignable from the static world; an assignment to a global inside a function or class body is a static error. Ordinary scoping still applies, so a parameter, field, or local of the same name shadows the global throughout the body in which it is bound.

Because a global belongs to the dynamic world, it holds no value until the let that binds it has executed (Section 7.3). To keep every static-world read well-defined, the Definition imposes a def-before-use watermark. Let the entry point be the first top-level statement, in source order, that transfers control into the static world—one that calls a free function or creates an instance of a user-defined class. (A method call need not be considered: its receiver must already have been created, so a create always precedes it.) The rule is:

Every global read by any function or class body must be bound by a let that stands, at top level, strictly before the entry point.

A program that violates the watermark is rejected before it runs. The rule is sound because nothing in the static world executes before the entry point, so a global bound before that point is guaranteed to hold its value at every static-world read. It is deliberately conservative: it treats all globals read anywhere in the static world uniformly, rather than tracing which body a given execution can reach. The programmer’s obligation is therefore simple—initialize the globals a program’s functions and classes depend on before the program begins calling into them.

7.5The Definition and the Implementation

The procedure of this chapter mirrors the reference interpreter, which registers imports and interns, then classes, then functions, and only then executes the top-level statements—loading the static world before running the dynamic one. That correspondence is intentional: the Definition is meant to describe the same language the interpreter implements. Where the bytecode and JavaScript back ends are concerned, they are required to reproduce the behaviour defined here; a back end that diverges is, by the project’s own rule, in error, and the divergence is a defect to be repaired rather than a second meaning to be admitted.