Główna zawartość

Kurs: Podstawy informatyki - program rozszerzony > Rozdział 4

Lekcja 2: Ocena złożoności algorytmów

Weryfikacja algorytmu

Ważnym aspektem każdego algorytmu jest to, że jest poprawny : zawsze wytwarza oczekiwany wynik dla zakresu danych wejściowych i ostatecznie się kończy.

Jak się okazuje, trudno udowodnić, że algorytm jest poprawny. Programiści często używają analizy empirycznej do znajdowania błędów w algorytmie, ale tylko formalne rozumowanie może udowodnić całkowitą poprawność.

Analiza empiryczna

Analiza „empiryczna” opiera się na faktycznych eksperymentach i obserwacji wyników. W świecie algorytmów oznacza to, że algorytm musi zostać faktycznie przetłumaczony na język programowania i wykonany na komputerze.

Przeprowadźmy analizę empiryczną algorytmu, który znajdzie maksymalną wartość na liście liczb.

Oto pseudokod, który wyraża ten algorytm:

maxNum ← -1
FOR num IN numbers {
  if (num > maxNum) {
    maxNum ← num
  }
}

Następnie przetłumaczymy to na język JavaScript, ponieważ możemy to wykonać w naszym interaktywnym edytorze tutaj w Khan Academy.

var maxNum = -1;
for (var i = 0; i < numbers.length; i++) { 
  if (numbers[i] > maxNum) {
    maxNum = numbers[i];
  }
}

Następnie musimy wprowadzić dane wejściowe do algorytmu i obserwować jego działanie. W naszym pierwszym eksperymencie, dajmy mu szereg 4 liczb, [13, 4, 24, 7] i zobaczmy, czy daje wynik 24,

Super, zadziałało! Czy możemy zadeklarować, że jest to całkowicie poprawny algorytm i iść dalej? Obawiam się, że to nie jest takie łatwe ...

Czas na eksperyment nr 2. Tym razem zróbmy wszystkie liczby w szeregu ujemne, [-13, -4, -24, -7]. Tym razem maksymalna wartość powinna wynosić -4, najmniejsza liczba ujemna na liście.

O nie, kod wypisał -1 zamiast -4. Jest tak, ponieważ początkowa wartość dla maxNum wynosi -1, a pętla nigdy nie znajduje wartości na liście większej niż ta. Nasz algorytm zdecydowanie nie działa poprawnie dla liczb ujemnych.

W tym momencie musimy zmodyfikować nasz algorytm i przeprowadzić analizę empiryczną na (miejmy nadzieję) ulepszonym algorytmie. Wypróbujmy wersję algorytmu, która inicjuje maxNum do pierwszej liczby na liście:

To działa! A przynajmniej działa na liście liczb ujemnych. Czy nadal działa na liście liczb dodatnich? Co z mieszaną listą liczb dodatnich i ujemnych? Co z ułamkami? Czy liczby nieracjonalne? Jest tak wiele możliwości przetestowania!

Testy możemy wykonać łatwiej, zawijając nasz algorytm w procedurze i używając biblioteki testowej do potwierdzenia, że wyniki procedur są zgodne z oczekiwaniami. W Khan Academy Program.assertEqual (rzeczywisty, oczekiwany) jest prostą procedurą testową, która wyświetla błąd, ilekroć rzeczywista wydajność nie jest równa oczekiwanej.

Oto analiza empiryczna czterech różnych list:

Brak błędów! Nowy algorytm wygląda bardziej poprawnie niż stary. Ale czy to naprawdę prawda? Nie wiemy tego na pewno. W rzeczywistości moglibyśmy przeprowadzić o wiele więcej eksperymentów i nadal nie będziemy wiedzieć.

Analizy empirycznej można użyć tylko w celu udowodnienia, że zaimplementowany algorytm nie jest poprawny, poprzez wykrycie danych wejściowych, w których dane wyjściowe są nieoczekiwane. Nie może jednak udowodnić, że algorytm jest poprawny.

Formalne uzasadnienie

Jedynym sposobem udowodnienia poprawności algorytmu we wszystkich możliwych danych wejściowych jest formalne lub matematyczne uzasadnienie.

Jedną z form rozumowania jest „dowód indukcyjny”, technika stosowana również przez matematyków w celu udowodnienia właściwości sekwencji numerycznych.

📝 Wskazówka do egzaminu : Egzamin AP CSP nie wymaga zrozumienia, jak udowodnić algorytmy przez indukcję. Przechodzimy tutaj, aby poczuć, jak mogłoby wyglądać formalne rozumowanie, ale AP nie oczekuje, że uczniowie zrozumieją ten zaawansowany poziom rozumowania matematycznego.

Metafora może pomóc w zrozumieniu indukcji. Wyobraź sobie, że mamy linię miliona kostek domino, które są idealnie rozmieszczone. Skąd wiemy, że każde domino upadnie gdy przewrócimy pierwsze? W rzeczywistości nie musimy sprawdzać każdą kostkę domina. Musimy tylko udowodnić, że 1) pierwsze domino upadnie, i 2) przechylenie się dowolnej kostki domino spowoduje przewrócenie następnego domina. Po udowodnieniu tylko tych dwóch rzeczy, milion kostek domino przewróci się!

Teraz zastosujmy indukcję do algorytmu. Oto pseudokod algorytmu obliczającego silnię dodatniej liczby całkowitej:

PROCEDURE calcFactorial(n) {
    factorial ← 1
    i ← 1
    REPEAT UNTIL (i > n) {
        factorial ← factorial * i
        i ← i + 1
    }
    RETURN factorial
}

Silnia liczby jest iloczynem tej liczby ze wszystkimi liczbami mniejszymi od niej, aż do 1. Na przykład silnia

4

, często zapisywana jako 4

!

, Wynosi

4 \times 3 \times 2 \times 1 = 24

Zanim udowodnimy, że ten algorytm z powodzeniem oblicza

n!

, wypróbujmy go dla

n

równego

4

. Jeśli algorytm jest poprawny, powinien zwrócić

24

Zmienne factorial i i zaczynają się od 1.
Ponieważ i (1) nie jest większe niż n (4), wchodzimy do pętli.
Iteracja nr 1: factorial jest ustawiony na 1 (bo 1 * 1), a i wzrasta do 2.
Iteracja nr 2: factorial jest ustawiony na 2 (bo 1 * 2), a i wzrasta do 3.
Iteracja nr 3: factorial jest ustawiony na 6 (bo 2 * 3), a i wzrasta do 4.
Iteracja nr 4: factorial jest ustawiony na 24 (bo 6 * 4), a i wzrasta do 5.
W tym momencie i (5) jest większe niż n (4), więc kończymy pętlę.
Procedura zwraca wartość 24.

Świetnie, sprawdziliśmy, że algorytm oblicza poprawny wynik dla pojedynczej liczby całkowitej.

Udowodnijmy teraz, że dla wszystkich liczb całkowitych dodatnich algorytm oblicza silnię z danej liczby.

Po pierwsze, musimy udowodnić, że algorytm ostatecznie się zakończy, ponieważ nie można uznać za poprawny algorytm, który działa w nieskończoność. W tym algorytmie i zaczyna się od 1 i rośnie o 1, aż osiągnie wartość n + 1. Tak więc algorytm zawsze zatrzymuje się po n powtórzeniach pętli.

Następnie, aby udowodnić, że ten algorytm wylicza silnię, udowodnimy "niezmiennik pętli", czyli własność pętli, która zawsze powinna być prawdziwa. W tym algorytmie, po przejściu przez pętlę n razy, factorial powinien być równy n!, a i powinno być równe n + 1. Tak było w naszym przykładzie z factorial(4), a teraz spróbujemy udowodnić, że jest to prawda dla każdej dodatniej liczby całkowitej.

Wymaga to udowodnienia 1) przypadku bazowego oraz 2) hipotezy indukcyjnej.

Przypadek bazowy: W tym miejscu sprawdzamy, czy algorytm działa dla pierwszej liczby z zakresu możliwych danych wejściowych.

W przypadku tego algorytmu, sprawdzamy go dla wszystkich liczb całkowitych dodatnich, więc przypadek bazowy jest wtedy, gdy n wynosi 1. Zgodnie z naszym niezmiennikiem pętli, po przejściu przez pętlę 1 raz, factorial powinien być równy 1! (1), a i powinno być równe 1 + 1 (2).

Możemy prześledzić nasz algorytm dla calcFactorial(1), podobnie jak to zrobiliśmy dla liczby 4:

Zmienne factorial i i zaczynają się od 1.
Ponieważ i (1) nie jest większe niż n (1), algorytm wchodzi w pętlę.
Iteracja nr 1: factorial jest ustawiony na 1 (bo 1 * 1) a i wzrasta do 2.
W tym momencie i (2) jest większe niż n (1), więc algorytm wychodzi z pętli.

Nasz niezmiennik pętli zawiera: factorial przechowuje 1, a i przechowuje 2.

Skoro przypadek bazowy został udowodniony, przejdźmy dalej!

Krok indukcyjny: W tym kroku pokazujemy, że jeśli to działa dla dowolnej liczby, to działa również dla kolejnej liczby po niej.

Zaczynamy od hipotezy indukcyjnej: założenia, że niezmiennik pętli jest prawdziwy dla pewnej dodatniej liczby całkowitej k. Po przejściu przez pętlę k razy, factorial powinien być równy k!, a i powinno być równe k + 1.

Wychodząc z tego założenia, udowodnimy, że niezmiennik pętli jest prawdziwy także dla k + 1, liczby zaraz po k. Po przejściu przez pętlę k + 1 razy, factorial powinien być równy (k + 1)!, a i powinno być równe (k + 1) + 1.

Aby to zrobić, przejdźmy przez calcFactorial(k + 1). Możemy szybko przejść przez pierwsze k powtórzeń, dzięki naszej hipotezie indukcyjnej.

Po k powtórzeniach, factorial przechowuje k! a i przechowuje k + 1.
Iteracja nr k+1: factorial jest ustawiony na k! * (k + 1) a i wzrasta do k + 2.
W tym momencie i (którego wartością jest k + 2) jest większe niż n (którego wartością jest k + 1), więc algorytm wychodzi z pętli.

Czy niezmiennik pętli był prawdziwy? Tak! Zmienna factorial przechowuje k! * (k + 1), co jest równoważne (k + 1)!, a zmienna i przechowuje k + 2, co jest równoważne (k + 1) + 1.

Możemy śmiało stwierdzić, że niezmiennik pętli jest prawdziwy dla wszystkich dodatnich liczb całkowitych k.

Ponieważ wykazaliśmy wcześniej, że pętla zatrzymuje się po n powtórzeniach, zatem calcFactorial(n) zawsze zwraca n!. Nasz algorytm jest poprawny, ponieważ zarówno kończy działanie, jak i daje poprawną odpowiedź, gdy kończy działanie.

Dowód przez indukcję to technika, która sprawdza się w przypadku algorytmów zapętlających się na liczbach całkowitych i pozwala udowodnić, że algorytm zawsze daje poprawne dane wyjściowe. Inne rodzaje dowodów mogą weryfikować poprawność dla innych typów algorytmów, np. dowód przez sprzeczność lub dowód przez wyczerpanie.

Ten poziom rozumowania formalnego ma niewątpliwe wady: po pierwsze, większość programistów komputerowych nie ma przygotowania matematycznego do weryfikacji za pomocą dowodów, a po drugie, dowód jest przeprowadzany poza kodem, więc implementacja algorytmu może odbiegać od udowodnionej wersji algorytmu.

Najpopularniejszą formalną techniką pisania poprawnego kodu jest używanie języków programowania stworzonych specjalnie z myślą o sprawdzalności. Firmy działające w chmurze obliczeniowej, takie jak Amazon czy Microsoft, używają języków weryfikowalnych dla swojej infrastruktury krytycznej, ponieważ nie mogą sobie pozwolić na awarię z powodu błędu w ich algorytmach.

Realnie rzecz biorąc, większość oprogramowania jest weryfikowana za pomocą analizy empirycznej. Wynika to częściowo z faktu, że większości programistów brakuje teoretycznego przygotowania do udowadniania poprawności algorytmów. Ale wynika to także z łatwości, z jaką można przeprowadzić analizę empiryczną, oraz z faktu, że dobrze przemyślany zestaw testów może udowodnić, że algorytm jest prawie na pewno poprawny - i to często wystarcza.

🙋🏽🙋🏻‍♀️🙋🏿‍♂️Czy masz jakieś pytania na ten temat? Chętnie na nie odpowiemy — wystarczy, że zadasz pytanie w poniższym obszarze pytań!

Chcesz dołączyć do dyskusji?

Zaloguj się

Sortuj według

Na razie brak głosów w dyskusji

Rozumiesz angielski? Kliknij tutaj, aby zobaczyć więcej dyskusji na angielskiej wersji strony Khan Academy.