Program understanding plays an important role in nearly all software related tasks. This approach generates rigorous program documentation mechanically by combining and building on strengths of a practical program decomposition method, the axiomatic correctness notation, and the knowledge­ based analysis approaches.