Concurrent Search Program

PROGRAM VERIFICATION

Handout #4

Let f: Z->Z be a function with at least one zero. The following program is intended to search the positive integers and negative integers in parallel until a zero is found.

S is [S1||S2] where

S1:
found := false
x := 0
while not found do
    x := x+1
    found := (f(x) = 0)
S2:
found := false
y := 1
while not found do
    y := y-1
    found := (f(y) = 0)