Abstract
One school holds that a program should be developed hand-in-hand with a proof that the program satisfies its specification [Dijkstra76, Gries81]. Support for this programming methodology can be provided in the form of a proof editor that permits a programmer to create and modify program proofs. The editor provides the programmer with feedback about errors that exist in a proof as it is developed, using knowledge embedded within the editor of the programming logic’s inference rules [Reps84].
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1989 Springer-Verlag New York Inc.
About this chapter
Cite this chapter
Reps, T.W., Teitelbaum, T. (1989). Interactive Program Verification. In: The Synthesizer Generator. Texts and Monographs in Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-1-4613-9623-9_10
Download citation
DOI: https://doi.org/10.1007/978-1-4613-9623-9_10
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4613-9625-3
Online ISBN: 978-1-4613-9623-9
eBook Packages: Springer Book Archive