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

摘要

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.