A METHOD FOR DOCUMENTING CODE COMPONENTS

We propose a set of criteria for facilitating the rigorous understandi ng of code components via documentation and evaluate existing notation s and approaches with respect to these criteria. We present an overvie w of an analysis approach designed to generate program documentation t hat satisfies these criteria. Because of the inherent difficulty and i mportance of reasoning about loops, we focus on understanding and docu menting loops. We decompose loops into their component parts and obtai n formal specifications of the resulting loop fragments by use of a kn owledge base. We build this knowledge base for a specific application domain by designing plans that allow us to recognize stereotyped code patterns and associate them with their formal specifications. Finally, we synthesize a consistent and accurate specification of the whole lo op construct from the specifications of its fragments. To evaluate our loop analysis approach, a case study was performed on a preexisting p rogram of reasonable size. Results concerning the analyzed loops and t he plans designed for them are given. To generate formal documentation of complete program modules, we briefly describe how to integrate our loop analysis approach with an existing program analysis tool, FSQ(2) , which uses user-supplied loop specifications.