Accession Number : ADA288818
Title : SDVS Verification of a Stage 3 Ada Program.
Corporate Author : AEROSPACE CORP EL SEGUNDO CA ENGINEERING AND TECHNOLOGY GROUP
Personal Author(s) : Doner, J. E.
PDF Url : ADA288818
Report Date : 30 SEP 1992
Pagination or Media Count : 65
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