Skip to main content
main-content

Über dieses Buch

Alphard is a design for a programming system that supports the abstraction and verification techniques required by modern program'ming methodology. During the language design process, we were concerned simultaneously with problems of methodology, correctness, and efficiency. Methodological concerns are addressed through facilities for defining new, task·specific abstractions that capture complex notions in terms of their intended properties, without explicating them in terms of specific low· level implementations. Techniques for verifying certain properties of these programs address the correctness concerns. Finally, the language has been designed to permit compilation to efficient object code. Although a compiler was not implemented, the research shed light on specification issues and on programming methodology. an abstraction, specifying its behavior Alphard language constructs allow a programmer to isolate publicly while localizing knowledge about its implementation. The verification of such an abstraction consists of showing that its implementation behaves in accordance with the public specification. Given such a verification, the abstraction may be used with confidence to construct higher·level, more abstract, programs. The most common kind of abstraction in Alphard corresponds to what is now called an abstract data type. An abstract data type comprises a set of values for elements of the type and a set of operations on those values. A new language construct, the form, provides a way to encapsulate the definitions of data structures and operations in such a way that only public information could be accessed by the rest of the program.

Inhaltsverzeichnis

Frontmatter

Publication History

Abstract
The Alphard research on abstraction techniques has been presented in a number of articles and reports. These appeared over a period of several years, and the language was evolving as the papers were written. A discussion of the chronology of these papers may help to clarify the relations among them.
Mary Shaw

Introduction History and Overview

Abstract
When this work was originally conceived in the early 1970s, the concepts associated with the phrase “structured programming” were less clearly perceived than they are now, and the notion of “abstract data type” did not exist. While it was generally recognized that methodological approaches to the solution of software problems had enormous potential, there was neither agreement on the methodology nor much experience on which to base belief in the potential.
Mary Shaw

Prelude The Alphard form and Verification Issues

Abstract
This section presents a brief, informal introduction to the Alphard form, the linguistic mechanism we use to define abstractions. Our purpose is primarily to relate the mechanism to its goals, not to explicate it fully; the details are given in the papers that make up this volume.
Mary Shaw

Part One. Abstraction and Verification in Alphard: Introduction to Language and Methodology

Abstract
Alphard is a programming language whose goals include supporting both the development of well-structured programs and the formal verification of these programs. This paper attempts to capture the symbiotic influence of these two goals on the design of the language. To that end the language description is interleaved with the presentation of a proof technique and discussion of programming methodology. Examples to illustrate both the language and the verification technique are included.
Wm. A. Wulf, Ralph L. London, Mary Shaw

Part Two. Remarks on the Impact of Program Verification on Language Design

Abstract
The interactions between program verification and language design are deeper than just providing assertion statements. Experience with this interaction has been provided by the designs of two programming languages, Euclid and Alphard, each of which has verification as one of its important goals. Verification converns in Euclid were important in controlling, for example, the use of global variables, aliasing, and pointers. In Alphard verification exposed the need for specification of the various objects and operations, and at the same time focussed attention on programming methodology concerns that would otherwise have been missed. Verification serves as an evaluator of language designs by asking how one might verify a language feature, or more generally, by asking what are appropriate axiomatic definitions or proof rules for the language. Even if programs are not verified, the concern for verifiability leads both to better language designs and to better program designs.
Ralph L. London

First Interlude Inadequacy of Simple Encapsulation

Abstract
A little experience with the use of abstract data types shows that it often isn’t entirely possible to hide the implementation of a type. A common example arises in the case where a data structure is used to contain a collection of individual values and the program needs to iterate systematically through these values. Unless the programming language provides a way to access these values through the abstract data type, the application program will have to make explicit references to the data structure, thereby compromising any attempt to suppress and localize details of the implementation.
Mary Shaw

Part Three. Abstraction and Verification in Alphard: Iteration and Generators

Abstract
The Alphard form provides the programmer with a great deal of control over the implementation of abstract data types. In this report we extend the abstraction techniques from simple data representation and function definition to the iteration statement, the most important point of interaction between data and the control structure of the language itself. We introduce a means of specializing Alphard’s loops to operate on abstract entities without explicit dependence on the representation of those entities. We develop specification and verification techniques that allow the properties of such iterations to be expressed in the form of proof rules. We also provide a means of showing that a generator will terminate and obtain results for common special cases that are essentially identical to the corresponding constructs in other languages.
Mary Shaw, Wm. A. Wulf, Ralph L. London

Part Four. Achieving Quality Software: Reflections on the Aims and Objectives of Alphard

Abstract
The design of the Alphard language responded to concerns from several areas, including programming methodology, specification and verification, and object code efficiency. There is often tension among these concerns, with different concerns favoring different language decisions. This paper describes the interaction of the three concerns in the language design and in particular in the design of the iteration facility.
Wm. A. Wulf, Mary Shaw, Ralph L. London

Second Interlude Larger Examples

Abstract
The papers in the next two Parts present complete examples. The examples include specifications, code, and verification. They are large enough to show how the language features interact in real programs; indeed, they were selected for that purpose.
Mary Shaw

Part Five. Abstraction and Verification in Alphard: Design and Verification of a Tree Handler

Abstract
The design of the Alphard programming language has been strongly influenced by ideas from the areas of programming methodology and formal program verification. The interaction of these ideas and their influence on Alphard are described by developing a nontrivial example, a program for manipulating the parse tree of an arithmetic expression.
Mary Shaw

Part Six. Abstraction and Verification in Alphard: A Symbol Table Example

Abstract
The design of the Alphard programming language has been strongly influenced by ideas from the areas of programming methodology and formal program verification. In this paper we design, implement, and verify a general symbol table mechanism. This example is rich enough to allow us to illustrate the use as well as the definition of programmer-defined abstractions. The verification illustrates the power of the form to simplify proofs by providing strong specifications of such abstractions.
Ralph L. London, Mary Shaw, Wm. A. Wulf

Third Interlude Language Evolution

Abstract
After writing up the examples of Parts Five and Six, we set out to complete the language design. The chief issues in the design completion were the rules for strong typing, the semantics for sharing, scope rules, ways to do pointers and addressing, storage allocation – and making a complete, consistent definition. The summer of 1977 was spent on these issues, and the report was written in the fall and winter of 1977–78. The preliminary language report appeared as a Carnegie-Mellon University technical report. No final report was issued; the reasons are discussed in the Postlude.
Mary Shaw

Part Seven. (Preliminary) An Informal Definition of Alphard

Abstract
The Alphard language was designed to support the joint goals of facilitating contemporary programming methodology, encouraging formal specification of programs and verification of those specifications, allowing the programmer to exercise control over details that affect performance, and being able to compile compact, efficient code. This report presents the informal definition of the complete language.
Paul Hilfinger, Gary Feldman, Robert Fitzgerald, Izumi Kimura, Ralph L. London, K. V. S. Prasad, V. R. Prasad, Jonathan Rosenberg, Mary Shaw, Wm. A. Wulf

Fourth Interlude Generality and Generic Definitions

Abstract
After some experience with the definitions and use of Alphard, we realized that generic definitions — form and routine defintions that take types as parameters — provide a rich abstraction tool when coupled with careful specification of the properties of the generic parameters.
Mary Shaw

Part Eight. An Alphard Specification of a Correct and Efficient Transformation on Data Structures

Abstract
In this paper we study standard program components applicable to a wide variety of design tasks; we choose for this study the specific problem domain of data structures for general searching problems. Within this domain Bentley and Saxe have developed transformations for converting solutions of simple searching problems to solutions of more complex problems. We discuss one of those transformations, specify precisely the transformation and its conditions of applicability, and prove its correctness; we accomplish this by casting it in terms of abstract data types — specifically by using the Alphard form mechanism. We also demonstrate that the costs of the structures derived by this transformation are only slightly greater than the costs of the original solutions. The transformation we describe has already been used to develop a number of new algorithms, and it represents a new level of generality in software engineering tools.
Jon Louis Bentley, Mary Shaw

Fifth Interlude Validating and Extending the Concepts

Abstract
The last two papers in this volume are concerned not so much with Alphard as with the lessons to be learned from the abstract data type research of which Alphard was a part. One paper addresses the problem of discovering whether the ideas surrounding the notion “abstract data type” are in fact as much of a contribution to programming methodology as we believe they are. The other paper deals with some problems of definitional power in languages that became apparent during the abstract data type research; it brings together examples from several languages to define a problem that is, as yet, unsolved.
Mary Shaw

Part Nine. Validating the Utility of Abstraction Techniques

Abstract
A number of recent research efforts have been based on the hypothesis that encapsulation techniques, formal specification, and verification lead to significant improvements in program quality. As we gain experience with the language facilities produced by this research, we should attempt to validate that hypothesis. This paper poses this validation as the next major task in this area and outlines some ways to address it.
Mary Shaw, Gary Feldman, Robert Fitzgerald, Paul Hilfinger, Izumi Kimura, Ralph L. London, Jonathan Rosenberg, Wm. A. Wulf

Part Ten. Toward Relaxing Assumptions in Languages and Their Implementations

Abstract
Language implementors frequently make pre-emptive decisions concerning the exact implementations of language features. These decisions constrain programmers’ control over their computations and may tempt them to write involuted code to obtain special (or efficient) effects. In many cases, we can distinguish some properties of a language facility that are essential to the semantics and other properties that are incidental. Recent abstraction techniques emphasize dealing with such distinctions by separating the properties that are necessary to preserve the semantics from the details for which some decision must be made but many choices are adequate. We suggest here that these abstraction techniques can be applied to the problem of pre-emptive language decisions by specifying the essential properties of language facilities in a skeleton base language and defining interfaces that will accept a variety of implementations that differ in other details.
Mary Shaw, Wm. A. Wulf

Postlude Reflections and Open Problems

Abstract
As we gained experience with Alphard, both our ideas about Alphard itself and our ideas about methodology and language design evolved. It was possible for some of these new perceptions to feed back directly into Alphard. Others, however, required a significant departure from decisions already in place. In this final set of retrospective notes we assess the impact of the Alphard work and discuss some of the ideas that can serve as points of departure for new work. We begin with some remarks on Alphard itself — its status, its impact, and some design decisions we would now make differently. We then discuss some issues that have emerged from the abstract data type research and that remain as open research questions.
Mary Shaw
Weitere Informationen