Abstract
These therories describe Hoare logics for a number of imperative language constructs, from while-loops to mutually recursive procedures. Both partial and total correctness are treated. In particular a proof system for total correctness of recursive procedures in the presence of unbounded nondeterminism is presented.
License
Topics
Related publications
- Nipkow, T. (2002). Hoare Logics in Isabelle/HOL. Proof and System-Reliability, 341–367. https://doi.org/10.1007/978-94-010-0413-8_11
- Nipkow, T. (2002). Hoare Logics for Recursive Procedures and Unbounded Nondeterminism. Computer Science Logic, 103–119. https://doi.org/10.1007/3-540-45793-3_8
- author's copy
- author's copy