Hoare logic is an important basis for formal verification of imperative programs. This chapter presents Hoare triples for the basic constructs of an imperative program, illustrating through examples how the correctness of the program is established in Hoare logic. Except loop invariants, it describes how verification conditions are generated automatically. This automated process is illustrated by a Prolog program. Some heuristics for generating good loop invariants are also presented.