Browse Prior Art Database

ABSTRACTION and VERIFICATION in ALPHARD Introduction to Language and Methodology Disclosure Number: IPCOM000128642D
Original Publication Date: 1976-Dec-31
Included in the Prior Art Database: 2005-Sep-16
Document File: 30 page(s) / 84K

Publishing Venue

Software Patent Institute

Related People

Wm. A. Wulf: AUTHOR [+5]


This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 5% of the total text.

Page 1 of 30


ABSTRACTION and VERIFICATION in ALPHARD Introduction to Language and Methodology

Wm. A. Wulf, Carnegie-Mellon University

Ralph L. London, USC Information Sciences Institute

Mary Shaw, Carnegie-Mellon University

June 14, 1976

Abstract: Alphard is a programming language whose goals include supp ' orting both the development of well-structured programs and the formal, verification of these progr . ams. 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.

Keywords and Phrases: abstraction and representation, abstract data types, assertions, correctness, data abstraction, data structures, extensible languages, information hiding, levels of abstraction, modular decomposition, program specifications, program verification, programming languages, programming methodology, proofs of correctness, protection,. structured programming, types, verification

The research described here was supported in part by the National Science Foundation (Grant DCR74-04187) and in part by the Defense Advanced Research Projects Agency (Contracts: F44620-73-C-0074, monitored by the Air Force Office of Scientific Research, and DAHC-15-72- C-0308). The views expressed are those of the authors. Page 2


Introduction 3 Preview of the Alphard Language 5

Verification of Forms I 8 Introduction to Alphard I 14

Example of a ForrnVorification: Restricted Stachs 21

Generalizing Form Definitions ; 24

Protection and Access Control 31

Another Example: Queues ............................................................................ ... 33

Conclusion I .. ............................ 39

References . .............. 42

Appendix A: Formal Definition of a Sequence 47

University of Southern California Page 1 Dec 31, 1976

Page 2 of 30

ABSTRACTION and VERIFICATION in ALPHARD Introduction to Language and Methodology

Preview of the Alphard Language.

A key concept in structured programming is abstraction: the retention of the essential properties of an object and the corollary neglect of inessential details. For example, all programming languages provide their users with an abstract machine from which inessential details such as the specific assignment of memory locations has been eliminated. Abstraction is important to structured programming precisely because it permits a programmer to ignore inessential detail and thereby reduce the apparent complexity of his task.

Several abstraction techniques have appeared in the literature on structured programming. For example, in stepwise refinement or top-down design, the top-level, abstract description of a program is refined to a description in a programming language in

Of course, in a certain sense...