Browse Prior Art Database

ABSTRACTION and VERIFICATION in ALPHARD: Iteration and Generators Disclosure Number: IPCOM000128643D
Original Publication Date: 1976-Dec-31
Included in the Prior Art Database: 2005-Sep-16
Document File: 26 page(s) / 69K

Publishing Venue

Software Patent Institute

Related People

Mary Shaw: AUTHOR [+5]


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

Page 1 of 26


ABSTRACTION and VERIFICATION in ALPHARD: Iteration and Generators

Mary Shaw, Carnegie-Mellon University

Wm. A. Wulf, Carnegie-Mellon University

Ralph L. London, USC Information Sciences Institute

.August 20, 1976


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 import-ant 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 soecification and verification techniques that allow the properties of such iteration'. to be e . xpressed in the form of proof rules. We also provide a means of showing that a generator will te.rminate and obtain results for common special cases that are essentially identical to the corresponding constructs in other languages~

Keywords and Phrases:. abstraction and representation, abstract data types, assertions, control specialization, correctness, generators, invariants, iteration statements, modular decomposition, program specifications, programming languages., programming methodology, proofs of correctness, 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. This report is one in a series being printed jointly by CMU and ISI. Page 2


Introduction i I 3

Form Extensions 5 Iteration Constructs in Alphard 6 Defining and Verifying Generators 9 Proof Rules for Loops 13 Special Cases and Examples 19 Termination of'Generators 23 Example: Finite Sets 25

Conclusions e 36 References I 38

Appendix A: Informal Description of Verification Methodology 39

University of Southern California Page 1 Dec 31, 1976

Page 2 of 26

ABSTRACTION and VERIFICATION in ALPHARD: Iteration and Generators

Appendix 8: Derivations of Simplified Proof Rules ...... 40

Form Extensions

In this section we introduce another language facility which makes it more convenient to define certain abstractions and to manage the definitions after they are written. The facility allows a programmer to define one form as an extension of another. The new form will have most or all of the properties of the old one, plus some additional ones. (This mechanism Is similar to, and derived from, the class concatenation mechanism of Simula [DA172]., We introduce this mechanism at this point because it Is needed for generator definitions, which will be discussed in the next section.

The following ske...