Proof rules for partial correctness

To prove partial correctness for programs with synchronization, it is enough to deal with the additional await construct.

If B is , then the rule simply transforms into the rule for atomic regions. Proof outlines are generated with the rules applied for parallel programs with shared variables together with the rule for synchronization:

where, as usual, is some proof outline obtained from S. A proof outline is standard as usual, in this case a subprogram is normal if it is not within an await statement. There are no assertions within await statements. Interference freedom (partial correctness with synchronization) is understood as no normal assignment or await statement interferes with the proof outline of another parallel component. The proof system is formulated now, in the form of a proof outline, by the usual rules for proof outlines for while programs together with , and and is added for the parallel components. We state a soundness theorem.

Theorem 129. The proof system is sound, that is, for a fixed interpretation , if the standard proof outline is inferred, then holds, as well.

As an example we prove the following partial correctness assertion.

Example 130. Let . Let us verify

done;

while done do [await X=0 then done:=true end X:=X-1] od

.

To this end, we provide the proofs of the parallel components first, in the forms of proof outlines. As an invariant, we choose . First of all, we prove

await X=0 do

done:=true

end

and

X:=X-1

We have to check interference freedom. We confine ourselves to standard proof outlines in order to have fewer assertions to take into account. Thus, there are no assertions within atomic regions. Hence, for example,

X:=X-1

or

await X=0 do

done:=true

end

Combining all these together, rule yields

thus

From this the partial correctness assertion follows.