A Tool for Assisting the Understanding and Formal Development of Software
Abstract
This paper presents a program understanding tool which documents programs by generating predicate logic annotations of their loops. The tool is based on an analysis by decomposition approach which utilizes a knowledge-base of plans in recognizing the high-level concepts in programs. Using data. :flow analysis, the decomposition encapsulates closely related statements in separate parts, ca1.led events, which can be analyzed individually. The :first order predicate logic annotations of loops a.re synthesized from these individual analysis results. A summary of the results of a ca.se study, performed on a pre-existing program of reasonable size, is given. The loops in this study, which a.re used as input data. to the tool, serve to validate our analysis approach. Finally, different applications of the tool, including the application of assisting the formal development of software, a.re discussed. This discussion focuses on how the tool can help in Validating the proof obligations generated during the last stage of the operation refinement process of VDM and Z.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1993
- Accession Number
- AD1005522
Entities
People
- S. K. Abd-el-hafiz
- V. R. Basili
Organizations
- University of Maryland