• People
• Events
• Research

The Definition of Extended ML

Abstract: This document formally defines the syntax and semantics of the Extended ML language. It is based directly on the published semantics of Standard ML in an attempt to ensure compatibility between the two languages.

From the Preface: Extended ML is a framework for the formal development of programs in the Standard ML programming language from high-level specifications of their required behaviour. The Extended ML language is a "wide-spectrum" language which encompasses both specifications and executable programs in a single unified framework. This allows all stages in the development of a program to be expressed in the Extended ML language, from the initial high-level specification to the final code itself and including intermediate stages in which specification and code are intermingled.

The Extended ML language is an extension of a large subset of Standard ML. This subset excludes references, assignment, input/output and imperative polymorphism, requires structure declarations and functor declarations to include explicit signatures, and restricts structures and functors to behave as abstractions and parameterised abstractions respectively. Thus, Extended ML can only be used to specify/develop programs written in this subset of Standard ML. The Extended ML language extends this subset by permitting axioms in module interfaces (for specifying required properties of module components) and in place of code in module bodies (for describing functions in a non-algorithmic way prior to their implementation as Standard ML code).

The principles behind the design of the Extended ML language and development framework, details of its theoretical underpinnings and examples of its use may be found in [ST85], [ST86], [ST89], [ST90] and [ST91]. The interested reader should consult these for background information. This document is a formal definition of the syntax and semantics of the Extended ML language; the other components of the Extended ML framework are disregarded here.

Because of the intimate relationship between The Definition of Standard ML and this document, familiarity with the former (for which study of Commentary on Standard ML is strongly recommended!) is almost a prerequisite to achieving a deep understanding of the latter. The length and necessary formality of a definition such as this one makes it rather difficult to penetrate. For this reason an informal overview of the definition, which explains most of the main issues involved and justifies some of the choices taken, is provided in [KST93].

This report is 156-pages long. It is available in DVI (563Kb) and Postscript (0.9Mb) format.