The wp-calculus

We turn to the brief discussion of the termination conditions on while programs, prior to this we introduce a notion very similar to that used in the proof of the completeness of the partial correctness calculus. The function called the weakest precondition of with respect to is defined as follows.

Definition 51.

The wp-calculus has very similar properties to the wlp-calculus. In this section we gather some of them, and we return to the wp-calculus in relation to the question of relative completeness in later section. The following properties hold true, which show a great resemblance to the case of the wlp-calculus.

Lemma 52.

Proof. The proofs for , assignment, conditional statement and composition is similar to that of Lemma 46. We treat only the case of the while loop.

  1. Assume . Then and . By Lemma 21, there exists such that and . This means exactly and, hence, .

  2. Let . This means and . Again, by Lemma 21, and entails , which gives the result.

By an argument similar to that of Lemma 48 one can prove a statement for the iterative computation of the weakest precondition for a while loop. Observe that in this case we do not need the assumption any more. Without proof, we assert the statement for the wp-calculus mutatis mutandis.

Lemma 53. Let be a program, let Q denote a set of states. Then can be computed iteratively as the union of the following sets of states.

Then

We illustrate by an example below how to compute the weakest precondition of the while loop with the help of Lemma 53.

Example 54. Compute .

In general, we can prove by induction on i that , if i is positive. Thus, can be chosen as the weakest precondition.