This is a research monograph intended primarily for those researchers in
Theoretical Computer Science interested in the areas of logics of programs,
programming language semantics and program verification. It is also aimed at
mathematically-inclined researchers in Logic, Linguistics and Philosophy,
interested in a well-motivated application of ideas from modal logic. The theory
developed here, although deriving its motivation and part of its terminology from
programming theory, can be viewed as a theory for reasoning about action in
general; hence the term dynamic logic.
Dynamic Logic (DL) is covered on the first-order (rather than the
proposltional) level. Regular DL, context-free DL and versions of them for
treating infinite computations (or actions) are defined and analyzed, and a
complete proof theory is developed for proving that formulae of these logics are
valid in arithmetical universes. Various notions of correctness of programs with
respect to their specifications are investigated within the DL framework.
This monograph constitutes a revised version of the author's doctoral
dissertation, submitted to the department of Electrical Engineering and Computer
Science of the Massachusetts Institute of Technology in May 1978.