Abstraction and Verification in Alphard: Introduction to Language and Methodology
- 14 June 1976
- report
- Published by Defense Technical Information Center (DTIC)
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.Keywords
This publication has 0 references indexed in Scilit: