SDVS Verification of a Stage 3 Ada Program.

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.

Open PDF

Document Details

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

Entities

People

  • J. E. Doner

Organizations

  • The Aerospace Corporation

Tags

DTIC Thesaurus Topics

  • Algorithms
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Coverings
  • Environment
  • High Level Languages
  • Information Security
  • Language
  • Lisp Programming Language
  • National Security
  • Operating Systems
  • Permutations
  • Personal Computers
  • Security
  • Side Effects

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.