Isolating and Transforming an Ada Heapsort for SDVS Analysis.

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.