Recursive assertions and parallel programs

Summary We prove that recursive assertions are enough for proofs of parallel programs considered in Owicki and Gries 7]. In other words, we prove that for any parallel program S and recursive assertions p and q if {p} S{q} is true under the standard interpretation in natural numbers then all intermediate assertions needed in the proof can be chosen recursive. Finally, we show that if auxiliary variables are used only as program counters then the above result does not hold.