W tym punkcie omówimy algorytm rozwiązywania problemu wyszukiwania, który wykorzystuje w sposób bardzo istotny, założenie o uporządkowaniu danego ciągu. Dla uproszczenia założymy, że x należy do przedziału [e[1], e[n]]. Przyjmijmy specyfikację algorytmu

Metoda zastosowana w tym algorytmie nosi nazwę "dziel i zwyciężaj". W tym przypadku polega ona na znalezieniu zadania o mniejszym rozmiarze, którego rozwiązanie jest równocześnie rozwiązaniem zadania początkowego.

BinSearch{
	i := 1; j := n;
	while (i+1 < j) do	//e[i] £ x < e[j] oraz i<j
	m := (i + j) div 2;	// i < m < j
	if e(m) £ x then	// e[m] £ x < e[j]
	i := m	// e[i] £ x < e[j] oraz i<j
	else	// e[i] £ x < e[m]
	j := m	// e[i] £ x < e[j] oraz i<j
	fi
	od;	// i<j, e[i] £ x < e[j] oraz i+1=j
	result := i	// e[result] £ x < e[result+1]
}

Formuły zapisane obok instrukcji informują o własnościach prawdziwych w trakcie realizacji algorytmu. Wynika z nich, że niezmiennikiem pętli w tym algorytmie, jest formuła (e[i] £ x < e[j] Ù i < j).

Rzeczywiście, jeżeli formuła (e[i] £ x < e[j] Ù i < j) jest spełniona na początku kolejnej iteracji oraz spełniony jest warunek pętli, to po sprawdzeniu, po której stronie elementu środkowego e[m] znajduje się x oraz przesunięciu odpowiedniego końca przedziału znów mamy prawdziwą formułę (e[i] £ x < e[j]). Ponieważ i+1<j, to (i+j)/2<j, oraz i <(i+j)/2, czyli w obu przypadkach po wykonaniu przypisania i :=m lub j :=m, mamy i<j. Na mocy twierdzenia I.4.1 (o niezmiennikach), po wyjściu z pętli mamy i+1 ³ j oraz prawdziwy jest niezmiennik. Zatem (e[i] £ x < e[j] Ù i < j Ù i+1=j), czyli algorytm ustala wartość zmiennej result zgodnie z wymaganiami specyfikacji. Udowodniliśmy w ten sposób, że dla wszystkich danych spełniających warunek początkowy, jeżeli algorytm daje wynik, to spełnia on warunek końcowy w dowolnej strukturze danych z określonym liniowym porządkiem.

Twierdzenie 4.1

W każdej strukturze danych STR, w której określony jest z liniowy porządek £, algorytm BinSearch jest całkowicie poprawny ze względu na specyfikację

wp = {n > 1, e[1]< e[2]< ... < e[n], e[1] £ x < e[n]}, wk = { result £ n, e[result] £ x < e[result+1]}.

Dla dowodu twierdzenia 4.1 trzeba jeszcze pokazać, że algorytm BinSearch zatrzymuje się dla dowolnych danych spełniających warunek początkowy.

Zauważmy, że jeżeli różnica j - i pewnej iteracji wynosi c, to w następnej iteracji jest mniejsza od c, bo

Zatem ciąg różnic j - i wartości zmiennych i, j w kolejnych iteracjach pętli "While", jest ciągiem malejącym liczb naturalnych. Ponieważ nie można zbudować nieskończonego ciągu malejącego liczb naturalnych, zatem po skończonej liczbie kroków warunek j - i >1 nie będzie spełniony. Algorytm zakończy wtedy obliczenie. Wynika stąd, że algorytm BinSearch zatrzymuje się dla dowolnych danych, co kończy dowód twierdzenia 4.1.

Zastanówmy się najpierw czym będziemy mierzyć koszt czasowy tego algorytmu. Poza operacjami przypisania i operacjami arytmetycznymi, wykonuje się porównywanie elementów. Zauważmy, że dla tego algorytmu, nie jest istotne czym są elementy ciągu i jakie mają wartości. Ważne są tylko relacje między x, a elementami ciągu. Wydaje się więc naturalnym wybranie porównywania, jako operacji dominującej, przy pomocy której będziemy mierzyli koszt czasowy algorytmu. Zauważmy jeszcze, że niezależnie od wartości elementów, algorytm zawsze postępuje podobnie: w każdym kroku patrzymy, w której połowie rozważanego fragmentu ciągu, znajduje się x.

Pytanie o liczbą wykonanych operacji dominujących sprowadza się do pytania: ile iteracji wykona pętla "while". Ponieważ w każdej iteracji, segment, w którym mieści się x, jest dwa razy krótszy od rozważanego w poprzedniej iteracji, zatem pytanie sprowadza się do tego, ile razy ciąg o długości n można podzielić na 2 części. Ponieważ algorytm zatrzymuje się, gdy indeksy i, j są sąsiednimi liczbami naturalnymi, zatem w najgorszym razie wykona élg nù porównań.

Koszt czasowy algorytmu BinSearch jest logarytmiczny w stosunku do liczby elementów ciągu, T(BinSearch, n) = Q(lg n). Jest to więc istotna poprawa w porównaniu z algorytmami wyszukiwania przedstawionymi w poprzednich punktach tego wykładu.

Pytanie 4: Który z algorytmów wykona mniejszą liczbę porównań w przypadku najgorszym: algorytm Skoki z długością skoku równą éÖ(n-1) ù, czy algorytm poszukiwań binarnych?