An Interactive Program Verification System
UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
Pagination or Media Count:
This paper is an initial progress report on the development of an interactive system for verifying that computer programs meet given formal specifications. The system is based on the conventional inductive assertion method given a program and its specifications, the object is to generate the verification conditions, simplify them, and prove what remains. This system addresses two aspects of software improvement of extreme importance to the military increase in the quality of software and decrease in the cost of producing high-quality software. A general description is given of the overall design philosophy, structure, and functional components of the system, and a simple sorting program is used to illustrate both the behavior of major system components and the type of user interaction the system provides.
- Computer Programming and Software