Example Proofs Using Offline Characterizations of Procedures in the State Delta Verification System (SDVS)
AEROSPACE CORP EL SEGUNDO CA ENGINEERING GROUP
Pagination or Media Count:
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.
- Computer Programming and Software
- Computer Systems