A tool for assisting the understanding and formal development of software
Salwa K. Abd–El–Hafiz, Victor Robert Basili · University Libraries (University of Maryland) · 1993
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.