Dynamic logics come from Pratt’s interpretation of Hoare triples and Hoare calculus in the formalism of modal logic. With the modality [α], we can express formally that all states reachable by executing α satisfy the formula A. This is done by writing [α]A. Thus, the Hoare triple {A}α{B} is simply captured by the PDL formula