This text presents the knowledge-based approach to the automation of program understanding which plays an important role in nearly all software related tasks: it is vital to the development, maintenance and re-use activities, and is useful in improving the quality of software development. The approach generates program documentation mechanically by combining and building on the strengths of a practical program decomposition method, the axiomatic correctness notation, and the knowledge-based analysis approach. This text is aimed at: computer science students at the advanced graduate level and researchers and practitioners interested in software development, maintenance and re-use.