Demonstrates the close links between construction, proof, and analysis of programs. Introduces the basic elements that allow proof and analysis of iterative programs to be carried out and introduces the concept of recursive programming. Also shows how a recursive program can be converted into an iterative program. Offers numerous, clearly presented examples.