# Abstract Hoare Logics

 Title: Abstract Hoare Logics Author: Tobias Nipkow Submission date: 2006-08-08 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. BibTeX: @article{Abstract-Hoare-Logics-AFP, author = {Tobias Nipkow}, title = {Abstract Hoare Logics}, journal = {Archive of Formal Proofs}, month = aug, year = 2006, note = {\url{https://isa-afp.org/entries/Abstract-Hoare-Logics.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.