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.
This uniquely accessible textbook introduces students to computation using a very distinctive approach, quite rapidly leading them into essential topics with sufficient depth, yet in a highly intuitive manner. The work is anchored in coverage of functional programming (in Haskell), symbolic logic, and finite automata - each a critical component of the foundations of Informatics, and together offering students a clear glimpse into an intellectual journey beyond mere mastery of technical skills. From core elements like types, Venn diagrams and logic, to patterns of reasoning, sequent calculus, recursion and algebraic data types, the book spans the breadth of key concepts and methods that will enable students to readily progress with their studies in Computer Science.
[Available from Springer at link.springer.com/book/10.1007/978-3-030-76908-6 and from Amazon at www.amazon.com/dp/3030769070/.]
In recent years, there has been a shift of interest towards the field of biometric authentication, which proves the identity of the user using their biological characteristics. We explore a novel biometric based on the electrical activity of the human heart in the form of electrocardiogram (ECG) signals. In order to explore the stability of ECG as a biometric, we collect data from 55 participants over two sessions with a period of 4 months in between. We also use a consumer-grade ECG monitor that is more affordable and usable than a medical-grade counterpart. Using a standard approach to evaluate our classifier, we obtain error rates of 2.4% for data collected within one session and 9.7% for data collected across two sessions. The experimental results suggest that ECG signals collected using a consumer-grade monitor can be successfully used for user authentication.
Hartmut Ehrig and others in [EWT83] studied normal form results for complex generating constraints imposed on basic specifications. Since then this work has been followed by subsequent results concerning normal forms for structured specifications, typically built from basic specifications using union, translation and hiding. We consider generating constraints as additional specification-building operations and follow and extend the results concerning normal forms for the resulting specifications with various forms of generating constraints.
We propose and study a framework for systematic development of software systems (or models) from their formal specifications. We introduce a language for formal development by refinement and decomposition, as an extension to CASL. We complement it with a notion of refinement tree and present proof calculi for checking correctness of refinements as well as their consistency. Both calculi have been implemented in the Heterogeneous Tool Set (HETS), and have been integrated with other tools like model finders and conservativity checkers.
We recall the kernel algebraic specification language ASL and outline its main features in the context of the state of research on algebraic specification at the time it was conceived in the early 1980s. We discuss the most significant new ideas in ASL and the influence they had on subsequent developments in the field and on our own work in particular.
We propose a simple framework of algebraic constructions for software specification, modular design and development. Algebraic constructions generalise (parameterised) modules by allowing on one hand a rather arbitrary collection of elements to form the parameter and on the other hand dependencies between the module elements to be spelled out explicitly. Algebraic constructions are specified in a very natural way by means of ordinary algebraic specifications. They are combined using a sum operation which captures as special cases various operations on (parameterised) modules offered by standard specification and development frameworks. We show the expected composability result for the sum of algebraic constructions and of their specifications.
The notion of module extraction has been studied extensively in the ontology community. The idea is to extract, from a large ontology, ythose axioms that are relevant to certain concepts of interest (formalised as a subsignature). The technical concept used for the definition of module extraction is that of inseparability, which is related to indistinguishability known from observational specifications.Module extraction has been studied mainly for description logics and the Web Ontology Language OWL. In this work, we generalise previous definitions and results to an arbitrary inclusive institution. We reveal a small inaccuracy in the formal definition of inseparability, and show that some results hold in an arbitrary inclusive institution, while others require the institution to be weakly union-exact.
This work provides the basis for the treatment of module extraction within the institution-independent semantics of the distributed ontology, modeling and specification language (DOL), which is currently under submission to the Object Management Group (OMG).
ThreadSafe is a commercial static analysis tool that focuses on detection of Java concurrency defects. ThreadSafe's bug-finding capabilities and its look and feel are presented through examples of bugs found in the codebases of two widely-used open source projects.
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.
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.
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.]
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.
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.
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].]
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].]
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.
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.
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.
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.
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.
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.
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.]
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).]
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.
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).]
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.
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.
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.
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.
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.
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.
Various formalizations of the concept of “refinement step” as used in the formal development of programs from algebraic specifications are presented and compared.
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.
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.
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.
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.
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.
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.
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].]
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.]
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.
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.
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].]
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.
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.
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].]
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.
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.
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].]
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.
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.]
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.]
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.
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].]
[Reviewed in CR 9209-0662.]
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].]
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.
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.
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.
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].]
[This is a longer version of [HST89b] and a preliminary version of [HST94].]
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.
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.]
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].]
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].]
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].]
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.
A tutorial introduction to specifying ML programs using ideas from Extended ML
[A terrible english translation is: Introduction to Functional Programming: HOPE and ML. Technology and Science of Informatics 6:693-700 (1989).]
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.
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.]
[Reviewed in Zbl 584.68036.]
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.]
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.]
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.]
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.]
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.]
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.
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.]
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.
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.]
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.
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.