A note on predicate transformers and loop invariants

For standard programs, the computational model of execution supports a "logical" view—given a set of final states, we can examine the program to determine the largest set of initial states from which execution of the program is guaranteed to reach the final states. The sets of states are characterized by logical formula called predicates, and the program is being regarded as a predicate transformer, i.e., a total function that maps one predicate to another. We give some important terminology before we proceed:

• An assertion is a predicate placed in a program to assert that it holds at that point
• A precondition is an assertion placed before a program segment
• A postcondition is an assertion placed after a program segment
• A formula in form $\{precond\} \; program \; \{postcond\}$ is called a Hoare triple
• A Hoare triple is valid iff whenever the precondition holds, the postcondition holds after the execution of the program segment terminates
• A loop invariant is an assertion supposed to be true before and after each iteration of a loop

The following example puts all ingredients together:

// Precondition: (x=0 and y=0 and n≥0)
while (y<n) { 
    // Loop invariant: 2*x = y*(y-1)
    x+=y; y++; 
}
// Postcondition: 2*x = n*(n-1)

Observe that $\{x=0 \wedge y=0 \wedge n\ge0\}$ while(y<n){x+=y;y++;} $\{2x=n(n-1)\}$ is a valid Hoare triple and $2x = y(y-1)$ is an invariant for the while loop.

Predicate transformer semantics provide an effective algorithm to verify a Hoare triple by reducing the verification problem to the problem of proving logical entailment: Given a Hoare triple $\{pre\} \; prog \; \{post\}$, we first compute the weakest precondition of executing $prog$ starting from $post$, and then check that it entails $pre$. This amounts to proving that $$pre \Rightarrow wp(prog, post).$$When $prog$ doesn't contain a loop, the weakest precondition is simply given by syntactic rules. However, the presence of loops may pose a problem because the precondition is given in terms of a least fixed point. Besides, a separate proof is required to establish that the loops terminate from their initial state. Formally, if $G$ is a predicate and $body$ is a loop-free program segment, then \begin{equation} wp({\rm while}(G)\{body\}, post) = \mu X.((G\Rightarrow wp(body, X)) \wedge (\neg G\Rightarrow post)),\label{loop-wp} \end{equation} where $\mu$ is the least fixed point operator w.r.t. logic implication. Given that the loop terminates and the least fixed point exists, the construction of the weakest precondition can be sketched in set theory as follows. Let $\Sigma$ denote the state space. We define a family $\{A_k:k\ge0\}$ of subsets of $\Sigma$ by induction over $k$: \begin{array}{rcl} A_0 & = & \emptyset \\ A_{k+1} & = & \left\{\ y \in \Sigma: ((G \Rightarrow wp(body, x \in A_k)) \wedge (\neg G \Rightarrow post))[x \leftarrow y]\ \right\} \\ \end{array} Informally, $A_k$ represents the set of initial states that makes the postcondition $post$ satisfied after less than $k$ iterations of the loop. We can then define the weakest precondition in \eqref{loop-wp} as a first-order predicate $\exists k. x \in A_k$.

While an abstract construction as above is elegant, it can not be handled efficiently by theorem provers in practice. Fortunately, using special assertions called loop invariants we may by and large avoid the need of calculating fixed points. Suppose that we want to verify \begin{equation} pre \Rightarrow wp({\rm while} (G) \{body\}, post).\label{loop-hoare} \end{equation} Instead of calculating the least fixed point of the loop directly, we may divide the problem into simpler subtasks:

1. Find an assertion $I$ such that $pre \Rightarrow I$ and $I\wedge\neg G \Rightarrow post$.
2. Show that $I$ is an invariant: $I\wedge G \Rightarrow wp(body, I)$.
3. Show that $I$ is sound: $I \Rightarrow wp({\rm while}(G)\{body\}, I\wedge\neg G)$.

The first task ensures that the existence of $I$ establishes the desired relation between $pre$ and $post$. The second task considers a single iteration of the loop body and ensures that the execution of the loop preserves the validity of $I$. Note that it is easy to compute $wp(body, I)$ because $body$ is loop-free by assumption. In the third task, we check the soundness property such that every execution of the loop from a state satisfying the invariant can only terminate in a state that also satisfies the invariant and violates the guard $G$. It is still an open problem in the literature to give a necessary and sufficient condition for the soundness. On the other hand, soundness property can be established if one can show, e.g., by using a loop variant, that the loop terminates when it started from a state satisfying $I$.

With invariant $I$, the relation between $pre$ and $post$ in \eqref{loop-hoare} is established as $$pre \Rightarrow I \Rightarrow wp({\rm while}(G)\{body\}, I\wedge\neg G)\quad {\rm and }\quad I\wedge\neg G \Rightarrow post.$$ Checking correctness for code without loops turns out be easy in practice. Hence, the crucial point in verifying a Hoare triple is to discover the necessary loop invariants for each loop in the program.

References

Gries, David. "The science of programming." Vol. 1981. Heidelberg: Springer, 1981.