Case study

We illustrate the proof method described in this chapter by an example presented in ([1]). Before discussing the example, we deal with some additional results simplifying the proof to follow.

Theorem 123. (Atomicity) Let be a parallel program, where is a sequential one. Let be fixed. Let T be the program obtained from S either

  1. by replacing in an atomic region of the form by , where one of and is disjoint from every in the sense of Definition 92, or

  2. by replacing in an atomic region of the form by , where B is disjoint from every in the sense of Definition 92.

Then

and

Corollary 124. Let , be assertions, assume S and T are as in Theorem 123. Then

A similar result holds for total correctness, too.

Theorem 125. (Initialization) Let

be a parallel program, where , are sequential ones. Suppose there exists such that is disjoint from all . Let

Then

and

Corollary 126. Let , be assertions, assume S and T are as in Theorem 125. Then

A similar result holds for total correctness, too.

Now we can set to and demonstrate the applicability of our deduction system in a partial correctness proof.

Example 127. ([1]) Let us find the zeros of a number theoretic function f . The task is distributed between two components and : searches among the positive and among the negative arguments. Thus:

where

= X:=0;

while do

    X:=X+1;

    if then

        

    fi

od

and

= Y:=1;

while do

    Y:=Y-1;

    if then

        

    fi

od

We wish to verify the partial correctness formula

First we simplify the components by virtue of Theorems 125 and 123 making use of the observations that X does not occur in and does not occur in . Thus the new statement is

where = while do

     X:=X+1;

    if then

        

    fi

od

and

= while do

     Y:=Y-1;

    if then

        

    fi

od

Thus we need fewer statements to consider when verifying interference freedom. We choose the loop invariant for and for , respectively, where and are defined as follows.

We try to keep track of some of the steps of the proof. For the assertion we have to verify

X:=X+1;

if then

    

fi

By the assignment and the conditional rules for proof outlines we obtain

if then fi

.

Moreover, the assignment and composition rules together give

X:=X+1; if then fi

.

By the rule for atomic reg ions we can assert

X:=X+1; if then fi

.

What remains is to prove the validity of

Instead, we prove that the conclusion is a consequence of the premiss , which can be checked by using laws of first order logic. From this, by the consequence rule, the intended partial correctness assertion follows. In an analogous manner, we can demonstrate . To combine the two proof outlines, we have to check interference freedom. We may assume that the proof outlines in question are standard ones, that is, we may omit the subsequent assertions in the proof outlines leaving just one assertion in front of every normal subprogram of and . Thus, it is enough to consider the proof outlines

while do

    

     X:=X+1;

    if then

        

    fi

    

od

and

while do

    

     Y:=Y-1;

    if then

        

    fi

    

od

So, for example we have to check for the independence of X:=X+1; if then fi of the proof outline for . Hence, we have to check statements like

X:=X+1; if then fi .

They can be verified in a manner similar to the proof above. Having done all these steps, we can deduce, by the parallelism with shared variable rule,

But

hence the consequence rule yields the result. We remark that proving termination is impossible under these conditions, since there are scenarios when the program does not terminate. Assume, for example, if , and the execution of Search consists in a sequence of executions of the component . Then will never find a solution even if there is one, and the execution of the program will never terminate.