Accession Number:
ADA037768
Title:
Abstraction and Verification in Alphard: A Symbol Table Example.
Descriptive Note:
Interim rept.,
Corporate Author:
CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Personal Author(s):
Report Date:
1976-12-29
Pagination or Media Count:
32.0
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
Descriptors:
Subject Categories:
- Computer Programming and Software
- Computer Hardware