Linear Search with Break

DATE : September 2001
AUTHOR : underdarkPrime and Ade
ADDRESS : underdarkPrime@yahoo.com and ade@cs.uu.nl

Index



This program is a smarter version of linear search. The program tests whether the array contains 0. It stops as soon as it finds a 0 (where the 'naive' of linear search would here simply continue till the end of the array).
{= 0<=N =}



{

n=0 							;	 

b=F  							;



inv 

	(! i: 0<=i /\ i < n : ~(a#i=0))

	/\

	0<=n

	/\

	n<=N

	/\

	(b ==> (a#n=0))

	/\

	(b ==> n < N)



while (~b /\ ~(n=N))

      if (a#n=0)  

		b=T 

		else n=n+1			;

}



{= b = (? i: 0<=i /\ i < N : a#i=0) =}


Generated by mosmldoc --underdarkPrime