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.

 

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2009: afp-Abstract-Hoare-Logics-2009-04-29.tar.gz Isabelle 2008: afp-Abstract-Hoare-Logics-2008-06-10.tar.gz Isabelle 2007: afp-Abstract-Hoare-Logics-2007-11-27.tar.gz