We propose a set of criteria for facilitating the rigorous understanding of code components via documentation and evaluate existing notations and approaches with respect to these criteria. We present an overview of an analysis approach designed to generate program documentation that satisfies these criteria. Because of the inherent difficulty and importance of reasoning about loops, we focus on understanding and documenting loops. We decompose loops into their component parts and obtain formal specifications of the resulting loop fragments by use of a knowledge 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 loop construct from the specifications of its fragments. To evaluate our loop analysis approach, a case study was performed on a preexisting program of reasonable size. Results concerning the analyzed loops and the 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.