Foundations of formal software development

Algebraic and Logical Foundations of Formal Software Development

Formal software development involves the use of a formal logical calculus which is proven sound with respect to a complete mathematical semantics of the specification language and the programming language involved. It is also necessary to prove the soundness of the development framework itself, i.e. that a series of individual design steps which are individually shown to be correct yields a system which is correct with respect to its specification. Such proofs of soundness rely on the availability of appropriate foundations, providing precise definitions and results related to the basic concepts involved in the enterprise of formally developing systems from specifications.

Over the past decade or so, many of the components needed for a complete, general and coherent theory of specification and formal development of modular software systems have emerged. These include an understanding of: the structure of specifications and how this relates to the modular structure of programs; behavioural equivalence and its role in the implementation of data abstractions; stepwise refinement and implementation of specifications; parameterisation of specifications and program modules; proof in the context of structured specifications; and the degree to which such a theory can be made independent of the particular logical system used to write specifications. Much of this work has been done in the context of an algebraic specification language called ASL having a very simple semantics but which is nonetheless powerful enough to capture all the essential problems on a level at which their essence can easily be studied.

This work is complemented by research on practical formal development of Standard ML software systems in Extended ML (look here for more information) and contributions to the Common Framework Initiative for algebraic specification and development of software (look here for more information and here for Edinburgh contributions).

Publications

Most of the material below, and more, is contained in the following book: The following paper is a shorter and rather informal introduction, with pointers to relevant papers. The papers below are in reverse chronological order of production.
Don Sannella (dts@inf.ed.ac.uk)