View article

Among the many approaches to formal reasoning about programs, Dynamic Logic enjoys the singulax aclv~ ntage of being strongly related to classical logic. Its variants constitute natural generalizations and extensions of classical formalisms. For example, Prepositional Dynamic Logic (PDL) can be described as a blend of three complementary classical ingredients: prepositional calculus, modal logic, and the algebra of regular events. In First-Order Dynamic Logic (DL), the prepositional calculus is replaced by classical first-order predicate calculus. Dynamic Logic is a system of remarl~ ble unity that is theoretically rich as well as of practical v'~ lue. It can be used for formalizing correctness specifications and proving rigorously that those specifications are met by a particular program. Other uses include determining the equlv'~ lence of programs, comparing the expressive power of various programming constructs …