🚀 go-pugleaf

In article <1990Dec17.190909.10829@news.nd.edu>, rohrs@handel.helios.nd.edu (533) writes:
> I am in the early stages of a literature survey on the topic of formal 
> specification of (software) systems. I'm looking for any suggestions, leads
> or pointers to survey papers or taxonomies published in the area.
> 
> I'm also interested in any tutorials, texts, papers, etc. on particular 
> specification "languages" including, but not limited to: SDL, Z, PSL/PSA,
> SADT, RSL, Anna, IORL, Gypsy, OBJ, and Estelle.

I think the specification language / formal program development framework
"Extended ML" deserves to be included in this list.  This is for specifying
and developing programs in the Standard ML functional programming language,
although it is applicable to other programming languages as well.  Since I
haven't seen anything about it in this group before, I'm posting the
following rather than mailing it to rohrs@handel.helios.nd.edu.  Anybody
interested is welcome to contact me for copies of papers or further details.


From the introduction of [ST91]
-------------------------------

Extended ML is a framework for the formal development of programs in the
Standard ML functional programming language from high-level specifications of
their required input/output behaviour.  Extended ML is a completely formal
framework with a very extensively-developed mathematical basis in the theory of
algebraic specifications.  It strongly supports ``development in the large'',
producing modular programs consisting of an interconnected collection of
generic and modular units.  The Extended ML framework includes a methodology
for formal program development which establishes a number of ways of proceeding
from a given specification of a programming task towards a program.  Each such
step (modular decomposition, etc.) gives rise to one or more proof obligations
which must be discharged in order to establish the correctness of that step.

The Extended ML language is a wide-spectrum language which encompasses both
specifications and executable programs in a single unified framework.  It is a
simple extension of the Standard ML programming language in which axioms are
permitted in module interfaces and in place of code in module bodies.  This
allows all stages in the development of a program to be expressed in the
Extended ML language, 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 Extended ML means writing a high-level
specification of a generic Standard ML module and then refining this
specification top-down by means of a sequence (actually, a tree) of development
steps until an executable Standard ML 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
Standard ML 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.


Some recent papers
------------------

D. Sannella and A. Tarlecki.  Toward formal development of ML programs:
foundations and methodology.  Joint Conf. on Theory and Practice of Software
Development (TAPSOFT), Barcelona.  Springer LNCS 352 (1989).

D. Sannella.  Formal program development in Extended ML for the working
programmer.  Proc. 3rd BCS/FACS Workshop on Refinement, Hursley Park.
Springer LNCS, to appear (1990).

D. Sannella and A. Tarlecki.  Extended ML: past, present and future.  Proc. 7th
Workshop on Specification of Abstract Data Types, Wusterhausen.  Springer LNCS,
to appear (1991).


Caveats
-------

The emphasis in work on Extended ML has mainly been on the FOUNDATIONS of
practical formal program development.  We are very serious about e.g. providing
a complete semantics for the entire specification language, proving that if you
do formal program development in the Extended ML framework then your programs
really will satisfy the specification you started with, etc.  Thus, relatively
few case studies have been carried out, and no tools are yet available for
working with Extended ML specifications (although work is in progress on these).
Until recently, we concentrated on simple first-order total functional programs,
but we are now trying to handle all of Standard ML (except for references and
assignment), including higher-order functions, polymorphism, exceptions, and
non-terminating programs.


About Standard ML
-----------------

Standard ML is a powerful functional (but not purely functional) programming
language with advanced modularisation facilities.  See the first two references
below for an introduction to Standard ML; the third reference is the complete
formal semantics of the language.

R. Harper.  Introduction to Standard ML.  Report ECS-LFCS-86-14, Univ. of
Edinburgh.  Revised edition (1989).

C. Reade.  Elements of Functional Programming.  Addison-Wesley (1989).

R. Milner, M. Tofte and R. Harper.  The Definition of Standard ML.
MIT Press (1990).



Don Sannella
University of Edinburgh