Soundness and completeness

The proof system for the deduction of partial correctness formulas with shared variables was formulated in terms of proof outlines in the previous section. The change in comparison with the partial correctness calculus of while programs is the addition of three more rules: the atomic region rule, the auxiliary variable rule and the rule of parallelism with shared variables. Let us denote this proof system by . Since in the case of shared variable parallel programs compositionality is no more valid, that is, we are not able to compute the result of a program execution from the results obtained for its parallel components, it seems more reasonable to talk about the result of a program execution in the frames of the operational semantics. Thus

and

Here the symbol for divergence is not a member of . The sets of states forming a subset of are called proper. We know from Theorem 20, that the operational semantics and the denotational semantics convey the same meaning for while programs, so, in the case of while programs, this approach does not necessitate any changes in the statements of Chapter 1 made about soundness and completeness. With this new notation a partial correctness assertion is true if, for every ,

An analogue definition holds for total correctness: let , and be proper sets of states, that is , , then is true if, for every ,

Observe that the latter definition involves the non-divergence of , since is proper.

As before, let us fix an interpretation . Then the meaning of a partial correctness formula is understood as

which is true iff, for every s such that , is valid. If is known, we may simply write for . An analogous definition can be formulated to total correctness, too. Without proof we state the soundness of the deduction system.

Theorem 120. (Soundness of PSV) Let be a partial correctness formula for a parallel program with shared variables. Assume is a standard proof outline obtained form . Then holds true for the fixed interpretation .

As to the completeness, a relative completeness statement can be formulated again in this case. We state the claim for relative completeness, the proof of which can be found in ([2]).

Theorem 121. (Relative completeness of PSV) Let be the standard model of arithmetic. Let be the set of all true arithmetical statements. Assume S is a parallel program with shared variables. Let be the proof system defined as above. Then

Remark 122. (Total correctness) If we would like to prove total correctness assertions for while programs, the loop rule for the partial correctness proof system must be modified. However, it turns out that this kind of modification of our proof system does not yield a deduction system strong enough to prove the total correctness of parallel programs with shared variables. Instead, a stronger concept of termination is needed, since the various subprograms can interact with each other, hence, a loop in a computation sequence can emerge with the control switching to and fro between the otherwise terminating program components. We illustrate this phenomenon by an example taken from ([1]). Let be

while do;

;

if then

    else fi

od

and let be

while do;

;

if then

    else fi

od

Both programs possess a correct proof outline for total correctness with specifications , loop invariant and bound function . In addition these proof outlines are interference free, hence, by rule we would obtain

But the above sequence of configurations show that S can diverge. Let be such that . In what follows, we distinguish reduction steps coming from and by writing upper-indexes and , respectively. Let be the conditional statement in .

and the whole process starts all over again. This example shows that total correctness needs more precaution: the loop rule for the total correctness of while programs is not enough in this case. The new loop rule must ensure that every program execution reduces the value of the bound function. We do not elaborate the question any further here, the interested reader can find a detailed exposition in ([1]).