Isolating and Transforming an Ada Heapsort for SDVS Analysis.

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 30, 1992
Accession Number
ADA288830

Entities

People

  • L. A. Campbell

Organizations

  • The Aerospace Corporation

Tags

Communities of Interest

  • Space

DTIC Thesaurus Topics

  • Computer Programs
  • Computer Science
  • Computers
  • Contracts
  • Encapsulation
  • Engineering
  • Language
  • National Security
  • Personality
  • Production
  • Prototypes
  • Public Relations
  • Reliability
  • Security
  • Semantics
  • Translations

Fields of Study

  • Engineering

Readers

  • Computational Linguistics
  • Computer Programming and Software Development.
  • Systems Analysis and Design