Ebook: Alphard: Form and Content

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.

---

---

Content:
Front Matter....Pages i-viii
Publication History....Pages 1-4
Introduction History and Overview....Pages 5-10
Prelude The Alphard form and Verification Issues....Pages 11-13
Abstraction and Verification in Alphard: Introduction to Language and Methodology....Pages 15-60
Remarks on the Impact of Program Verification on Language Design....Pages 61-69
First Interlude Inadequacy of Simple Encapsulation....Pages 71-72
Abstraction and Verification in Alphard: Iteration and Generators....Pages 73-116
Achieving Quality Software: Reflections on the Aims and Objectives of Alphard....Pages 117-134
Second Interlude Larger Examples....Pages 135-137
Abstraction and Verification in Alphard: Design and Verification of a Tree Handler....Pages 139-159
Abstraction and Verification in Alphard: A Symbol Table Example....Pages 162-190
Third Interlude Language Evolution....Pages 191-193
(Preliminary) An Informal Definition of Alphard....Pages 195-252
Fourth Interlude Generality and Generic Definitions....Pages 253-253
An Alphard Specification of a Correct and Efficient Transformation on Data Structures....Pages 255-281
Fifth Interlude Validating and Extending the Concepts....Pages 283-284
Validating the Utility of Abstraction Techniques....Pages 285-293
Toward Relaxing Assumptions in Languages and Their Implementations....Pages 295-313
Postlude Reflections and Open Problems....Pages 315-321

---

Content:
Front Matter....Pages i-viii
Publication History....Pages 1-4
Introduction History and Overview....Pages 5-10
Prelude The Alphard form and Verification Issues....Pages 11-13
Abstraction and Verification in Alphard: Introduction to Language and Methodology....Pages 15-60
Remarks on the Impact of Program Verification on Language Design....Pages 61-69
First Interlude Inadequacy of Simple Encapsulation....Pages 71-72
Abstraction and Verification in Alphard: Iteration and Generators....Pages 73-116
Achieving Quality Software: Reflections on the Aims and Objectives of Alphard....Pages 117-134
Second Interlude Larger Examples....Pages 135-137
Abstraction and Verification in Alphard: Design and Verification of a Tree Handler....Pages 139-159
Abstraction and Verification in Alphard: A Symbol Table Example....Pages 162-190
Third Interlude Language Evolution....Pages 191-193
(Preliminary) An Informal Definition of Alphard....Pages 195-252
Fourth Interlude Generality and Generic Definitions....Pages 253-253
An Alphard Specification of a Correct and Efficient Transformation on Data Structures....Pages 255-281
Fifth Interlude Validating and Extending the Concepts....Pages 283-284
Validating the Utility of Abstraction Techniques....Pages 285-293
Toward Relaxing Assumptions in Languages and Their Implementations....Pages 295-313
Postlude Reflections and Open Problems....Pages 315-321
....