Accession Number : ADA288830

Title :   Isolating and Transforming an Ada Heapsort for SDVS Analysis.

Corporate Author : AEROSPACE CORP EL SEGUNDO CA ENGINEERING AND TECHNOLOGY GROUP

Personal Author(s) : Campbell, L. A.

PDF Url : ADA288830

Report Date : 30 SEP 1992

Pagination or Media Count : 34

Abstract : This report examines some of the issues that arise when the State Delta Verification System (SDVS) is used for the analysis of code fragments extracted from larger bodies of 'production' code. The code fragment must be isolated from the larger body of code - by narrowing its interface to other program components. It must often be altered as well, to satisfy the narrowed interface semantics or to match available SDVS capabilities. These issues are illustrated by means of a running example, involving a heapsort written in Ada. The code is prepared for SDVS analysis, with the intention of proving that index-out-of-range conditions cannot arise during execution. A bug is uncovered in the original source code in the course of the analysis and the bug is fixed. The planned proof is then successfully carried out for the corrected heapsort code. The point of view is that of a relatively unsophisticated user of the SDVS system.

Descriptors :   *SOFTWARE ENGINEERING, *CODING, *SYSTEMS ANALYSIS, *DEBUGGING(COMPUTERS), SOURCES, PRODUCTION, VERIFICATION, INTERFACES, SEMANTICS, FRAGMENTS.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE