Extended ML is a

wide-spectrum language A wide-spectrum language (WSL) is a programming language designed to be simultaneously a low-level and a high-level language—possibly a non-executable specification language. Wide-spectrum languages are designed to support a programming m ...

based on ML, covering both

specification A specification often refers to a set of documented requirements to be satisfied by a material, design, product, or service. A specification is often a type of technical standard. There are different types of technical or engineering specificati ...

and implementation. It extends the syntax of ML to include

axioms An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or f ...

, which need not be executable but can rigorously specify the behavior of the program. With this addition the language can be used for stepwise refinement, proceeding gradually from an initial

formal specification In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verif ...

to eventually yield an executable

Standard ML Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of the ...

program. Correctness of the final executable with respect to the original specification can then be established by proving the correctness of each of the refinement steps. Extended ML is used for research into and teaching of formal program development and

, and research into automatic

program verification In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...

. Extended ML is neither related to the programming language Extensible ML (other than being similarly derived from ML), nor to the

specification language A specification language is a formal language in computer science used during systems analysis, requirements analysis, and systems design to describe a system at a much higher level than a programming language, which is used to produce the executa ...

Extensible Markup Language Extensible Markup Language (XML) is a markup language and file format for storing, transmitting, and reconstructing arbitrary data. It defines a set of rules for encoding documents in a format that is both human-readable and machine-readable. T ...

(XML).

References

* S. Kahrs, D. Sannella and A. Tarlecki. The definition of extended ML: A gentle introduction. ''

Theoretical Computer Science Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory. It is difficult to circumsc ...

'', 173(2):445–484, 28 February 1997.

External links

Don Sannella — Information about Extended ML
ML programming language family Formal specification languages Programming languages created in the 1980s {{compu-lang-stub