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

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)
References