First-Order Dynamic Logic

A-equivalent A-valid a,ße a>true abbreviate arithmetical completeness arithmetical universe array-DL asserts assignments and tests Assume atomic formula augmented AX(U axiom system binary relations CF'DL CFDL CFDL-wff Chapter class of programs complete axiomatization computation trees Computer Science concepts construct defined definition denote derived rule Dijkstra Diverging and Failing domain dynamic logic Edited elements EPDL equivalent execution expressive fact faila failure false finite first-order formula function symbol guarded commands language hence Hoare's holds iff induction inference rules infinite path intuition leaf leaf labeled Lemma Logics of Programs loopa method modal logic natural numbers nondeterministic Note notion obtain onenode partial correctness predicate symbol premises programming language provable prove r.e. programs random-DL recursive programs regular programs respectively result Section Seiten semantics term T(X terminate Theorem 3.1 total correctness true U-complete U-expressive uninterpreted valid DL-wffs var(a variables weakest precondition WPBG α α