Jump to content

Extended ML

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Rcbarnes (talk | contribs) at 23:13, 16 October 2006. The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Extended ML is a specification language created by Kahrs, Sannella and Tarlecki 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 refinement step. 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 o the specification language eXtensible Markup Language.

References

  • S. Kahrs, D. Sannella, and A. Tarlecki. The definition of extended ML: A gentle introduction. Theoretical Computer Science, 173(2):445-484, 28 Feb 1997
Stub icon

This programming-language-related article is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Extended_ML&oldid=81883339"