Accession Number:

ADA235082

Title:

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

Descriptive Note:

Corporate Author:

AEROSPACE CORP EL SEGUNDO CA ENGINEERING GROUP

Personal Author(s):

Report Date:

1990-12-14

Pagination or Media Count:

44.0

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.

Subject Categories:

  • Computer Programming and Software
  • Computer Systems

Distribution Statement:

APPROVED FOR PUBLIC RELEASE