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:

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. (More ...)

The following paper is a shorter and rather informal introduction, with pointers to relevant papers.

D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program development. Formal Aspects of Computing 9:229-269 (1997).

The papers below are in reverse chronological order of production.

D. Sannella and A. Tarlecki. On normal forms for structured specifications with generating constraints. Graph Transformations, Algebraic Specifications and Nets: In Memory of Hartmut Ehrig. Springer LNCS 10800, 266-284 (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):117-139 (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, 253-272 (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, 66-91 (2014).
D. Sannella and A. Tarlecki. Property-oriented 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:325-371 (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, 296-316 (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, 68-91 (2003).
M. Bidoit, D. Sannella and A. Tarlecki. Toward component-oriented 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, 75-90 (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, 1-24 (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, 85-102 (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, 149-164 (2000).
D. Sannella. Algebraic specification and program development by stepwise refinement. Proc. 9th Intl. Workshop on Logic-based Program Synthesis and Transformation, LOPSTR'99, Venice. Springer LNCS 1817, 1-9 (2000).
F. Honsell and D. Sannella. Prelogical relations. Information and Computation 178:23-43 (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, 114-134 (1996).
M. Hofmann and D. Sannella. On behavioural abstraction and behavioural satisfaction in higher-order logic. Theoretical Computer Science 167:3-45 (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, 247-261 (1995).
R. Harper, D. Sannella and A. Tarlecki. Structured theory presentations and logic representations. Annals of Pure and Applied Logic 67:113-160 (1994).
D. Sannella, S. Sokolowski and A. Tarlecki. Toward formal development of programs from algebraic specifications: parameterisation revisited. Acta Informatica 29, 689-736 (1992).
D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifications: model-theoretic foundations. Proc. 19th Intl. Colloq. on Automata, Languages and Programming, Vienna. Springer LNCS 623, 656-671 (1992).
But wait! An improved and extended version of this is: Essential concepts of algebraic specification and program development. Formal Aspects of Computing 9:229-269 (1997).
D. Sannella and A. Tarlecki. A kernel specification formalism with higher-order parameterisation. Proc. 7th Workshop on Specification of Abstract Data Types, Wusterhausen, 1990. Springer LNCS 534, 274-296 (1991).
D. Sannella and A. Tarlecki. Algebraic specification and formal methods for program development: what are the real problems? EATCS Bulletin 41:134-137 (1990).
D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifications: implementations revisited. Acta Informatica 25, 233-281 (1988).
D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Computation 76:165-210 (1988).
D. Sannella and A. Tarlecki. On observational equivalence and algebraic specification. Journal of Computer and System Sciences 34:150-178 (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 Informatik-Fachberichte 116, 31-38 (1985).
D. Sannella. A set-theoretic semantics for Clear. Acta Informatica 21:443-472 (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, 413-427 (1983).
D.Sannella and M. Wirsing. Implementation of parameterised specifications. Proc. 9th Intl. Colloq. on Automata, Languages and Programming, Aarhus. Springer LNCS 140, 473-488 (1982).

Don Sannella (dts@inf.ed.ac.uk)