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.
 D. Sannella and A. Tarlecki.
On normal forms for structured specifications with generating constraints.
In Memoriam Hartmut Ehrig: On Graph Transformations, Algebraic Specifications and Nets.
Springer LNCS 10800 (2018).
 G. Marczynski, D. Sannella and A. Tarlecki.
Algebraic constructions:
a simple framework for complex dependencies and
parameterisation. International Journal of Software and
Informatics 9(2):117139 (2015).
 D. Sannella and A. Tarlecki.
The foundational legacy of ASL.
Software, Services and Systems: Essays Dedicated to Martin Wirsing
on the Occasion of His Emeritation.
Springer LNCS 8950, 253272 (2015).
 T. Mossakowski, W. Pawlowski, D. Sannella and A. Tarlecki.
Parchments for CafeOBJ logics.
Specification, Algebra, and Software: Essays Dedicated to Kokichi Futatsugi.
Springer LNCS 8373, 6691 (2014).
 D. Sannella and A. Tarlecki.
Propertyoriented semantics of structured specifications.
Mathematical Structures in Computer Science, 24(2), e240205, 37 pages (2014).
 D. Sannella and A. Tarlecki.
Observability concepts in abstract data type specification, 30 years later.
Concurrency, Graphs and Models: Essays Dedicated to Ugo Montanari on the Occasion of his 65th Birthday.
Springer LNCS (2008).
 M. Bidoit, D. Sannella and A. Tarlecki.
Observational interpretation of CASL specifications.
Mathematical Structures in Computer Science 18:325371 (2008).
 D. Sannella and A. Tarlecki.
Horizontal composability revisited.
Algebra, Meaning and Computation: Essays Dedicated to Joseph A. Goguen on the Occasion of his 65th Birthday.
Springer LNCS 4060, 296316 (2006).
 J. Hannay, S. Katsumata and D. Sannella.
Semantic and syntactic approaches to simulation relations.
Proc. 28th Intl. Symp. on Mathematical Foundations of
Computer Science, Bratislava.
Springer LNCS 2747, 6891 (2003).
 M. Bidoit, D. Sannella and A. Tarlecki.
Toward componentoriented formal
software development: an algebraic approach.
Proc. 9th Monterey Workshop, Radical Innovations of Software
and Systems Engineering in the Future, Venice, October 2002.
Springer LNCS 2941, 7590 (2004).
 M. Bidoit, D. Sannella and A. Tarlecki.
Global development via local
observational construction steps.
Proc. 27th Intl. Symp. on Mathematical Foundations of
Computer Science, Warsaw. Springer LNCS 2420, 124 (2002).

G. Plotkin, J. Power, D. Sannella and R. Tennent.
Lax
logical relations.
Proc. 27th Intl. Colloq. on Automata, Languages
and Programming, Geneva. Springer LNCS 1853, 85102 (2000).

F. Honsell, J. Longley, D. Sannella and A. Tarlecki.
Constructive
data refinement in typed lambda calculus.
Proc. 2nd Intl. Conf. on Foundations of Software Science and
Computation Structures, ETAPS'2000, Berlin. Springer LNCS
1784, 149164 (2000).

D. Sannella.
Algebraic
specification and program development by stepwise refinement.
Proc. 9th Intl. Workshop on Logicbased Program Synthesis and
Transformation, LOPSTR'99, Venice.
Springer LNCS 1817, 19 (2000).

F. Honsell and D. Sannella.
Prelogical relations.
Information and Computation 178:2343 (2002).

D. Sannella and A. Tarlecki.
Algebraic
methods for specification and formal development of programs.
ACM Computing Surveys 31 (3es) (1999).
 D. Sannella and A. Tarlecki.
Mind
the gap! Abstract versus concrete models of specifications.
Proc. 21st Intl. Symp. on Mathematical Foundations
of Computer Science, Cracow.
Springer LNCS 1113, 114134 (1996).
 M. Hofmann and D. Sannella.
On
behavioural abstraction and behavioural satisfaction in
higherorder logic.
Theoretical Computer Science 167:345 (1996).
This is the full version of a paper that appeared in
Proc. Joint Conf. on Theory and Practice of Software
Development, Aarhus. Springer LNCS 915, 247261 (1995).
 R. Harper, D. Sannella and A. Tarlecki.
Structured
theory presentations and logic representations.
Annals of Pure and Applied Logic 67:113160 (1994).
 D. Sannella, S. Sokolowski and A. Tarlecki.
Toward
formal development of programs from algebraic specifications:
parameterisation revisited.
Acta Informatica 29, 689736 (1992).
 D. Sannella and A. Tarlecki.
Toward
formal development of programs from algebraic specifications:
modeltheoretic foundations.
Proc. 19th Intl. Colloq. on Automata, Languages and Programming,
Vienna. Springer LNCS 623, 656671 (1992).
But wait! An improved and extended version of this is:
Essential
concepts of algebraic specification and program development.
Formal Aspects of Computing 9:229269 (1997).
 D. Sannella and A. Tarlecki.
A
kernel specification formalism with higherorder
parameterisation.
Proc. 7th Workshop on Specification of Abstract Data Types,
Wusterhausen, 1990. Springer LNCS 534, 274296 (1991).
 D. Sannella and A. Tarlecki.
Algebraic
specification and formal methods for program development: what
are the real problems?
EATCS Bulletin 41:134137 (1990).
 D. Sannella and A. Tarlecki.
Toward
formal development of programs from algebraic specifications:
implementations revisited.
Acta Informatica 25, 233281 (1988).
 D. Sannella and A. Tarlecki.
Specifications in an arbitrary institution.
Information and Computation 76:165210 (1988).
 D. Sannella and A. Tarlecki.
On observational equivalence and
algebraic specification.
Journal of Computer and System Sciences 34:150178 (1987).
 D.Sannella and A. Tarlecki.
Some
thoughts on algebraic specification.
Proc. 3rd Workshop on Theory and Applications of Abstract Data
Types, Bremen, 1984.
Springer InformatikFachberichte 116, 3138 (1985).
 D. Sannella. A settheoretic
semantics for Clear.
Acta Informatica 21:443472 (1984).
 D.Sannella and M. Wirsing.
A kernel language for algebraic
specification and implementation.
Proc. 1983 Intl. Conf. on
Foundations of Computation Theory, Borgholm.
Springer LNCS 158, 413427 (1983).
 D.Sannella and M. Wirsing.
Implementation of parameterised
specifications.
Proc. 9th Intl. Colloq. on Automata, Languages and
Programming, Aarhus.
Springer LNCS 140, 473488 (1982).
Don Sannella (dts@inf.ed.ac.uk)