// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // // This is the well-known binary search algorithm that expects a sorted array // // and a value whose membership in the array is to be checked. The algorithm // // starts looking at the entire array a[left..right] with left=0 and right=N-1// // and compares the middle element a[mid] with v. Since the array is sorted, // // the algorithm next proceeds inspecting either the lower half a[left..mid] // // or the upper half a[mid+1..right] of the array. // // It is well-known that most binary search algorithms are broken in that the // // computation of mid suffers from arithmetic overflows. This does not happen // // in Quartz since the arithmetic operations are performed in full precision. // // ************************************************************************** // macro N = 16; macro M = 62; macro sorted(a) = forall(i=0..N-2) (a[i] <= a[i+1]); macro contains(a,x) = exists(i=0..N-1) (a[i] == x); macro compare(a,b) = forall(i=0..N-1) (a[i] == b[i]); module Search_OlogN([N]int{M} ?a,int{M} ?v,nat{N} i,event !rdy) { nat{N} left,right,mid; assume(sorted(a)); left = 0; right = N-1; do { mid = (left+right)/2; if(v <= a[mid]) next(right) = mid; else next(left) = mid+1; pause; } while(left<right); i = left; emit(rdy); assert(contains(a,v) -> a[i] == v); } satisfies { termination : assert A F rdy; } drivenby { v = 2; for(i=0..N-1) a[i] = 2*i; await(rdy); }