Example Proofs Using Offline Characterizations of Procedures in the State Delta Verification System (SDVS)
J. V. Cook, John E. Doner · 1990
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.