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. This paper designs, implements, and verifies a general symbol table mechanism. This example is rich enough to allow an illustration of 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 29, 1976
- Accession Number
- ADA035461
Entities
People
- Mary Shaw
- Ralph L. London
- William A. Wulf
Organizations
- University of Southern California