Example Proofs Using Offline Characterizations of Procedures in the State Delta Verification System (SDVS)

Abstract

This report presents two examples demonstrating the use of an offline characterization mechanism for Ada procedures. By offline characterization we mean the characterization of the actions of a procedure independent of context. The characterization is performed using the State Delta Verification System (SDVS). The subset of Ada in which procedures may be written is Stage 2 Ada, the subset of Ada recognized by SDVS in FY90. Section 2 presents background on the offline characterization mechanism. Section 3 gives a simple example of the offline characterization of an Ada subprogram, demonstrating the use of the characterization in a proof about an Ada program containing the subprogram. Section 4 gives a more complicated example, involving the offline characterization of two subprograms, one of which utilizes the other. Section 5 concludes this report.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 14, 1990
Accession Number
ADA235082

Entities

People

  • J. E. Doner
  • J. V. Cook

Organizations

  • The Aerospace Corporation

Tags

Communities of Interest

  • Space

DTIC Thesaurus Topics

  • Air Force
  • Air Force Facilities
  • Classification
  • Computer Science
  • Corporations
  • Coverings
  • Environment
  • High Level Languages
  • Lisp Programming Language
  • Security
  • Space Systems
  • Verification

Readers

  • Computer Science.
  • Database Systems and Applications
  • Materials Science (Mechanical Engineering).