Abstraction and Verification in Alphard: Introduction to Language and Methodology
UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
Pagination or Media Count:
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.
- Computer Programming and Software