Don Sannella's publications

Don Sannella's publications

Where electronic copies are supplied, they are usually formatted for A4 paper. Where I know about problems resulting from margins (especially top margins) that are too narrow to fit on US-size paper, I have converted the Postscript and PDF versions to fit. Please tell me about any problems of this kind that you might have so that I can do something about them. If you want to try doing the conversion yourself, the incantation I use (for the Postscript version) is
psnup -Pa4 -pletter filea4.ps > fileUS.ps
(this requires psnup) but please tell me about the problem anyway.

Sometimes the same paper appears in both a conference version (short and preliminary) and a journal or book version (longer and more polished). Then I have put a note in each entry indicating the existence of the other.

Copyright notice: These documents are provided as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
For papers published in Springer Lecture Notes in Computer Science: these publications are © Springer-Verlag, see the LNCS series homepage for the full volume.



[MPST14]
Till Mossakowski, Wieslaw Pawlowski, Donald Sannella, and Andrzej Tarlecki. Parchments for CafeOBJ logics. In Specification, Algebra, and Software, volume 8373 of Lecture Notes in Computer Science, pages 66-91. Springer, 2014. [ bib | .pdf ]
This paper addresses issues arising in the systematic construction of large logical systems. We rely on a model-theoretic view of logical systems, captured by institutions that are in turn presented by parchments. We define their categories, and study constructions that may be carried out in these categories. In particular we show how limits of parchments may be used to combine features involved in various logical systems, sometimes necessarily augmenting the universal construction by additional systematic adjustments. We illustrate these developments by sketching how the logical systems that form the logical foundations of CafeOBJ may be built in this manner.

[ST13]
Donald Sannella and Andrzej Tarlecki. Property-oriented semantics of structured specifications. Mathematical Structures in Computer Science, 2013. [ bib | .pdf ]
We consider structured specifications built from flat specifications using union, translation and hiding with their standard model-class semantics, in the context of an arbitrary institution. We examine the alternative of sound property-oriented semantics for such specifications, and study their relationship to model-class semantics. An exact correspondence between the two (completeness) is not achievable in general. We show via general results on property-oriented semantics that the semantics arising from the standard proof system is the strongest sound and compositional property-oriented semantics in a wide class of such semantics. We also sharpen one of the conditions that does guarantee completeness and show that it is a necessary condition.

[To appear.]
[ST12]
Donald Sannella and Andrzej Tarlecki. Foundations of Algebraic Specification and Formal Software Development. EATCS Monographs in Theoretical Computer Science. Springer, 2012. [ bib ]
This book provides foundations for software specification and formal software development from the perspective of work on algebraic specification, concentrating on developing basic concepts and studying their fundamental properties. These foundations are built on a solid mathematical basis, using elements of universal algebra, category theory and logic, and this mathematical toolbox provides a convenient language for precisely formulating the concepts involved in software specification and development. Once formally defined, these notions become subject to mathematical investigation, and this interplay between mathematics and software engineering yields results that are mathematically interesting, conceptually revealing, and practically useful.

[Available from Springer at www.springer.com/computer/theoretical+computer+science/book/978-3-642-17335-6 and from Amazon at www.amazon.co.uk/Foundations-Specification-Development-Monographs-Theoretical/dp/3642173357.]
[AAMS10]
David Aspinall, Robert Atkey, Kenneth MacKenzie, and Donald Sannella. Symbolic and analytical techniques for resource analysis of Java bytecode. In Proc. 5th Symp. on Trustworthy Global Computing (TGC 2010), volume 6084 of Lecture Notes in Computer Science, pages 1-22. Springer, 2010. [ bib | .pdf ]
Recent work in resource analysis has translated the idea of amortised resource analysis to imperative languages using a program logic that allows mixing of assertions about heap shapes, in the tradition of separation logic, and assertions about consumable resources. Separately, polyhedral methods have been used to calculate bounds on numbers of iterations in loop-based programs. We are attempting to combine these ideas to deal with Java programs involving both data structures and loops, focusing on the bytecode level rather than on source code.

[ST08]
Donald Sannella and Andrzej Tarlecki. Observability concepts in abstract data type specification, 30 years later. In Concurrency, Graphs and Models: Essays Dedicated to Ugo Montanari on the Occasion of his 65th Birthday, Lecture Notes in Computer Science. Springer, 2008. [ bib | .ps | .pdf ]
We recall the contribution of Montanari's paper [GGM76] and sketch a framework for observable behaviour specification that blends some of these early ideas, seen from a more modern perspective, with our own approach.

[MHST08]
Till Mossakowski, Anne Haxthausen, Donald Sannella, and Andrzej Tarlecki. CASL - the common algebraic specification language. In Dines Bjørner and Martin Henson, editors, Logics of Specification Languages, pages 241-298. Springer, 2008. [ bib ]
CASL is an expressive specification language that has been designed to supersede many existing algebraic specification languages and provide a standard. CASL consists of several layers, including basic (unstructured) specifications, structured specifications and architectural specifications; the latter are used to prescribe the structure of implementations.

We describe an simplified version of the CASL syntax, semantics and proof calculus for each of these three layers and state the corresponding soundness and completeness theorems. The layers are orthogonal in the sense that the semantics of a given layer uses that of the previous layer as a “black box”, and similarly for the proof calculi. In particular, this means that CASL can easily be adapted to other logical systems.

We conclude with a detailed example specification of a warehouse, which serves to illustrate the application of both CASL and the proof calculi for the various layers.

[This is an extended version of [MHST03].]
[BST08]
Michel Bidoit, Donald Sannella, and Andrzej Tarlecki. Observational interpretation of CASL specifications. Mathematical Structures in Computer Science, 18:325-371, 2008. [ bib | .pdf ]
The way that refinement of individual “local” components of a specification relates to development of a “global” system from a specification of requirements is explored. Observational interpretation of specifications and refinements add expressive power and flexibility while bringing in some subtle problems. Our study of these issues is carried out in the context of CASL architectural specifications. We introduce a definition of observational equivalence for CASL models, leading to an observational semantics for architectural specifications for which we prove important properties. Overall, this fulfills the long-standing goal of complementing the standard semantics of CASL specifications with an observational view that supports observational refinement of specifications in combination with CASL-style architectural design.

[An early short version was [BST02b].]
[SHA+07]
Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, Hans-Wolfgang Loidl, Kenneth MacKenzie, Alberto Momigliano, and Olha Shkaravska. Mobile resource guarantees. In Trends in Functional Programming, volume 6, pages 211-226. Intellect, 2007. [ bib | .dvi | .ps | .pdf ]
The Mobile Resource Guarantees (MRG) project has developed a proof-carrying-code infrastructure for certifying resource bounds of mobile code. Key components of this infrastructure are a certifying compiler for a high-level language, a hierarchy of program logics, tailored for reasoning about resource consumption, and an embedding of the logics into a theorem prover. In this paper, we give an overview of the project's results, discuss the lessons learnt from it and introduce follow-up work in new projects that will build on these results.

[ST06]
Donald Sannella and Andrzej Tarlecki. Horizontal composability revisited. In Algebra, Meaning and Computation: Essays Dedicated to Joseph A. Goguen on the Occasion of his 65th Birthday, volume 4060 of Lecture Notes in Computer Science, pages 296-316. Springer, 2006. [ bib | .ps | .pdf ]
We recall the contribution of Goguen and Burstall's 1980 CAT paper and its powerful influence on theories of specification implementation that were emerging at about the same time, via the introduction of the notions of vertical and horizontal composition of implementations. We then give a different view of implementation which we believe provides a more adequate reflection of the rather subtle interplay between implementation, specification structure and program structure.

[AGH+05]
David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella, and Ian Stark. Mobile resource guarantees for smart devices. In Proc. Intl. Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS 2004), volume 3362 of Lecture Notes in Computer Science, pages 1-26. Springer, 2005. [ bib | .dvi | .ps | .pdf ]
We present the Mobile Resource Guarantees framework: a system for ensuring that downloaded programs are free from run-time violations of resource bounds. Certificates are attached to code in the form of efficiently checkable proofs of resource bounds; in contrast to cryptographic certificates of code origin, these are independent of trust networks. A novel programming language with resource constraints encoded in function types is used to streamline the generation of proofs of resource usage.

[BST04]
Michel Bidoit, Donald Sannella, and Andrzej Tarlecki. Toward component-oriented formal software development: An algebraic approach. In Proc. 9th Monterey Workshop, Radical Innovations of Software and Systems Engineering in the Future, volume 2941 of Lecture Notes in Computer Science, pages 75-90. Springer, 2004. [ bib | .dvi | .ps | .pdf ]
Component based design and development of software is one of the most challenging issues in software engineering. In this paper, we adopt a somewhat simplified view of software components and discuss how they can be conveniently modeled in a framework that provides a modular approach to formal software development by means of stepwise refinements. In particular we take into account an observational interpretation of requirements specifications and study its impact on the definition of the semantics of specifications of (parametrized) components. Our study is carried out in the context of CASL architectural specifications.

[ST04]
Donald Sannella and Andrzej Tarlecki, editors. CASL semantics. In Peter Mosses, editor, CASL Reference Manual, volume 2960 of Lecture Notes in Computer Science, pages 115-274. Springer, 2004. [ bib ]
[San04b]
Donald Sannella. CASL semantics: Introduction. In Peter Mosses, editor, CASL Reference Manual, volume 2960 of Lecture Notes in Computer Science, chapter III.1, pages 117-123. Springer, 2004. [ bib ]
[San04a]
Donald Sannella. CASL semantics: Basic specifications. In Peter Mosses, editor, CASL Reference Manual, volume 2960 of Lecture Notes in Computer Science, chapter III.2, pages 125-170. Springer, 2004. [ bib ]
[MST04]
Till Mossakowski, Donald Sannella, and Andrzej Tarlecki. A simple refinement language for CASL. In Recent Trends in Algebraic Development Techniques: Selected Papers from WADT 2004, volume 3423 of LNCS, pages 162-185. Springer, 2004. [ bib | .dvi | .ps | .pdf ]
We extend CASL architectural specifications with a simple refinement language that allows the formalization of developments as refinement trees. The essence of the extension is to allow refinements of unit specifications in CASL architectural specifications.

[HKS03]
Jo Hannay, Shin-ya Katsumata, and Donald Sannella. Semantic and syntactic approaches to simulation relations. In Proc. 28th Intl. Symp. on Mathematical Foundations of Computer Science, volume 2747 of Lecture Notes in Computer Science, pages 68-91. Springer, 2003. [ bib | .dvi | .ps | .pdf ]
Simulation relations are tools for establishing the correctness of data refinement steps. In the simply-typed lambda calculus, logical relations are the standard choice for simulation relations, but they suffer from certain shortcomings; these are resolved by use of the weaker notion of pre-logical relations instead. Developed from a syntactic setting, abstraction barrier-observing simulation relations serve the same purpose, and also handle polymorphic operations. Meanwhile, second-order pre-logical relations directly generalise pre-logical relations to polymorphic lambda calculus (System F). We compile the main refinement-pertinent results of these various notions of simulation relation, and try to raise some issues for aiding their comparison and reconciliation.

[MHST03]
Till Mossakowski, Anne Haxthausen, Donald Sannella, and Andrzej Tarlecki. CASL - the common algebraic specification language: Semantics and proof theory. Computing and Informatics, 22:285-321, 2003. An extended version appeared in [MHST08]. [ bib | .dvi | .ps | .pdf ]
CASL is an expressive specification language that has been designed to supersede many existing algebraic specification languages and provide a standard. CASL consists of several layers, including basic (unstructured) specifications, structured specifications and architectural specifications (the latter are used to prescribe the structure of implementations).

We describe an simplified version of the CASL syntax, semantics and proof calculus at each of these three layers and state the corresponding soundness and completeness theorems. The layers are orthogonal in the sense that the semantics of a given layer uses that of the previous layer as a “black box”, and similarly for the proof calculi. In particular, this means that CASL can easily be adapted to other logical systems.

[Reviewed in Zbl 1104.68365.]
[ST03]
Donald Sannella and Andrzej Tarlecki. Foundations. In CASL User Manual, volume 2900 of Lecture Notes in Computer Science, chapter 10, pages 125-129. Springer, 2003. [ bib ]
[HS02]
Furio Honsell and Donald Sannella. Prelogical relations. Information and Computation, 178:23-43, 2002. [ bib | .dvi | .ps | .pdf ]
We study a weakening of the notion of logical relations, called prelogical relations, that has many of the features that make logical relations so useful as well as further algebraic properties including composability. The basic idea is simply to require the reverse implication in the definition of logical relations to hold only for pairs of functions that are expressible by the same lambda term. Prelogical relations are the minimal weakening of logical relations that gives composability for extensional structures and simultaneously the most liberal definition that gives the Basic Lemma. Prelogical predicates (i.e., unary prelogical relations) coincide with sets that are invariant under Kripke logical relations with varying arity as introduced by Jung and Tiuryn, and prelogical relations are the closure under projection and intersection of logical relations. These conceptually independent characterizations of prelogical relations suggest that the concept is rather intrinsic and robust. The use of prelogical relations gives an improved version of Mitchell's representation independence theorem which characterizes observational equivalence for all signatures rather than just for first-order signatures. Prelogical relations can be used in place of logical relations to give an account of data refinement where the fact that prelogical relations compose explains why stepwise refinement is sound.

[This is an extended version of [HS99] that supercedes Report ECS-LFCS-99-405, Laboratory for Foundations of Computer Science, Univ. of Edinburgh (1999).]
[BST02b]
Michel Bidoit, Donald Sannella, and Andrzej Tarlecki. Global development via local observational construction steps. In Proc. 27th Intl. Symp. on Mathematical Foundations of Computer Science, volume 2420 of Lecture Notes in Computer Science, pages 1-24. Springer, 2002. An extended version appeared in [BST08]. [ bib | .dvi | .ps | .pdf ]
The way that refinement of individual “local” components of a specification relates to development of a “global” system from a specification of requirements is explored. Observational interpretation of specifications and refinements add expressive power and flexibility while bringing in some subtle problems. The results are instantiated in the context of CASL architectural specifications.

[BST02a]
Michel Bidoit, Donald Sannella, and Andrzej Tarlecki. Architectural specifications in CASL. Formal Aspects of Computing, 13:252-273, 2002. [ bib | .dvi | .ps | .pdf ]
One of the most novel features of CASL, the Common Algebraic Specification Language, is the provision of so-called architectural specifications for describing the modular structure of software systems. A brief discussion of refinement of CASL specifications provides the setting for a presentation of the rationale behind architectural specifications. This is followed by some details of the features provided in CASL for architectural specifications, hints concerning their semantics, and simple results justifying their usefulness in the development process.

[This is an extended version of [BST99] that supercedes Report ECS-LFCS-99-407, Laboratory for Foundations of Computer Science, Univ. of Edinburgh (1999).]
[ABK+02]
Egidio Astesiano, Michel Bidoit, Hélène Kirchner, Bernd Krieg-Brückner, Peter Mosses, Donald Sannella, and Andrzej Tarlecki. CASL: The common algebraic specification language. Theoretical Computer Science, 286:153-196, 2002. [ bib | .dvi | .ps | .pdf ]
CASL is an expressive language for the formal specification of functional requirements and modular design of software. It has been designed by CoFI, the international Common Framework Initiative for algebraic specification and development. It is based on a critical selection of features that have already been explored in various contexts, including subsorts, partial functions, first-order logic, and structured and architectural specifications. CASL should facilitate interoperability of many existing algebraic prototyping and verification tools.

This paper gives an overview of the CASL design. The major issues that had to be resolved in the design process are indicated, and all the main concepts and constructs of CASL are briefly explained and illustrated - the reader is referred to the CASL Language Summary for further details. Some familiarity with the fundamental concepts of algebraic specification would be advantageous.

[MS02]
Patricia D.L. Machado and Donald Sannella. Unit testing for CASL architectural specifications. In Proc. 27th Intl. Symp. on Mathematical Foundations of Computer Science, volume 2420 of Lecture Notes in Computer Science, pages 506-518. Springer, 2002. [ bib | .dvi | .ps | .pdf ]
The problem of testing modular systems against algebraic specifications is discussed. We focus on systems where the decomposition into parts is specified by a CASL-style architectural specification and the parts (units) are developed separately, perhaps by an independent supplier. We consider how to test such units without reference to their context of use. This problem is most acute for generic units where the particular instantiation cannot be predicted.

[AS02]
David Aspinall and Donald Sannella. From specifications to code in CASL. In Proc. 9th Intl. Conf. on Algebraic Methodology And Software Technology, volume 2422 of LNCS, pages 1-14. Springer, 2002. [ bib | .dvi | .ps | .pdf ]
The status of the Common Framework Initiative (CoFI) and the Common Algebraic Specification Language (CASL) are briefly presented. One important outstanding point concerns the relationship between CASL and programming languages; making a proper connection is obviously central to the use of CASL specifications for software specification and development. Some of the issues involved in making this connection are discussed.

[RS02]
David Rydeheard and Donald Sannella. Preface to a collection of papers and memoirs celebrating the contribution of Rod Burstall to advances in Computer Science. Formal Aspects of Computing, 13:187-193, 2002. [ bib | .dvi | .ps | .pdf ]
In this Preface, we attempt to summarize Rod Burstall's scientific achievements. In addition, we describe the personal style and enthusiasm that Rod has brought to the subject.

[San01]
Donald Sannella. The Common Framework Initiative for algebraic specification and development of software: Recent progress. In Recent Trends in Algebraic Development Techniques: Selected Papers from WADT 2001, volume 2267 of Lecture Notes in Computer Science, pages 328-343. Springer, 2001. [ bib | .ps | .pdf ]
The Common Framework Initiative (CoFI) is an open international collaboration which aims to provide a common framework for algebraic specification and development of software. The central element of the Common Framework is a specification language called CASL for formal specification of functional requirements and modular software design which subsumes many previous algebraic specification languages. This paper is a brief summary of progress on CoFI during the period 1998-2001, when CoFI received funding from the European Commission as a Working Group under the Esprit programme.

[PPST00]
Gordon Plotkin, John Power, Donald Sannella, and Robert Tennent. Lax logical relations. In Proc. 27th Intl. Colloq. on Automata, Languages and Programming, volume 1853 of Lecture Notes in Computer Science, pages 85-102. Springer, 2000. [ bib | .dvi | .ps | .pdf ]
Lax logical relations are a categorical generalisation of logical relations; though they preserve product types, they need not preserve exponential types. But, like logical relations, they are preserved by the meanings of all lambda-calculus terms. We show that lax logical relations coincide with the correspondences of Schoett, the algebraic relations of Mitchell and the pre-logical relations of Honsell and Sannella on Henkin models, but also generalise naturally to models in cartesian closed categories and to richer languages.

[San00a]
Donald Sannella. Algebraic specification and program development by stepwise refinement. In Proc. 9th Intl. Workshop on Logic-based Program Synthesis and Transformation, LOPSTR'99, volume 1817 of Lecture Notes in Computer Science, pages 1-9. Springer, 2000. [ bib | .dvi | .ps | .pdf ]
Various formalizations of the concept of “refinement step” as used in the formal development of programs from algebraic specifications are presented and compared.

[HLST00]
Furio Honsell, John Longley, Donald Sannella, and Andrzej Tarlecki. Constructive data refinement in typed lambda calculus. In Proc. 3rd Intl. Conf. on Foundations of Software Science and Computation Structures. European Joint Conferences on Theory and Practice of Software (ETAPS 2000), volume 1784 of Lecture Notes in Computer Science, pages 161-176. Springer, 2000. [ bib | .dvi | .ps | .pdf ]
A new treatment of data refinement in typed lambda calculus is proposed, phrased in terms of pre-logical relations [HS99] rather than logical relations, and incorporating a constructive element. Constructive data refinement is shown to have desirable properties, and a substantial example of refinement is presented.

[San00b]
Donald Sannella. The Common Framework Initiative for algebraic specification and development of software. In Proc. 3rd Intl. Conf. on Perspectives of System Informatics (PSI'99), volume 1755 of Lecture Notes in Computer Science, pages 1-9. Springer, 2000. [ bib | .dvi | .ps | .pdf ]
The Common Framework Initiative (CoFI) is an open international collaboration which aims to provide a common framework for algebraic specification and development of software. The central element of the Common Framework is a specification language called CASL for formal specification of functional requirements and modular software design which subsumes many previous algebraic specification languages. This paper is a brief summary of past and present work on CoFI.

[ST99b]
Donald Sannella and Andrzej Tarlecki. Algebraic preliminaries. In Egidio Astesiano, Hans-Jörg Kreowski, and Bernd Krieg-Brückner, editors, Algebraic Foundations of Systems Specification, chapter 2. Springer, 1999. [ bib | .dvi | .ps | .pdf ]
[SW99]
Donald Sannella and Martin Wirsing. Specification languages. In Egidio Astesiano, Hans-Jörg Kreowski, and Bernd Krieg-Brückner, editors, Algebraic Foundations of Systems Specification, chapter 8. Springer, 1999. [ bib | .dvi | .ps | .pdf ]
[ST99a]
Donald Sannella and Andrzej Tarlecki. Algebraic methods for specification and formal development of programs. ACM Computing Surveys, 31(3es), 1999. [ bib | .dvi | .ps | .pdf ]
This note gives our personal perspective on the state of foundations of software specification and development including applications to the formal development of reliable complex software systems.

[HS99]
Furio Honsell and Donald Sannella. Pre-logical relations. In Proc. Computer Science Logic, CSL'99, volume 1683 of Lecture Notes in Computer Science, pages 546-561. Springer, 1999. The final full version of this is [HS02]. [ bib | .dvi | .ps | .pdf ]
We study a weakening of the notion of logical relations, called pre-logical relations, that has many of the features that make logical relations so useful as well as further algebraic properties including composability. The basic idea is simply to require the reverse implication in the definition of logical relations to hold only for pairs of functions that are expressible by the same lambda term. Pre-logical relations are the minimal weakening of logical relations that gives composability for extensional structures and simultaneously the most liberal definition that gives the Basic Lemma. The use of pre-logical relations in place of logical relations gives an improved version of Mitchell's representation independence theorem which characterizes observational equivalence for all signatures rather than just for first-order signatures. Pre-logical relations can be used in place of logical relations to give an account of data refinement where the fact that pre-logical relations compose explains why stepwise refinement is sound.

[BST99]
Michel Bidoit, Donald Sannella, and Andrzej Tarlecki. Architectural specifications in CASL. In Proc. 7th Intl. Conference on Algebraic Methodology and Software Technology (AMAST'98), volume 1548 of Lecture Notes in Computer Science, pages 341-357. Springer, 1999. An extended version appeared in [BST02a]. [ bib | .dvi | .ps | .pdf ]
One of the novel features of CASL, the Common Algebraic Specification Language, is the provision of so-called architectural specifications for describing the modular structure of software systems. A discussion of refinement of CASL specifications provides the setting for a presentation of the rationale behind architectural specifications. This is followed by details of the features provided in CASL for architectural specifications, hints concerning their semantics, and simple results justifying their usefulness in the development process.

[KS98]
Stefan Kahrs and Donald Sannella. Reflections on the design of a specification language. In Proc. Intl. Colloq. on Fundamental Approaches to Software Engineering. European Joint Conferences on Theory and Practice of Software (ETAPS'98), volume 1382 of Lecture Notes in Computer Science, pages 154-170. Springer, 1998. [ bib | .dvi | .ps | .pdf ]
We reflect on our experiences from work on the design and semantic underpinnings of Extended ML, a specification language which supports the specification and formal development of Standard ML programs. Our aim is to isolate problems and issues that are intrinsic to the general enterprise of designing a specification language for use with a given programming language. Consequently the lessons learned go far beyond our original aim of designing a specification language for ML.

[ST97]
Donald Sannella and Andrzej Tarlecki. Essential concepts of algebraic specification and program development. Formal Aspects of Computing, 9:229-269, 1997. [ bib | .dvi | .ps | .pdf ]
The main ideas underlying work on the model-theoretic foundations of algebraic specification and formal program development are presented in an informal way. An attempt is made to offer an overall view, rather than new results, and to focus on the basic motivation behind the technicalities presented elsewhere.

[An early short version of this is [ST92].]
[KST97a]
Stefan Kahrs, Donald Sannella, and Andrzej Tarlecki. The definition of Extended ML: A gentle introduction. Theoretical Computer Science, 173:445-484, 1997. The published version contains two typos: p461, rule at bottom: second gamma should be gamma'; p462, rule in middle: second premise should start with E. [ bib | .dvi | .ps | .pdf ]
Extended ML (EML) is a framework for the formal development of modular Standard ML (SML) software systems. Development commences with a specification of the behaviour required and proceeds via a sequence of partial solutions until a complete solution, an executable SML program, is obtained. All stages in this development process are expressed in the EML language, an extension of SML with axioms for describing properties of module components.

This is an overview of the formal definition of the EML language. To complement the full technical details presented elsewhere, it provides an informal explanation of the main ideas, gives the rationale for certain design decisions, and outlines some of the technical issues involved. EML is unusual in being built around a “real” programming language having a formally-defined syntax and semantics. Interesting and complex problems arise both from the nature of this relationship and from interactions between the features of the language.

[This is the final version of [KST94c]; a close-to-final version of this is: Report ECS-LFCS-95-322, Dept. of Computer Science, Univ. of Edinburgh, 1995.]
[KST97b]
Stefan Kahrs, Donald Sannella, and Andrzej Tarlecki. The definition of Extended ML, version 1.21. Revised version of [KST94a], 1997. [ bib | .dvi | .ps | .pdf ]
This document formally defines the syntax and semantics of the Extended ML language. It is based directly on the published semantics of Standard ML in an attempt to ensure compatibility between the two languages.

[San97]
Donald Sannella. What does the future hold for theoretical computer science? In Proc. 7th Intl. Joint Conf. on Theory and Practice of Software Development (TAPSOFT'97), volume 1214 of Lecture Notes in Computer Science, pages 15-19. Springer, 1997. [ bib | .dvi | .ps | .pdf ]
Prospects for research in theoretical computer science are discussed. The maintenance of a genuine link between theory and practice is seen as key to the future health of both.

[HS96]
Martin Hofmann and Donald Sannella. On behavioural abstraction and behavioural satisfaction in higher-order logic. Theoretical Computer Science, 167:3-45, 1996. [ bib | .dvi | .ps | .pdf ]
The behavioural semantics of specifications with higher-order logical formulae as axioms is analyzed. A characterization of behavioural abstraction via behavioural satisfaction of formulae in which the equality symbol is interpreted as indistinguishability, which is due to Reichel and was recently generalized to the case of first-order logic by Bidoit et al, is further generalized to this case. The fact that higher-order logic is powerful enough to express the indistinguishability relation is used to characterize behavioural satisfaction in terms of ordinary satisfaction, and to develop new methods for reasoning about specifications under behavioural semantics.

[This is the full version of [HS95].]
[ST96]
Donald Sannella and Andrzej Tarlecki. Mind the gap! Abstract versus concrete models of specifications. In Proc. 21st Intl. Symp. on Mathematical Foundations of Computer Science, volume 1113 of Lecture Notes in Computer Science, pages 114-134. Springer, 1996. [ bib | .dvi | .ps | .pdf ]
In the theory of algebraic specifications, many-sorted algebras are used to model programs: the representation of data is arbitrary and operations are modelled as ordinary functions. The theory that underlies the formal development of programs from specifications takes advantage of the many useful properties that these models enjoy.

The models that underlie the semantics of programming languages are different. For example, the semantics of Standard ML uses rather concrete models, where data values are represented as closed constructor terms and functions are represented as “closures”. The properties of these models are quite different from those of many-sorted algebras.

This discrepancy brings into question the applicability of the theory of specification and formal program development in the context of a concrete programming language, as has been attempted in the Extended ML framework for the formal development of Standard ML programs. This paper is a preliminary study of the difference between abstract and concrete models of specifications, inspired by the kind of concrete models used in the semantics of Standard ML, in an attempt to determine the consequences of the discrepancy.

[HS95]
Martin Hofmann and Donald Sannella. On behavioural abstraction and behavioural satisfaction in higher-order logic. In Proc. 20th Colloq. on Trees in Algebra and Programming. Intl. Joint Conf. on Theory and Practice of Software Development (TAPSOFT'95), volume 915 of Lecture Notes in Computer Science, pages 247-261. Springer, 1995. The final full version of this is [HS96]. [ bib | .dvi | .ps | .pdf ]
The behavioural semantics of specifications with higher-order logical formulae as axioms is analyzed. A characterization of behavioural abstraction via behavioural satisfaction of formulae in which the equality symbol is interpreted as indistinguishability, which is due to Reichel and was recently generalized to the case of first-order logic by Bidoit et al, is further generalized to this case. The fact that higher-order logic is powerful enough to express the indistinguishability relation is used to characterize behavioural satisfaction in terms of ordinary satisfaction, and to develop new methods for reasoning about specifications under behavioural semantics.

[HST94]
Robert Harper, Donald Sannella, and Andrzej Tarlecki. Structured presentations and logic representations. Annals of Pure and Applied Logic, 67:113-160, 1994. [ bib | .ps | .pdf ]
The purpose of a logical framework such as LF is to provide a language for defining logical systems suitable for use in a logic-independent proof development environment. All inferential activity in an object logic (in particular, proof search) is to be conducted in the logical framework via the representation of that logic in the framework. An important tool for controlling search in an object logic, the need for which is motivated by the difficulty of reasoning about large and complex systems, is the use of structured theory presentations. In this paper a rudimentary language of structured theory presentations is presented, and the use of this structure in proof search for an arbitrary object logic is explored. The behaviour of structured theory presentations under representation in a logical framework is studied, focusing on the problem of “lifting” presentations from the object logic to the metalogic of the framework. The topic of imposing structure on logic presentations, so that logical systems may themselves be defined in a modular fashion, is also briefly considered.

[Reviewed in MR 95i:03024 and Zbl 0809.03019; this is the extended final version of [HST89b] and [HST89c].]
[KST94c]
Stefan Kahrs, Donald Sannella, and Andrzej Tarlecki. The semantics of Extended ML: A gentle introduction. In Proc. Intl. Workshop on Semantics of Specification Languages, Workshops in Computing, pages 186-215. Springer, 1994. An extended and improved version is [KST97a]. [ bib | .ps | .pdf ]
Extended ML (EML) is a framework for the formal development of modular Standard ML (SML) software systems. Development commences with a specification of the behaviour required and proceeds via a sequence of partial solutions until a complete solution, an executable SML program, is obtained. All stages in this development process are expressed in the EML language, an extension of SML with axioms for describing properties of module components.

This is a report on the current state of the semantics of the EML specification language as in nears completion. EML is unusual in being built around a “real” programming language having a formal semantics. Interesting and complex problems arise both from the nature of this relationship and from interactions between the features of the language.

[KST94b]
Stefan Kahrs, Donald Sannella, and Andrzej Tarlecki. Interfaces and Extended ML. In Proc. ACM Workshop on Interface Definition Languages, pages 111-118. ACM SIGPLAN Notices 29(8), 1994. [ bib | .ps | .pdf ]
This is a position paper giving our views on the uses and makeup of module interfaces. The position espoused is inspired by our work on the Extended ML (EML) formal software development framework and by ideas in the algebraic foundations of specification and formal development. The present state of interfaces in EML is outlined and set in the context of plans for a more general EML-like framework with axioms in interfaces taken from an arbitrary logical system formulated as an institution. Some more speculative plans are sketched concerning the simultaneous use of multiple institutions in specification and development.

[KST94a]
Stefan Kahrs, Donald Sannella, and Andrzej Tarlecki. The definition of Extended ML. Report ECS-LFCS-94-300, University of Edinburgh, 1994. [ bib | .ps | .pdf ]
This document formally defines the syntax and semantics of the Extended ML language. It is based directly on the published semantics of Standard ML in an attempt to ensure compatibility between the two languages.

[Version 1; a later version is [KST97b].]
[ST93]
Donald Sannella and Andrzej Tarlecki. Algebraic specification and formal methods for program development: What are the real problems? In G. Rozenberg and A. Salomaa, editors, Current Trends in Theoretical Computer Science. Essays and Tutorials, pages 115-120. World Scientific, 1993. Originally published in EATCS Bulletin 41:134-137 (1990). [ bib | .ps | .pdf ]
The long-term goal of work on algebraic specification is formal development of correct programs from specifications via verified-correct refinement steps. Define a real problem to be an unsolved problem which lies on (or near) the path betwen the current state of the art and this ultimate goal. Long-term progress depends on solving these problems, so it seems worthwhile to attack the real problems before worrying about other issues.

It is perhaps surprising that there is little agreement concerning what these problems are, at least if one takes the problems being tackled as an indication of what various researchers think the real problems are. Some sort of consensus seems desirable to promote effective joint progress towards our common goal.

We list some (not all) of what we think are the real problems. In an attempt to spark controversy, some things which we think are not real problems are also listed. Neither of these lists is exhaustive.

[San93]
Donald Sannella. A survey of formal software development methods. In Richard Thayer and Andrew McGettrick, editors, Software Engineering: A European Perspective, pages 281-297. IEEE Computer Society Press, 1993. [ bib | .ps | .pdf ]
This paper is a survey of the state of the art in 1988 of research on methods for formal software development.

[Originally published as report ECS-LFCS-88-56, Dept. of Computer Science, Univ. of Edinburgh, 1988.]
[SST92]
Donald Sannella, Stefan Sokolowski, and Andrzej Tarlecki. Toward formal development of programs from algebraic specifications: Parameterisation revisited. Acta Informatica, 29(8):689-736, 1992. [ bib | .ps | .pdf ]
Parameterisation is an important mechanism for structuring programs and specifications into modular units. The interplay between parameterisation (of programs and of specifications) and specification (of parameterised and of non-parameterised programs) is analysed, exposing important semantic and methodological differences between specifications of parameterised programs and parameterised specifications. The extension of parameterisation mechanisms to the higher-order case is considered, both for parameterised programs and parameterised specifications, and the methodological consequences of such an extension are explored.

A specification formalism with parameterisation of an arbitrary order is presented. Its denotational-style semantics is accompanied by an inference system for proving that an object satisfies a specification. The formalism includes the basic specification-building operations of the ASL specification language and is institution independent.

[Reviewed in CR 9405-0310, CR 9503-0176; an early version of this, with an extended example in an appendix, appeared as report 6/90, Univ. Bremen, 1990.]
[ST92]
Donald Sannella and Andrzej Tarlecki. Toward formal development of programs from algebraic specifications: Model-theoretic foundations. In Proc. 19th Intl. Colloq. on Automata, Languages and Programming, volume 623 of Lecture Notes in Computer Science, pages 656-671. Springer, 1992. This is superceded by [ST97]. [ bib | .ps | .pdf ]
This paper presents in an informal way the main ideas underlying our work on the model-theoretic foundations of algebraic specification and program development. We attempt to offer an overall view, rather than new results, and focus on the basic motivation behind the technicalities presented elsewhere and on the conclusions from this work.

[SW92]
Donald Sannella and Lincoln Wallen. A calculus for the construction of modular Prolog programs. Journal of Logic Programming, 12:147-177, 1992. [ bib | .pdf ]
We present a module language for Prolog based on the theory of modularity underlying the Standard ML module system. The language supports the construction of hierarchically-structured programs from parameterised components and provides a form of structural data abstraction. A formal semantics is given for the system which translates modular programs into conventional programs.

[An extended abstract of this is [SW87].]
[BKL+91]
Michel Bidoit, Hans-Jörg Kreowski, Pierre Lescanne, Fernando Orejas, and Donald Sannella, editors. Algebraic System Specification and Development: A Survey and Annotated Bibliography, volume 501 of Lecture Notes in Computer Science. Springer, 1991. [ bib ]
[Reviewed in CR 9209-0662.]
[ST91b]
Donald Sannella and Andrzej Tarlecki. A kernel specification formalism with higher-order parameterisation. In Proc. 7th Workshop on Specification of Abstract Data Types, volume 534 of Lecture Notes in Computer Science, pages 274-296. Springer, 1991. [ bib | .ps | .pdf ]
A specification formalism with parameterisation of an arbitrary order is presented. It is given a denotational-style semantics, accompanied by an inference system for proving that an object satisfies a specification. The inference system incorporates, but is not limited to, a clearly identified type-checking component.

Special effort is made to carefully distinguish between parameterised specifications, which denote functions yielding classes of objects, and specifications of parameterised objects, which denote classes of functions yielding objects. To deal with both of these in a uniform framework, it was convenient to view specifications, which specify objects, as objects themselves, and to introduce a notion of a specification of specifications.

The formalism includes the basic specification-building operations of the ASL specification language. This choice, however, is orthogonal to the new ideas presented. The formalism is also institution-independent, although this issue is not explicitly discussed at any length here.

[Superceded by Section 7 of [SST92].]
[San91]
Donald Sannella. Formal program development in Extended ML for the working programmer. In Proc. 3rd BCS/FACS Workshop on Refinement, Workshops in Computing, pages 99-130. Springer, 1991. [ bib | .ps | .pdf ]
Extended ML is a framework for the formal development of programs in the Standard ML programming language from high-level specifications of their required input/output behaviour. It strongly supports the development of modular programs consisting of an interconnected collection of generic and reusable 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 gives rise to one or more proof obligations which must be proved in order to establish the correctness of that step. This paper is intended as a user-oriented summary of the Extended ML language and methodology. Theoretical technicalities are avoided whenever possible, with emphasis placed on the practical aspects of formal program development. An extended example of a complete program development in Extended ML is included.

[ST91a]
Donald Sannella and Andrzej Tarlecki. Extended ML: Past, present and future. In Proc. 7th Workshop on Specification of Abstract Data Types, volume 534 of Lecture Notes in Computer Science, pages 297-322. Springer, 1991. [ bib | .ps | .pdf ]
An overview of past, present and future work on the Extended ML formal program development framework is given, with emphasis on two topics of current active research: the semantics of the Extended ML specification language, and tools to support formal program development.

[KBS91]
Bernd Krieg-Brückner and Donald Sannella. Structuring specifications in-the-large and in-the-small: Higher-order functions, dependent types and inheritance in SPECTRAL. In Proc. Colloq. on Combining Paradigms for Software Development. Intl. Joint Conf. on Theory and Practice of Software Development (TAPSOFT'91), volume 494 of Lecture Notes in Computer Science, pages 103-120. Springer, 1991. [ bib | .ps | .pdf ]
SPECTRAL is an experiment in specification language design that tries to maintain compactness in spite of a number of orthogonal concepts. The design is based on Extended ML and PROSPECTRA, generalising and extending both approaches. Of particular concern are the means for structuring specifications and programs in-the-large and in-the-small. The language includes constructs for defining general higher-order functions yielding specifications or program modules. Concepts of subtyping and (object-oriented) inheritance are included to support the specification development process and to enhance re-usability. Much of the power of the language comes from the use of dependent types.

[HST89b]
Robert Harper, Donald Sannella, and Andrzej Tarlecki. Structure and representation in LF. In Proc. 4th IEEE Symp. on Logic in Computer Science, pages 226-237, 1989. Extended abstract; the final full version of this is [HST94]. [ bib | .pdf ]
The purpose of a logical framework such as LF is to provide a language for defining logical systems suitable for use in a logic-independent proof development environment. All inferential activity in an object logic (in particular, proof search) is to be conducted in the logical framework via the representation of that logic in the framework. An important tool for controlling search in an object logic is the use of structured theory presentations. In order to apply these ideas to the setting of a logical framework, we study the behavior of structured theory presentations under representation in a framework, focusing on the problem of “lifting” presentations from the object logic to the metalogic of the framework. We also consider imposing structure on logic presentations so that logical systems may themselves be defined in a modular fashion. This opens the way to a CLEAR-like language for defining both theories and logics in a logical framework.

[This is an extended abstract of [HST89c], which is a preliminary version of [HST94].]
[HST89c]
Robert Harper, Donald Sannella, and Andrzej Tarlecki. Structure and representation in LF. In Proc. 1989 Workshop on Programming Logic, pages 232-257, 1989. Extended abstract; the final full version of this is [HST94]. [ bib ]
[This is a longer version of [HST89b] and a preliminary version of [HST94].]
[HST89a]
Robert Harper, Donald Sannella, and Andrzej Tarlecki. Logic representation in LF. In Proc. 3rd Summer Conf. on Category Theory and Computer Science, volume 389 of Lecture Notes in Computer Science, pages 250-272. Springer, 1989. [ bib ]
The purpose of a logical framework such as LF is to provide a language for defining logical systems suitable for use in a logic-independent proof development environment. In previous work we have developed a theory of representation of logics in a logical framework and considered the behaviour of structured theory presentations under representation. That work was based on the simplifying assumption that logics are characterized as families of consequence relations on “closed” sentences. In this report we extend the notion of logical system to account for open formula, and study its basic properties. Following standard practice, we distinguish two types of logical system of open formulae that differ in the treatment of free variables, and show how they may be induced from a logical system of closed sentences. The technical notions of a logic presentation and a uniform encoding of a logical system in LF are generalized to the present setting.

[ST89]
Donald Sannella and Andrzej Tarlecki. Toward formal development of ML programs: Foundations and methodology. In Proc. Colloq. on Current Issues in Programming Languages. Intl. Joint Conf. on Theory and Practice of Software Development (TAPSOFT'89), volume 352 of Lecture Notes in Computer Science, pages 375-389. Springer, 1989. [ bib | .ps | .pdf ]
A formal methodology is presented for the systematic evolution of modular Standard ML programs from specifications by means of verified refinement steps, in the framework of the Extended ML specification language. Program development proceeds via a sequence of design (modular decomposition) coding and refinement steps. For each of these three kinds of steps, conditions are given which ensure the correctness of the result. These conditions seem to be as weak as possible under the constraint of being expressible as “local” interface matching requirements. Interfaces are only required to match up to behavioural equivalence, which is seen as vital to the use of data abstraction in program development.

[Long version: Report ECS-LFCS-89-71, Dept. of Computer Science, Univ. of Edinburgh, 1989.]
[ASS89]
Jaume Agustí, Carlos Sierra, and Donald Sannella. Adding generic modules to flat rule-based languages: A low-cost approach. In Proc. 4th Intl. Symp. on Methodologies for Intelligent Systems, pages 43-51. North Holland, 1989. [ bib | .pdf ]
[ST88b]
Donald Sannella and Andrzej Tarlecki. Specifications in an arbitrary institution. Information and Computation, 76:165-210, 1988. [ bib | .pdf ]
A formalism for constructing and using axiomatic specifications in an arbitrary logical system is presented. This builds on the framework provided by Goguen and Burstall's work on the notion of an institution as a formalisation of the concept of a logical system for writing specifications. We show how to introduce free variables into the sentences of an arbitrary institution and how to add quantifiers which bind them. We use this foundation to define a set of primitive operations for building specifications in an arbitrary institution based loosely on those in the ASL kernel specification language. We examine the set of operations which results when the definitions are instantiated in institutions of total and partial first-order logic and compare these with the operations found in existing specification languages. We present proof rules which allow proofs to be conducted in specifications built using the operations we define. Finally, we introduce a simple mechanism for defining and applying parameterised specifications and briefly discuss the program development process.

[Reviewed in MR 89d:68056 and Zbl 654.68017; an early short version was [ST84].]
[ST88d]
Donald Sannella and Andrzej Tarlecki. Toward formal development of programs from algebraic specifications: Implementations revisited. Acta Informatica, 25:233-281, 1988. [ bib | .ps | .pdf ]
The program development process is viewed as a sequence of implementation steps leading from a specification to a program. Based on an elementary notion of refinement, two notions of implementation are studied: constructor implementations which involve a construction “on top of” the implementing specification, and abstractor implementations which additionally provide for abstraction from some details of the implemented specification. These subsume most formal notions of implementation in the literature. Both kinds of implementations satisfy a vertical composition and a (modified) horizontal composition property. All the definitions and results are shown to generalise to the framework of an arbitrary institution, and a way of changing institutions during the implementation process is introduced. All this is illustrated by means of simple concrete examples.

[This is the final version of [ST87b].]
[San88a]
Donald Sannella. Algebraic specification and formal program development: Motivation, present state and future prospects. LFCS Newsletter, 1:7-10, 1988. [ bib ]
[ST88c]
Donald Sannella and Andrzej Tarlecki. Tools for formal program development: Some fantasies. LFCS Newsletter, 1:10-15, 1988. [ bib ]
[ST88a]
Donald Sannella and Andrzej Tarlecki. Recent Trends in Data Type Specification: 5th Workshop on Specification of Abstract Data Types - Selected Papers, volume 332 of Lecture Notes in Computer Science. Springer, 1988. [ bib ]
[BSD+88]
Alan Bundy, Donald Sannella, Roberto Desimone, Fausto Giunchiglia, Frank van Harmelen, Jane Hesketh, Peter Madden, Alan Smaill, Andrew Stevens, and Lincoln Wallen. Proving properties of logic programs: A progress report. In Proc. 1988 Alvey Technical Conference, pages 153-156, 1988. [ bib ]
[San88b]
Donald Sannella. Edinburgh University postgraduate examination questions in computation theory, 1978-1988. Report ECS-LFCS-88-64, University of Edinburgh, 1988. [ bib ]
[ST87a]
Donald Sannella and Andrzej Tarlecki. On observational equivalence and algebraic specification. Journal of Computer and System Sciences, 34:150-178, 1987. [ bib | .pdf ]
The properties of a simple and natural notion of observational equivalence of algebras and the corresponding specification-building operation are studied. We begin with a definition of observational equivalence which is adequate to handle reachable algebras only, and show how to extend it to cope with unreachable algebras and also how it may be generalised to make sense under an arbitrary institution. Behavioural equivalence is treated as an important special case of observational equivalence, and its central role in program development is shown by means of an example.

[Reviewed in MR 88j:68118 and CR 8808-0615; this is the final complete version of [ST85a].]
[ST87b]
Donald Sannella and Andrzej Tarlecki. Toward formal development of programs from algebraic specifications: Implementations revisited. In Proc. 12th Colloq. on Trees in Algebra and Programming. Intl. Joint Conf. on Theory and Practice of Software Development (TAPSOFT'87), volume 249 of Lecture Notes in Computer Science, pages 96-110. Springer, 1987. Extended abstract; the final full version of this is [ST88d]. [ bib | .pdf ]
The program development process is viewed as a sequence of implementation steps leading from a specification to a program. Based on an elementary notion of refinement, two notions of implementation are studied: constructor implementations which involve a construction “on top of” the implementing specification, and abstractor implementations which additionally provide for abstraction from some details of the implemented specification. These subsume most formal notions of implementation in the literature. Both kinds of implementations satisfy a vertical composition and a (modified) horizontal composition property. All the definitions and results generalise to the framework of an arbitrary institution.

[San87]
Donald Sannella. Formal specification of ML programs. In Jornadas Rank Xerox Sobre Inteligencia Artificial Razonamiento Automatizado, pages 79-98, 1987. [ bib | .ps | .pdf ]
A tutorial introduction to specifying ML programs using ideas from Extended ML

[WS87]
Martin Wirsing and Donald Sannella. Une introduction à la programmation fontionnelle: HOPE et ML. Technique et Science Informatiques, 6:517-525, 1987. [ bib ]
[A terrible english translation is: Introduction to Functional Programming: HOPE and ML. Technology and Science of Informatics 6:693-700 (1989).]
[SW87]
Donald Sannella and Lincoln Wallen. A calculus for the construction of modular Prolog programs. In Proc. 1987 IEEE Symp. on Logic Programming, pages 368-378, 1987. Extended abstract; the final full version of this is [SW92]. [ bib ]
We present a module language for Prolog based on the theory of modularity underlying the Standard ML module system. The calculus supports the construction of hierarchically-structured programs from parameterised components and provides a form of structural data abstraction. The system has a formal semantics which translates modular programs into conventional programs.

[ST86]
Donald Sannella and Andrzej Tarlecki. Extended ML: An institution-independent framework for formal program development. In Proc. Workshop on Category Theory and Computer Programming, volume 240 of Lecture Notes in Computer Science, pages 364-389. Springer, 1986. [ bib | .ps | .pdf ]
The Extended ML specification language provides a framework for the formal stepwise development of modular programs in the Standard ML programming language from specifications. The object of this paper is to equip Extended ML with a semantics which is completely independent of the logical system used to write specifications, building on Goguen and Burstall's work on the notion of an institution as a formalisation of the concept of a logical system. One advantage of this is that it permits freedom in the choice of the logic used in writing specifications; an intriguing side-effect is that it enables Extended ML to be used to develop programs in languages other than Standard ML since we view programs as simply Extended ML specifications which happen to include only “executable” axioms. The semantics of Extended ML is defined in terms of the primitive specification-building operations of the ASL kernel specification language which itself has an institution-independent semantics.

It is not possible to give a semantics for Extended ML in an institutional framework without extending the notion of an institution; the new notion of an institution with syntax is introduced to provide an adequate foundation for this enterprise. An institution with syntax is an institution with three additions: the category of signatures is assumed to form a concrete category; an additional functor is provided which gives concrete syntactic representations of sentences; and a natural transformation associates these concrete objects with the “abstract” sentences they represent. We use the first addition to “lift” certain necessary set-theoretic constructions to the category of signatures, and the other two additions to deal with the low-level semantics of axioms.

[Reviewed in MR 88f:68100; somewhat obsolete with respect to the current design of Extended ML but the technicalities are still relevant.]
[ST85c]
Donald Sannella and Andrzej Tarlecki. Some thoughts on algebraic specification. In Proc. 3rd Workshop on Theory and Applications of Abstract Data Types, volume 116 of Informatik-Fachberichte, pages 31-38. Springer, 1985. [ bib | .ps | .pdf ]
[Reviewed in Zbl 584.68036.]
[MS85]
David MacQueen and Donald Sannella. Completeness of proof systems for equational specifications. IEEE Trans. on Software Engineering, SE-11(5):454-461, 1985. [ bib | .pdf ]
Contrary to popular belief, equational logic with induction is not complete for initial models of equational specifications. Indeed, under some regimes (the Clear specification language and most other algebraic specification languages) no proof system exists which is complete even with respect to ground equations. A collection of known results is presented along with some new observations.

[Reviewed in Zbl 558.68017.]
[ST85a]
Donald Sannella and Andrzej Tarlecki. On observational equivalence and algebraic specification. In Proc. 10th Colloq. on Trees in Algebra and Programming. Intl. Joint Conf. on Theory and Practice of Software Development (TAPSOFT'85), volume 185 of Lecture Notes in Computer Science, pages 308-322. Springer, 1985. Extended abstract; the final full version of this is [ST87a]. [ bib | .pdf ]
The properties of a simple and natural notion of observational equivalence of algebras and the corresponding specification-building operation (observational abstraction) are studied. We begin with a definition of observational equivalence which is adequate to handle reachable algebras only, and show how to extend it to cope with unreachable algebras and also how it may be generalised to make sense under an arbitrary institution . Behavioural equivalence is treated as an important special case of observational equivalence, and its central role in program development is shown by means of an example.

[Long version: Report CSR-172-84, Dept. of Computer Science, Univ. of Edinburgh, 1984.]
[ST85b]
Donald Sannella and Andrzej Tarlecki. Program specification and development in Standard ML. In Proc. 12th ACM Symp. on Principles of Programming Languages, pages 67-77, 1985. [ bib | .pdf ]
An attempt is made to apply ideas about algebraic specification in the context of a programming language. Standard ML with modules is extended by allowing axioms in module interface specifications and in place of code. The resulting specification language, called Extended ML, is given a semantics based on the primitive specification-building operations of the kernel algebraic specification language ASL. Extended ML provides a framework for the formal development of programs from specifications by stepwise refinement, which is illustrated by means of a simple example. From its semantic basis Extended ML inherits complete independence from the logical system (institution) used to write specifications. This allows different styles of specification as well as different programming languages to be accommodated.

[Obsolete with respect to the current design of Extended ML.]
[San84]
Donald Sannella. A set-theoretic semantics for Clear. Acta Informatica, 21:443-472, 1984. [ bib | .pdf ]
A semantics for the Clear specification language is given. The language of set theory is employed to present constructions corresponding to Clear's specification-combining operations, which are then used as the basis for a denotational semantics. This is in contrast to Burstall and Goguen's 1980 semantics which described the meanings of these operations more abstractly via concepts from category theory.

[An early version is: A new semantics for Clear, Report CSR-79-81, Dept. of Computer Science, Univ. of Edinburgh, 1981.]
[ST84]
Donald Sannella and Andrzej Tarlecki. Building specifications in an arbitrary institution. In Proc. Intl. Symp. on Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 337-356. Springer, 1984. An extended and improved version is [ST88b]. [ bib | .pdf ]
A set of operations for constructing algebraic specifications in an arbitrary logical system is presented. This builds on the framework provided by Goguen and Burstall's work on the notion of an institution as a formalisation of the concept of a logical system for writing specifications. We show how to introduce free variables into the sentences of an arbitrary institution and how to add quantifiers which bind them. We use this foundation to define a set of primitive operations for building specifications in an arbitrary institution based loosely on those in the ASL kernel specification language, We examine the set of operations which results when the definitions are instantiated in an institution of first-order logic and compare these with the operations found in existing specification languages. The result of instantiating the operations in an institution of partial first-order logic is also discussed,

[Reviewed in CR 8505-0419.]
[SB83]
Donald Sannella and Rod Burstall. Structured theories in LCF. In Proc. 8th Colloq. on Trees in Algebra and Programming, volume 159 of Lecture Notes in Computer Science, pages 377-391. Springer, 1983. [ bib | .pdf ]
An extension to the Edinburgh LCF interactive theorem-proving system is described which provides new ways of constructing theories, drawing upon ideas from the Clear specification language. A new theory can be built from an existing theory in two new ways: by renaming its types and constants, or by abstraction (forgetting some types and constants and perhaps renaming the rest). A way of providing parameterised theories is described. These theory-building operations - together with operations for forming a primitive theory and for taking the union of theories - allow large theories to be built in a flexible and well-structured fashion. Inference rules and strategies for proof in structured theories are also discussed.

[SW83]
Donald Sannella and Martin Wirsing. A kernel language for algebraic specification and implementation. In Proc. 1983 Intl. Conf. on Foundations of Computation Theory, volume 158 of Lecture Notes in Computer Science, pages 413-427. Springer, 1983. [ bib | .pdf ]
A kernel specification language called ASL is presented. ASL comprises five fundamental but powerful specification-building operations and has a simple semantics. Behavioural abstraction with respect to a set of observable sorts can be expressed, and (recursive) parameterised specifications can be defined using a more powerful and more expressive parameterisation mechanism than usual. A simple notion of implementation permitting vertical and horizontal composition (i.e. it is transitive and monotonic) is adopted and compared with previous more elaborate notions. A collection of identities is given which can provide a foundation for the development of programs by transformation.

[Long version: Report CSR-131-83, Dept. of Computer Science, Univ. of Edinburgh, 1983.]
[San83]
Donald Sannella. Behavioural abstraction and algebraic specification. In Proc. 1983 Workshop on Semantics of Programming Languages, pages 153-166, 1983. [ bib ]
We argue that a proper notion of behavioural equivalence (a relation on algebras) is fundamental to the theory of program development. This view is supported by arguments from abstract data types, from program specification, and from stepwise refinement. Many different definitions of behavioural equivalence have appeared in the literature, but each definition yields one of three relations which differ only in their treatment of algebras containing unreachable data elements. Such algebras can be of use and so we adopt the relation which seems to treat them properly.

[SW82]
Donald Sannella and Martin Wirsing. Implementation of parameterised specifications. In Proc. 9th Intl. Colloq. on Automata, Languages and Programming, volume 140 of Lecture Notes in Computer Science, pages 473-488. Springer, 1982. [ bib | .pdf ]
A new notion is given for the implementation of one specification by another. Unlike most previous notions, this generalises to handle parameterised specifications as well as loose specifications (having an assortment of non-isomorphic models). Examples are given to illustrate the notion. The definition of implementation is based on a new notion of the simulation of a theory by an algebra. For the bulk of the paper we employ a variant of the Clear specification language [BG77] in which the notion of a data constraint is replaced by the weaker notion of a hierarchy constraint. All results hold for Clear with data constraints as well, but only under more restrictive conditions.

We prove that implementations compose vertically (two successive implementation steps compose to give one large step) and that they compose horizontally under application of (well-behaved) parameterised specifications (separate implementations of the parameterised specification and the actual parameter compose to give an implementation of the application).

[Long version: Report CSR-103-82, Dept. of Computer Science, Univ. of Edinburgh, 1982; reviewed in Zbl 492.68023.]
[San82]
Donald Sannella. Semantics, Implementation and Pragmatics of Clear, a Program Specification Language. PhD thesis, Department of Computer Science, University of Edinburgh, 1982. Report CST-17-82. [ bib ]
Specifications are necessary for communicating decisions and intentions and for documenting results at many stages of the program development process. Informal specifications are typically used today, but they are imprecise and often ambiguous. Formal specifications are precise and exact but are more difficult to write and understand. We present work aimed toward enabling the practical use of formal specifications in program development, concentrating on the Clear language for structured algebraic specification.

Two different but equivalent denotational semantics for Clear are given. One is a version of a semantics due to Burstall and Goguen with a few corrections, in which the category-theoretic notion of a colimit is used to define Clear's structuring operations independently of the underlying “institution” (logical formalism). The other semantics defines the same operations by means of straightforward set-theoretic constructions; it is not institution-independent but it can be modified to handle all institutions of apparent interest.

Both versions of the semantics have been implemented. The set-theoretic implementation is by far the more useful of the two, and includes a parser and typechecker. An implementation is useful for detecting syntax and type errors in specifications, and can be used as a front end for systems which manipulate specifications. Several large specifications which have been processed by the set-theoretic implementation are presented.

A semi-automatic theorem prover for Clear built on top of the Edinburgh LCF system is described. It takes advantage of the structure of Clear specifications to restrict the available information to that which seems relevant to proving the theorem at hand. If the system is unable to prove a theorem automatically the user can attempt the proof interactively using the high-level primitives and inference rules provided.

We lay a theoretical foundation for the use of Clear in systematic program development by investigating a new notion of the implementation of a specification by a lower-level specification. This notion extends to handle parameterised specifications. We show that this implementation relation is transitive and commutes with Clear's structuring operations under certain conditions. This means that a large specification can be refined to a program in a gradual and modular fashion, where the correctness of the individual refinements guarantees the correctness of the resulting program.

[BMS80]
Rod Burstall, David MacQueen, and Donald Sannella. HOPE: An experimental applicative language. In Proc. 1980 LISP Conference, pages 136-143, 1980. [ bib | .pdf ]
An applicative language called HOPE is described and discussed. The underlying goal of the design and implementation effort was to produce a very simple programming language which encourages the construction of clear and manipulable programs. HOPE does not include an assignment statement; this is felt to be an important simplification. The user may freely define his own data types, without the need to devise a complicated encoding in terms of low-level types. The language is very strongly typed, and as implemented it incorporates a typechecker which handles polymorphic types and overloaded operators. Functions are defined by a set of recursion equations; the left-hand side of each equation includes a pattern used to determine which equation to use for a given argument. The availability of arbitrary higher-order types allows functions to be defined which “package” recursion. Lazily-evaluated lists are provided, allowing the use of infinite lists which could be used to provide interactive input/output and concurrency. HOPE also includes a simple modularisation facility which may be used to protect the implementation of an abstract data type.


This file was generated by bibtex2html 1.96.