Accession Number:

ADA002279

Title:

An Interactive Program Verification System

Descriptive Note:

Research rept.

Corporate Author:

UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST

Personal Author(s):

• Good, Donald I.
• London, Ralph L.
• Bledsoe, W. W.

Report Date:

1974-10-01

Pagination or Media Count:

32.0

Abstract:

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.

Descriptors:

• *COMPUTER PROGRAMMING
• BOOLEAN ALGEBRA
• RECURSIVE FUNCTIONS

Subject Categories:

• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE