DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click HERE
to register or log in.
SDVS Verification of a Stage 3 Ada Program.
AEROSPACE CORP EL SEGUNDO CA ENGINEERING AND TECHNOLOGY GROUP
Pagination or Media Count:
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.
APPROVED FOR PUBLIC RELEASE