D. Harel First-Order Dynamic Logic, Lecture Notes in Computer Science, Vol. 68, Springer-Verlag, New York, 1979.

Table of Contents

~ Book info. from Amazon
~ Book info. from Barnes & Noble

Table of Contents

Part I: Binary-Relation Semantics

  1. Regular Propositional Dynamic Logic (PDL)
    1.1 Elementary PDL (EPDL)
    1.2 PDL
  2. Regular First-Order Dynamic Logic (DL)
    2.1 Definitions
    2.2 Descriptive Power
    2.3 Variations
    2.4 The Validity Problem for DL
  3. Arithmetical Axiomatization
    3.1 The Theorem of Completeness and Arithmetical Universes
    3.2 Axiomatization of DL
    3.3 A Derived Axiomatization of DDL
    3.4 Related Work
  4. Recursive Programs: Context-free Dynamic Logic (CFDL)

    4.1 Definitions
    4.2 Results
    4.3 Axiomatization of CFDL
    4.4 Mutual Recursion

Part II: Computation-Tree Semantics

  1. Computation Trees, Total Correctness and Weakest Preconditions

    5.1 Motivation
    5.2 Computation Trees, Diverging and Failing
    5.3 Execution Methods and Total Correctness
    5.4 Weakest Preconditions
    5.5 The Guarded Commands Language (GC)

  2. The Mathematics of Diverging and Failing I
    6.1 Diverging and Failing in DL
    6.2 DL Augmented with loop (DL+)
    6.3 A Pattern of Reasoning
    6.4 DL with an Iteration Quantifier (ADL)
  3. The Mathematics of Diverging and Failing II
  4. 7.1 Computation Trees for Recursive Programs
    7.2 Diverging and Failing in CFDL
    7.3 CFDL Augmented with loop (CFDL+)
    7.4 Language Dependent Diverging and Failing

Appendix A: Example of a Proof of a DL-wff in P(N)
Appendix B: Example of a Proof of a CFDL-wff in R(N)
Appendix C: Example of a Proof of a DL+-wff in P+(N)
Appendix D: Example of a Proof of a CFDL+-wff in R+(N)

Back to Top



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 propositional) 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.

Back to Top