444 We want to find the smallest number in 0,..n with property p . Linear search solves the problem. But evaluating p is expensive; let us say it takes time 1 , and all else is free. The fastest solution is to evaluate p on all n numbers concurrently, and then find the smallest number that has the property. Write a program without concurrency for which the sequential to parallel transformation gives the desired computation.
§ We introduce array A: [n*bin] . We define the desired result R , condition I i , and helper specification P as follows.
R = ¬(∃j: 0,..hʹ· pj) ∧ (phʹ ∨ hʹ=n) I i = ∀j: 0,..i· Aj=pj
P = I n ∧ ¬(∃j: 0,..h· pj) ⇒ R
Now the program is
R ⇐ I0⇒Iʹn. h:= 0. P
I0⇒Iʹn ⇐ for i:= 0;..n do Ii⇒Iʹ(i+1) od
Ii⇒Iʹ(i+1) ⇐ Ai:= pi
P ⇐ ifh=nthenokelseifAhthenokelseh:=h+1. Pfifi
The n iterations of the for-loop can be executed in parallel.
We can express the result of the sequential to parallel transformation at source as follows.
R ⇐ I0⇒Iʹn. h:= 0. P
I0⇒Iʹn ⇐ i:= 0. Ii⇒Iʹn
Ii⇒Iʹn ⇐ if i=n then ok else Ai:= pi || (i:= i+1. Ii⇒Iʹn) fi P ⇐ ifh=nthenokelseifAhthenokelseh:=h+1. Pfifi
To understand the execution, it might help to unroll the recursion a little: in the refinement of Ii⇒Iʹn , replace the recursive call Ii⇒Iʹn by what’s called if i=n then ok else Ai:= pi || (i:= i+1. Ii⇒Iʹn) fi . And maybe do the same once more.