Extended ML
Encyclopedia
Extended ML is a wide-spectrum language
covering both specification and implementation and based on the ML programming language
. It extends the syntax of ML to include axioms
, 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
to eventually yield an executable Standard ML
program. Correctness of the final executable SML program 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 specification, and research into automatic program verification.
Extended ML is neither related to the programming language Extensible ML
(other than being similarly derived from ML), nor to the specification language
eXtensible Markup Language
.
Wide-spectrum language
A wide-spectrum language 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 methodology based on program refinement.The concept was...
covering both specification and implementation and based on the ML programming language
ML programming language
ML is a general-purpose functional programming language developed by Robin Milner and others in the early 1970s at the University of Edinburgh, whose syntax is inspired by ISWIM...
. It extends the syntax of ML to include axioms
Axiomatic semantics
Axiomatic semantics is an approach based on mathematical logic to proving the correctness of computer programs. It is closely related to Hoare logic....
, 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
Formal specification
In computer science, a formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not how the system should do it...
to eventually yield an executable Standard ML
Standard ML
Standard ML 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 theorem provers.SML is a modern descendant of the ML...
program. Correctness of the final executable SML program 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 methods
In computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...
program development and specification, and research into automatic program verification.
Extended ML is neither related to the programming language Extensible ML
Extensible ML
Extensible ML is an ML-like programming language that adds support for object-oriented idioms in a functional setting. EML extends ML-style datatypes and functions with a class construct designed to be extended into hierarchies, thus allowing the programmer to seamlessly integrate the...
(other than being similarly derived from ML), nor to the specification language
Specification language
A specification language is a formal language used in computer science.Unlike most programming languages, which are directly executable formal languages used to implement a system, specification languages are used during systems analysis, requirements analysis and systems design.Specification...
eXtensible Markup Language
Extensible Markup Language
Extensible Markup Language is a set of rules for encoding documents in machine-readable form. It is defined in the XML 1.0 Specification produced by the W3C, and several other related specifications, all gratis open standards....
.