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.
As an example we prove the following partial correctness assertion.
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
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,
await X=0 do
Combining all these together, rule yields
From this the partial correctness assertion follows.