Path: utzoo!censor!geac!torsqnt!news-server.csri.toronto.edu!cs.utexas.edu!wuarchive!uunet!mcsun!ukc!edcastle!cs.ed.ac.uk!cs.edinburgh.ac.uk!dts From: dts@cs.edinburgh.ac.uk (Don Sannella) Newsgroups: comp.specification Subject: Re: formal system specification surveys Keywords: formal specification language, survey, taxonomy Message-ID: <3809@skye.cs.ed.ac.uk> Date: 19 Dec 90 15:30:24 GMT References: <1990Dec17.190909.10829@news.nd.edu> Sender: nnews@cs.ed.ac.uk Reply-To: dts@cs.edinburgh.ac.uk (Don Sannella) Organization: Department of Computer Science, University of Edinburgh Lines: 110 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