W jaki sposób uzyskuje się niezmiennik pętli w tym algorytmie znajdowania pierwiastka kwadratowego?

Oryginalnie na math.SE, ale bez odpowiedzi.

Rozważ następujący algorytm.

u := 0
v := n+1;
while ( (u + 1) is not equal to v) do
   x :=  (u + v) / 2;
   if ( x * x <= n) 
     u := x;
   else
     v := x;
   end_if
end_while 

gdzie u, v i n są liczbami całkowitymi, a operacja dzielenia jest dzieleniem liczb całkowitych.

• Wyjaśnij, co jest obliczane przez algorytm.
• Wykorzystując swoją odpowiedź do części I jako warunek końcowy algorytmu, ustal niezmiennik pętli i pokaż, że algorytm kończy się i jest poprawny.

W klasie stwierdzono, że warunek to a niezmiennikiem jest . Naprawdę nie rozumiem, w jaki sposób uzyskano warunek końcowy i niezmienniki. Sądzę, że warunek postu to u + 1 = v ... co oczywiście nie jest prawdą. Zastanawiam się więc, w jaki sposób uzyskano warunek końcowy i niezmiennik. Zastanawiam się także, w jaki sposób można uzyskać warunek wstępny za pomocą warunku końcowego.$0 \leq u^2 \leq n < (u + 1)^2$$0 \leq u^2 \leq n < v^2, u + 1 \leq v$$u + 1 = v$

Gilles ma rację, że ogólną techniką jest poszukiwanie ciekawych obserwacji.

W takim przypadku możesz zauważyć, że program jest instancją wyszukiwania binarnego, ponieważ ma następujący kształt:

while i + 1 != k
  j := strictly_between(i, k)
  if f(j) <= X then i := j
  if f(j) > X then k := j

Następnie wystarczy podłączyć w danym f, X... do ogólnego niezmiennika dla wyszukiwania binarnego. Dijkstra ma niezłą dyskusję na temat wyszukiwania binarnego .

$u+1=v$ jest rzeczywiście warunkiem końcowym pętli while (dlaczego według ciebie nie jest tak „tak”?). Dzieje się tak zawsze w przypadku pętli while, która nie zawiera break: gdy pętla kończy działanie, może być tak tylko dlatego, że warunek pętli (tutaj, ) jest fałszywy. To nie jedyna rzecz, która będzie prawdą, gdy pętla zostanie zamknięta tutaj (ten algorytm oblicza coś interesującego, jak widzieliście w klasie, więc i są również warunkami wstępnymi), ale jest to najbardziej oczywiste.$u+1 \neq v$$u = \text{[this interesting thing]}$$v = \text{[this interesting thing]}$

Teraz, aby znaleźć inne interesujące właściwości, nie ma ogólnej recepty. W rzeczywistości istnieje formalny sens, w którym nie ma ogólnej recepty na znalezienie niezmienników pętli. Najlepsze, co możesz zrobić, to zastosować techniki, które działają tylko w niektórych przypadkach, lub ogólnie wybrać się na ciekawe obserwacje (które działają coraz lepiej, gdy zdobędziesz więcej doświadczenia).

Jeśli uruchomisz pętlę dla kilku iteracji z pewną wartością , zobaczysz to przy każdej iteracji:$n$

• albo skacze do ;$u$$(u+v)/2$
• lub przeskakuje do .$v$$(u+v)/2$

W szczególności mniej niż i nigdy go nie wyprzedzisz. Ponadto zaczyna się od dodatniej i wzrasta, podczas gdy zaczyna się od i maleje. Więc jest niezmiennikiem w całym programie.$u$$v$$u$$v$$n+1$$0 \le u \le v \le n+1$

Jedną rzeczą, która nie jest tak oczywiste, czy może kiedykolwiek być równa . To ważne: jeśli i kiedykolwiek staną się równe, otrzymamy a pętla będzie działać wiecznie. Musisz więc udowodnić, że i nigdy nie stają się równe, aby udowodnić, że algorytm jest poprawny (tj. Nie zapętla się na zawsze). Po zidentyfikowaniu tej potrzeby łatwo jest udowodnić (pozostawiam to jako ćwiczenie), że jest niezmiennikiem pętli (pamiętaj, że i są liczbami całkowitymi, więc jest to równoważne ).$u$$v$$u$$v$$x = u = v$$u$$v$$u < v$$u$$v$$u+1 \le v$

Ponieważ na końcu programu, podany warunek końcowy można również zapisać (część jest trywialna). Powodem, dla którego chcemy takiego warunku końcowego, obejmującego , jest to, że chcemy powiązać wynik programu z wejściem . Skąd ten precyzyjny warunek? Szukamy czegoś tak precyzyjnego, jak to możliwe, i patrzymy, gdzie pojawia się w pętli:$v = u+1$$u^2 \le n < v^2$$0 \le u^2$$n$$n$$n$

• mamy ;$u \le x \le v$
• kiedy , wybieramy następny jako , aby (i się nie zmienia);$x^2 \le n$$u$$x$$u^2 \le n$$v$
• gdy , wybieramy następne jako , aby ( się nie zmienia).v x n < v 2$x^2 > n$$v$$x$$n < v^2$$u$

Ta dychotomia sugeruje, że być może cały czas . Innymi słowy, podejrzewamy, że jest to niezmienna pętla. Sprawdzanie tego pozostawia się czytelnikowi jako ćwiczenie (pamiętaj, aby początkowo sprawdzić, czy właściwość jest prawdziwa).$u^2 \le n < v^2$

A teraz, kiedy to wszystko zrobiliśmy, widzimy, że i : jest pierwiastkiem kwadratowym z zaokrąglonym w dół do najbliższej liczby całkowitej.( u + 1 ) 2 > n u $u^2 \le n$$(u+1)^2 > n$$u$$n$