The Hoare calculus from Hoare [1969] is a landmark for logics of programs. It concerns the truth of statements of the form {A}α{B}—meaning that with the precondition A the program α always has B as a post-condition—and is defined axiomatically. It comes from a want of rigorous methods to reason about the properties of programs, and thus giving to the activity of programming a certain place in the realm of science. Burstall [1974] saw the analogy between modal logics and reasoning about programs, but the actual work on it started with Pratt [1976] when it was suggested to him by R. Moore, a student of his at the time. PDL comes from Pratt’s interpretation of Hoare’s calculus in the formalism of modal logic. An introduction to the genesis of PDL can be found in Pratt [1980b]. The Hoare-triple {A}α{B} is captured by the PDL formula A → [α]B meaning literally that if A is true, then every successfully terminating execution of α will end with B being true. With this connection realized, it is a routine to prove the initial rules of Hoare’s calculus using exclusively the axiomatization of PDL. This is something we will do in detail in section 3 which concentrates on the reasoning about the correctness of structured programs. 