Introduction

This document defines Nex. It states exactly which texts are Nex programs—the grammar—and what each of those programs does—the meaning—so that questions about the language can be settled by appeal to rules rather than to examples.

Nex already has a reference manual, and for everyday programming it is the better guide: it explains each construct in prose, with a grammar alongside. But prose leaves gaps, and those gaps stand in the way of two kinds of reader. One is writing a second implementation. The other is trying to show that a program behaves as intended. Both need to know what happens when two features meet in a way no example covered, and which of two plausible readings is the right one. Closing those gaps takes a document in which the meaning of a program is not described but defined.

This Definition aims to be that document. It does not replace the tutorial or the reference; it underwrites them. Where the tutorial says what a construct is for, the Definition says what it is.

1.1Nex

Nex is a small object-oriented language with first-class functions, designed to keep the discipline of software engineering visible in ordinary code. It draws on four traditions. From Eiffel comes its structural vocabulary—classes, features, inheritance, and contracts. From Scheme comes the conviction that a small, regular core scales further than a large feature set. From ML comes the discipline of static, soundness-minded typing, checked before a program runs and specified in full by a formal definition. From CSP and its descendants comes its concurrency model: lightweight tasks communicating over channels.

What Nex takes from ML is this discipline, not the type algebra of ML proper. The type structure itself is Eiffel's: nominal classes related by inheritance and conformance, with bounded generics. Nex has neither Hindley–Milner inference nor structural typing.

Four commitments shape the language, and the balance struck between them gives it its character.

• Correctness is part of ordinary programming. Preconditions, postconditions, and class invariants are written in the program itself and checked as it runs; a failure is reported by name. They are not a separate proof obligation in another file; they are Design by Contract, carried forward from Eiffel.
• Readability must survive growth. A language that is clean at ten lines and illegible at ten thousand has solved the wrong problem. The core grammar is kept small enough that its meaning can be stated without hand-waving—which is precisely what makes a document like this one possible.
• Objects and functions cooperate. Classes, inheritance, and contracts model the stateful parts of a system; pure functions and immutable values handle the rest. Neither is treated as the privileged paradigm.
• Theory shows up as design, not as notation. The contract system has its roots in Hoare logic, just as the typing and concurrency disciplines have theirs in ML and CSP. None of this is required of the programmer. The theory pays for itself in the regularity of the surface.

It is the third and fourth commitments that make Nex worth defining precisely, and the second that makes it feasible.

1.2The Form of the Definition

Following The Definition of Standard ML, this Definition divides its task in two ways.

First, we separate syntax from semantics. Chapters 2 and 3 give the grammar: the rules that decide which strings of characters are Nex programs. The remaining chapters give the meaning of the programs so admitted.

Second, we separate the static semantics from the dynamic semantics. The static semantics (Chapter 4) describes what can be determined about a program before it runs: the types of its expressions, the conformance of its classes, the well-formedness of its contracts. The dynamic semantics (Chapter 5) describes what happens when the program is evaluated.

This factoring mirrors the implementation, which checks a program statically and then either interprets or compiles it. It also mirrors the programmer's experience: a type error and a contract violation are events of two quite different kinds.

This Definition tries to describe the rules of the language precisely, but its readers need not be versed in formal semantics. The rules are presented in clear prose that can be checked directly against a program.

• A compile-time rule lists the conditions a phrase must meet, and gives the type it has when it meets them. If a condition fails, the program is rejected with a compile-time error.
• A run-time rule gives, in order, the steps by which a phrase is evaluated, and says what happens when a step raises an exception. Rules that hold for every phrase, such as left-to-right evaluation, are stated once, in Section 5.2, and each later rule gives only its exceptions to them.
• Examples are complete programs wherever possible, shown with the output they produce on the reference implementation (Section 1.3).
• Figures illustrate particular cases. Where a figure and the prose seem to differ, the prose is authoritative.

1.3The Status of the Implementations

Nex is defined here independently of any implementation. But Nex also has a reference implementation: the compiler that translates a program to JVM bytecode, which is how the nex command runs a program by default. It is the most thoroughly tested implementation of the language, and it is the one this Definition is checked against.

Nex also has a tree-walking interpreter, which evaluates the abstract syntax directly. It has no special authority. Like any other implementation, where it differs from this Definition, it is in error.

This Definition and the reference implementation are intended to describe the same language. Where they agree, the Definition explains the implementation and the implementation exhibits the Definition. Where they disagree, one of them is in error, and the disagreement is a defect to be repaired rather than a question of taste. The Definition does not silently extend the language; if it appears to, that is a bug in the Definition.

1.4How to Read This Document

The reader who wants only the grammar may read Chapters 2 and 3 and stop. The reader implementing a checker will want Chapter 4; the one implementing an evaluator, Chapters 5 to 7. The appendices collect the full grammar (Appendix A), the classes and values that exist before any user code is loaded (Appendix B, the standard environment), and the derived forms—surface conveniences explained by translation into a smaller bare language (Appendix C), and the works on which Nex and this Definition draw (Appendix D).

Throughout, a few typographic conventions are observed. Nex source text, including the types written in it, is set in a monospaced face: class, require, ?T. Nonterminals of the grammar are set in slanted type: exp, dec, ty.

In a monospaced form that describes a whole kind of phrase, a name the text has not otherwise defined stands for any phrase of the right kind. In e.m(e1, …, en), for example, e is any expression, m any method name, and e1 to en the arguments; in A[T1, …, Tn], A is any class and T1 to Tn any types.