A Formal Definition

The Definition of Nex

A precise account of the syntax and meaning of the Nex programming language.

This document describes the grammar of Nex and the meaning of the constructions built from that grammar. It is written for implementers, for those who wish to reason about Nex programs, and for readers who want to understand the language as a designed object rather than as a collection of features. It follows, in spirit and in structure, the tradition of rigorous language definition gathered in the References (Appendix D): a separation of syntax from semantics, and of the static semantics (what can be checked before a program runs) from the dynamic semantics (what happens when it does).

1. 1
   Introduction What this document is, the method it follows, and the shape of the language.
2. 2
   Syntax of the Core Reserved words, special constants, identifiers, lexis, and the core grammar.
3. 3
   Syntax of Classes and Modules Classes, features, contracts, generics, and the unit structure.
4. 4
   Static Semantics Types, bindings, conformance, generic elaboration, and contract formation.
5. 5
   Dynamic Semantics Values, objects, evaluation, contract checking, and exceptions.
6. 6
   Concurrency Tasks, channels, and selective communication.
7. 7
   Programs Top-level elaboration and the execution of a whole program.
8. A
   Appendix A · The Full Grammar The complete context-free grammar collected in one place.
9. B
   Appendix B · The Standard Environment The classes and values present before any user code is loaded.
10. C
    Appendix C · Derived Forms Surface forms defined by translation into the bare language.
11. D
    Appendix D · References The works on whose ideas Nex and this Definition draw.

The authoritative implementation of Nex is its tree-walking interpreter; where this Definition and the interpreter disagree, that is a defect in one of them, and the discrepancy is worth reporting.