Extended ML

Frequently asked question: I got an email containing a downloadable file having an eml extension. Can you tell me what this means?

Answer: eml is the Microsoft Outlook/mail e-mail file format. Just like Word documents have .doc extensions and Excel spreadsheets have .xls, email files have .eml. You should be able to open .eml files in Outlook. All this has nothing whatsoever to do with EML as described here, and I can't help you with whatever your problem is with your eml attachment.


Extended ML

Extended ML (EML) is a framework for specification and formal development of Standard ML (SML) programs. EML specifications look just like SML programs except that axioms are allowed in signatures and in place of code in structures and functors. Some EML specifications are executable, since SML function definitions are just axioms of a certain special form. This makes EML a "wide-spectrum" language which can be used to express every stage in the development of a SML program from the initial high-level specification to the final program itself and including intermediate stages in which specification and program are intermingled.

Formally developing a program in EML means writing a high-level specification of a generic SML module and then refining this specification top-down by means of a sequence (actually, a tree) of development steps until an executable SML program is obtained. The development has a tree-like structure since one of the ways to proceed from a specification is to decompose it into a number of smaller specifications which can then be independently refined further. In programming terms, this corresponds to implementing a program module by decomposing it into a number of independent sub-modules. The end-product is an interconnected collection of generic SML modules, each with a complete and accurate specification of its interface with the rest of the system. The explicit interfaces enable correct reuse of the individual modules in other systems, and facilitate maintainability by making it possible to localize the effect on the system of subsequent changes in the requirements specification.

This work is complemented by research on algebraic and logical foundations for specification and formal program development. These foundations give substance to guarantees that a formally developed software system satisfies the specification of requirements from which the development process commenced. Look here for more information, and/or read

D. Sannella and A. Tarlecki. Foundations of Algebraic Specification and Formal Software Development. EATCS Monographs in Theoretical Computer Science. Springer, 2012. ISBN 978-3-642-17335-6. Order from Amazon (reviews) or Springer.

Publications

Here are good places to start reading about EML. Here are some other papers on EML, in reverse chronological order. (Some of the details in the older papers are obsolete.)


Tool support

An EML parser and typechecker by Kenneth MacKenzie based on Moscow ML v2.0 is available here.

The EML Kit, a parser and typechecker for EML based on the ML Kit, is available from Warsaw. If you experience delays in downloading, try these local copies (version 1.1): eml11-src.tar.gz (source, 300617 bytes) eml11-i386.tar.gz (i386 Linux binaries, 3394292 bytes) eml11-sparc.tar.gz (Sun SPARC Solaris binaries, 4890079 bytes).

Ben Kleinman worked on an environment for formal development of terminating SML programs in EML, building on the EML Kit, a prototype proof obligation generator by Paul Varnish, and the PVS theorem prover, but Ben moved on and that work has been abandoned.

Anybody who is interested in adding support for EML parsing and typechecking to an existing SML implementation is encouraged to read On the static analysis of Extended ML, and to contact me for further support and encouragement.


Educational resources

EML was used until 2010/2011 in the following course at the University of Edinburgh: Until 2000/2001 it was also used in the following course: Follow the links to find course notes etc. (If the course is in progress then some of the notes, examples, exercises etc. may be missing; contact me if you need them and can't wait.) Some of the items in the above list of publications are tutorial in character and can be used to teach EML. I would particularly recommend Formal specification of ML programs (an elementary tutorial about specification and proof) and Formal program development in Extended ML for the working programmer (a presentation of EML for people who want to use it without bothering about the theory behind it). Both are unfortunately obsolete with respect to the current syntax of EML, but the differences are minor. See the lecture notes here, here, here and here for a corrected version of the former.

EML is also used or has been used in various courses at other universities. Anybody who would like to publish a link here is invited to contact me.


Don Sannella. Please mail me if you have any comments on this page.
Last modified: Wed May 8 09:52:39 BST 2013