D. Harel First-Order
Dynamic Logic, Lecture Notes in Computer Science, Vol. 68, Springer-Verlag,
New York, 1979.
Table of Contents
Part I: Binary-Relation Semantics
- Regular Propositional Dynamic Logic (PDL)
1.1 Elementary PDL (EPDL)
1.2 PDL
- Regular First-Order Dynamic Logic (DL)
2.1 Definitions
2.2 Descriptive Power
2.3 Variations
2.4 The Validity Problem for DL
- 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
- 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
- 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)
- 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)
- The Mathematics of Diverging and Failing II
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
Back to Top
Preface
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 |