Partial correctness: The term-wise approach (Q793507)

The first reason to consider the correctness of programs with respect to terms rather than predicates is a simple observation that the classical Hoare's logic, although complete, is too weak to specify programs. Even if we know that a command c is correct w.r.t. predicates \(n\geq 0\) and \(x=n!\) we still cannot claim that c computes factorials since c might update n instead (e.g. c might be: \(n:=0\); \(x:=1)\). A way out put forward in the paper is to allow \(\{t_ 1\}c\{t_ 2\}\) where \(t_ 1\) and \(t_ 2\) are terms, to mean the value of \(t_ 2\) after execution of c is, if defined, equal to the value of \(t_ 1\) before. Now \(\{\) n!\(\}\) \(c\{\) \(x\}\) means that c assigns to x the factorial of the initial value of n. The actual calculus of the term-wise correctness turns out very close to the classical Hoare's logic with the backward substitution (in terms) and the loop invariants (terms as well). The generalization onto procedures and functions is easier than is the case with the Hoare's logic. The paper gives the inference system which is sound and relatively complete.