Hoares logic is an axiomatic system of proving programs correct, which has been extended to be a separation logic to reason about mutable heap structure. We develop the most fundamental logical structure of strongest postcondition of Hoares logic in Peanos arithmetic $PA$. Let $pin L$ and $S$ be any while-program. The arithmetical definability of $textbf{N}$-computable function $f_S^{textbf{N}}$ leads to separate $S$ from $SP(p,S)$, which defines the strongest postcondition of $p$ and $S$ over $textbf{N}$, achieving an equivalent but more meaningful form in $PA$. From the reduction of Hoares logic to PA, together with well-defined underlying semantics, it follows that Hoares logic is sound and complete relative to the theory of $PA$, which is different from the relative completeness in the sense of Cook. Finally, we discuss two ways to extend computability from the standard structure to nonstandard models of $PA$.
تحميل البحث