Accession Number:

ADA028365

Title:

Abstraction and Verification in Alphard: Introduction to Language and Methodology

Descriptive Note:

Research rept.

Corporate Author:

UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST

Report Date:

1976-06-14

Pagination or Media Count:

50.0

Abstract:

Alphard is a programming language whose goals include supporting both the development of well-structured programs and the formal verification of these programs. This paper attempts to capture the symbiotic influence of these two goals on the design of the language. To that end the language description is interleaved with the presentation of a proof technique and discussion of programming methodology. Examples to illustrate both the language and the verification technique are included.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE