Accession Number:

ADA288818

Title:

SDVS Verification of a Stage 3 Ada Program.

Descriptive Note:

Corporate Author:

AEROSPACE CORP EL SEGUNDO CA ENGINEERING AND TECHNOLOGY GROUP

Personal Author(s):

• Doner, J. E.

Report Date:

1992-09-30

Pagination or Media Count:

65.0

Abstract:

We describe all SDVS correctness proof for a fragment of operational code. This code implements a minor variant of the familiar bubble-sort algorithm, and uses for-loops and the record structure-Ada features that are either new with this version of the SDVS translator, or not previously exercised extensively. The proof demonstrates these features of SDVS, and is interesting because of the techniques used and the light it throws on possible improvements and enhancements for SDVS. We also discuss some data security problems and the ability of SDVS to treat them.

Descriptors:

• *COMPUTER PROGRAM VERIFICATION
• *ADA PROGRAMMING LANGUAGE
• ALGORITHMS
• DATA PROCESSING SECURITY
• TRANSLATORS

Subject Categories:

• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE