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

Subject Categories:

  • Computer Programming and Software
  • Computer Hardware

Distribution Statement:

APPROVED FOR PUBLIC RELEASE