Extended ML is a wide-spectrum language 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 specificat ...

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 ...

, 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 veri ...

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 ...

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 Formal, formality, informal or informality imply the complying with, or not complying with, some set of requirements (forms, in Ancient Greek). They may refer to: Dress code and events * Formal wear, attire for formal events * Semi-formal attire ...

program development and

, and research into automatic program verification. Extended ML is neither related to the programming language

Extensible ML Extensibility is a software engineering and systems design principle that provides for future growth. Extensibility is a measure of the ability to extend a system and the level of effort required to implement the extension. Extensions can be th ...

(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 electronic document, documents in a format that is both Human-readable med ...

(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