PROGRAM VERIFICATION

Handout #9: Disjoint Find

 
 

This is a program that finds the location k of the first positive element (a[k]>0) in an array a[1:N] and returns N+1 if there is none such.
 
 

{N > 0}

i1 := 1
i2 := 2
k1 := N+1
k2 := N+1

{N > 0, i1=1, i2=2, k1=N+1, k2=N+1}
{N > 0, i1=1, k1=N+1}

S1: while {1 < k1 < N+1,
             odd(i1), 1 < i1 < k1+1,
             a[1,3,...,i1-2] < 0, 
             k1<N => a[k1]>0}
             i1 < k1 do
       if a[i] > 0
          then k1 := i1
          else i1 := i1+2

{1 < k1 < N+1, odd(i1), 1 < i1 < k1+1,
a[1,3,...,i1-2] < 0, k1<N => a[k1]>0, k1 < i1}
{N > 0, i2=2, k2=N+1}

S2: while {1 < k2 < N+1,
             even(i2), 1 < i2 < k2+1,
             a[2,4,...,i2-2] < 0, 
             k2<N => a[k2]>0}
            i2 < k2 do
       if a[i2] > 0 
            then k2 := i2
            else i2 := i2+2

{1 < k2 < N+1, even(i2), 1 < i2 < k2+1,
a[2,4,...,i2-2] < 0, k2<N => a[k2]>0, k2 < i2}
{1 < k1, k2< N+1, odd(i1), even(i2), k1 < i1 < k1+1, k2< i2 < k2+1,
 a[1,2,...,min(i1,i2)-2] < 0, k1<N => a[k1]>0, k2<N => a[k2]>0}

k := min(k1,k2)

{1 < k <N+1, a[1:k-1] <0, k<N => a[k]>0}