Binary Search code.

1.	What is the running time of this algorithm?  How could you prove it?
2.	Is this program correct?  How could you prove it?



struct HammondAndIndexCodes {
	int hamCode; // the integer ID code from Hammond, Inc.
	int arrayIndex; // offset into array
};

int numHammondCodes; // # of different codes there are

HammondAndIndexCodes codesArray[1000]; // array of (Hammond code, array 
index), sorted by hamCode.


int HammondCodeToArrayIndex (int hamCode)
{
	// Function PRECONDITIONS:
	// codesArray has all the corresponding codes
//	and is sorted by the Hammond code (hamCode)
	// numHammondCodes is the size of the array

	// Function POSTCONDITIONS:
	// if hamCode is valid, returns the arrayIndex code
	// if hamCode is not valid, 
//	prints an error, and aborts the program

	int startCursor,endCursor; // where it could be
	startCursor=0;
	endCursor=numHammondCodes;

	// Loop INVARIANT
	// startCursor is the smallest element that hamCode could be
	// endCursor is one past the biggest element that hamCode
	//	could be
	// ? hamCode will be in 
// (startCursor, startCursor+1, startCursor+2,... , endCursor-1)
	while (startCursor+1!=endCursor) {

		int testCursor;

		// testCursor is mid-point
		testCursor=(startCursor+endCursor)/2; 
// remember: 5/2=2 in integer math

		if (codesArray[testCursor].hamCode == hamCode) {
			// found it exactly
			// cheat it to the correct loop postcondition
			startCursor=testCursor; 
			break; // exit loop
		}
		if (codesArray[testCursor].hamCode < hamCode)
			startCursor=testCursor;
		else
			endCursor=testCursor;
	}
	// Loop POSTCONDITION
	// startCursor is at hamCode, or hamCode does not exist
	if (codesArray[startCursor].hamCode == hamCode) {
		return codesArray [startCursor].arrayIndex;
	}
	else {
		printf("ERROR: reference to invalid Hammond code\n");
		abort();
	}
}