A formalized proof system for total correctness of while programs

Abstract

We introduce datatype specifications based on schemes, a slight generalization of first order specifications. For a schematic specification (Σ, $\mathbb{E}$), Hoare's Logic HL (Σ, $\mathbb{E}$) for partial correctness is defined as usual and on top of it a proof system (Σ, $\mathbb{E}$) ⊢ p → S ↓ for termination assertions is defined. The system is first order in nature, but we prove it sound and complete w.r.t. a second order semantics. We provide a translation of a standard proof system HL_T(A) for total correctness on a structure A into our format.