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. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 29, 1976
- Accession Number
- ADA037768
Entities
People
- Mary Shaw
- Ralph L. London
- Wm. A. Wulf
Organizations
- Carnegie Mellon University