POPRAWNOŚĆ PROGRAMÓW Gdzie można popełnić błąd?
Na poprawność programu komputerowego składa się: 1. Błędy składniowe
poprawność algorytmu,
Powstają w wyniku naruszenia reguł składni języka
poprawność zapisu w języku programowania.
programowania, którego używamy do zapisania algorytmu
Jeśli uważasz, że jakiś program komputerowy jest bezbłędny,
Np. zamiast for K := 1 to N do X[K] := K
to się mylisz  po prostu nie zauważyłeś jeszcze skutków
napisaliśmy for K := 1 to N to X[K] := K
błędu, który jest w nim zawarty.
:&
Możliwe skutki i znaczenie:
Na poprawność algorytmu składa się:
zatrzymanie kompilacji lub interpretacji z komunikatem lub bez,
poprawność logiczna (założenia, rozumowanie, metoda, ...)
przerwanie realizacji programu nawet jeśli kompilator błędu nie
poprawność algorytmiczna (struktura, sterowanie procesem, ...)
wykrył,
Na poprawność zapisu składa się:
błędy nieprzyjemne, ale zwykle niezbyt poważne
poprawność składniowa,
 są względnie łatwe do poprawienia.
poprawność semantyczna.
Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 1 Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 2
2. Błędy semantyczne
3. Błędy logiczne
Wynikają z niezrozumienia semantyki używanego
języka programowania
Mogą pochodzić z przyjęcia fałszywych założeń, wad
Np. sądziliśmy, że po zakończeniu instrukcji wykonania rozumowania lub z
le dobranej metody wyznaczania wyniku.
iteracji ograniczonej
for K := 1 to N do X[K] := K
Np. w algorytmie zliczania zdań zawierających słowo
zmienna K ma wartość równą zmiennej N, a nie N + 1,  algorytm nie zauważyliśmy, że sekwencja dwóch znaków
jak wynika z reguł semantycznych języka MJP,  .  może występować także wewnątrz zdania:
i wykorzystywaliśmy to w dalszej części programu
 Na Rys. 2 pokazano schemat... ,
Możliwe skutki i znaczenie:
a używaliśmy jej do wyszukiwania jego końca.
program nie realizuje poprawnie algorytmu,
błędy trudne do przewidzenia i potencjalnie groz
ne, ale są do
uniknięcia przy wnikliwym sprawdzaniu znaczenia używanych
instrukcji.
Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 3 Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 4
4. Błędy algorytmiczne
Możliwe skutki i znaczenie:
Wynikają z wadliwie skonstruowanych struktur sterujących
np. niewłaściwych zakresów iteracji, niewłaściwych warunków
algorytm przestaje być poprawnym rozwiązaniem zadania
użytych do zatrzymywania iteracji warunkowych lub
algorytmicznego,
przeniesienia sterowania w niewłaściwe miejsce procesu w
dla pewnych zestawów danych wejściowych algorytm podaje
wyniku zastosowania wyboru warunkowego (lub instrukcji
wyniki niezgodne z oczekiwanymi,
skoku).
W tym punkcie realizacji
procesor może nie być w stanie wykonać pewnych instrukcji
algorytmu X = 3,1415
Np. pętla nieskończona:
(np. żądamy dzielenia przez 0),
TAK
X = 100
błędy bardzo groz
ne  mogą być trudne do znalezienia
i pozostawać długo w ukryciu, nawet w trakcie wielokrotnego
NIE
używania programu w postaci kodu.
stop
X �! X + 1
Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 5 Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 6
1
Przykład algorytmu do sprawdzenia, czy nie ma błędów
Możliwe skutki i znaczenie:
Konstruujemy algorytm sumowania zarobków pracowników,
którzy zarabiają więcej niż ich bezpośredni przełożeni.
algorytm dla pewnych dopuszczalnych danych wejściowych
daje niepoprawny wynik,
Przyjmujemy koncepcję sprawdzania kolejno płac
wszystkich pracowników; dla każdego z nich będzie
wykonanie programu realizującego algorytm jest przerywane
wyszukiwana płaca jego bezpośredniego przełożonego i
w trybie awaryjnym,
porównanie tych dwóch płac będzie decydowało o dodaniu
program realizujący algorytm nie kończy w normalnym trybie
kolejnego składnika do wyznaczanej sumy.
swego działania,
Zmienna N ma wartość równą liczbie pracowników, zmienne
błędy groz
ne, ale możliwe do uniknięcia poprzez staranne
(indeksowe) I i J wskazują na kolejne elementy tablicy
opisanie struktury algorytmu przed jego zapisaniem w
jednowymiarowej P(X), która zawiera płace pracowników,
jakimkolwiek języku oraz zachowanie zasad  dobrej praktyki
zmienna S kumuluje sumę zarobków; dla każdej pary
programowania.
pracowników wskazanych aktualnymi wartościami zmiennych
I i J jest dostępna informacja, która pozwala stwierdzić, czy J
jest bezpośrednim przełożonym I.
Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 7 Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 8
start
Algorytmem całkowicie poprawnym nazywamy algorytm,
Czy podany algorytm
S �! 0;
dla którego udowodniono, że nie zawiera on ani błędów
zawiera błąd logiczny
I �! 1
logicznych, ani algorytmicznych.
lub algorytmiczny?
J �! 1
Twierdzenie, które należy udowodnić brzmi:
Czy J
 Dany algorytm dla każdego zestawu dopuszczalnych danych
TAK
jest bezpośrednim
przełożonym I?
wejściowych samoistnie przestaje działać po wykonaniu
NIE skończonej liczby operacji elementarnych, dając poprawny
NIE
P(I) > P(J)
(spełniający założone warunki) wynik końcowy
NIE
J �! J + 1 J = N TAK
Etapem pośrednim dla wykazania całkowitej poprawności
S �! S + P(I)
TAK
może być udowodnienie częściowej poprawności algorytmu.
TAK
NIE
I �! I + 1  Dla każdego zestawu dopuszczalnych danych wejściowych z
I = N
faktu, że dany algorytm samoistnie przestał działać po
Wypisz wartość S
wykonaniu skończonej liczby operacji elementarnych wynika, że
dał poprawny (spełniający założone warunki) wynik końcowy
stop
Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 9 Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 10
Dowolne Dowolne
Złożony program komputerowy może zawierać sporą
dopuszczalne dopuszczalne
liczbę błędów różnych typów, popełnionych na różnych
dane dane
etapach jego powstawania.
ALGORYTM ALGORYTM
Dla złożonego algorytmu badanie jego całkowitej
częściowo całkowicie
poprawności może być trudne i czasochłonne
poprawny poprawny
!
?
Prawdziwa jest
Prawdziwe jest
implikacja:
stwierdzenie: W praktyce opracowywania programów komputerowych
STOP
STOP jeśli to miejsce
to miejsce
pomija się (niestety) etap badania całkowitej poprawności
osiągnięto,
osiągnięto i
to wynik Poprawny algorytmu i bada się  produkt końcowy , czyli sam program:
Poprawny wynik jest
jest poprawny wynik
wynik
poprawny
testowanie na licznych zestawach danych wejściowych
(dla takiego zestawu powinien być znany wynik końcowy)
Schemat badania Schemat badania
częściowej poprawności całkowitej poprawności
uruchamianie w obecności narzędzi diagnostycznych
algorytmu algorytmu
(badanie stanów pośrednich i końcowych)
Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 11 Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 12
2
Podstawową metodą badania częściowej poprawności Po wykazaniu częściowej poprawności algorytmu
algorytmu jest metoda niezmienników, polegająca na: podstawową metodą badania jego całkowitej poprawności
jest metoda zbieżników, polegająca na:
wybraniu w schemacie algorytmu punktów kontrolnych,
ustaleniu dla każdej iteracji zbieżnika, czyli takiej zmiennej,
związaniu z każdym punktem kontrolnym tzw. asercji, czyli
której wartości zależą od stanu realizacji algorytmu po wykonaniu
warunku logicznego zależnego od stanu realizacji procesu
kolejnych powtórzeń tej iteracji i tworzą ograniczony ciąg
wyznaczania założonego wyniku końcowego,
monotoniczny,
ustaleniu w obrębie każdej z iteracji takiej asercji, której
wykazaniu, że każdy ze zbieżników nie może zmieniać się
prawdziwość będzie można wykazać po dowolnej liczbie
nieskończoną liczbę razy i algorytm po wykonaniu skończonej
powtórzeń tej iteracji (tzw. niezmiennik iteracji),
liczby powtórzeń w każdej z iteracji zatrzyma się w ostatnim
punkcie kontrolnym.
wykazaniu, że z prawdziwość jednej asercji wynika
prawdziwość następnej, że niezmienniki pozostają prawdziwe
po kolejnych iteracjach i pociągają za sobą prawdziwość
ostatniej asercji, która oznacza osiągnięcie założonego wyniku.
Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 13 Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 14
start
Przykład zastosowania metody niezmienników i zbieżnika Schemat
procedury
Badamy algorytm odwracania dowolnego napisu, którego działanie
X �! T
odwrócone
zapisane w postaci procedury odwrócone jest następujące:   oznacza napis
Y �!  
pusty (o liczbie
odwrócone( alama2koty ) =  ytok2amala
znaków równej 0)
Wykorzystamy pomocnicze procedury:
TAK
głowa( alama2koty ) =  a
X =  
ogon( alama2koty ) =  lama2koty
NIE
oraz operator konkatenacji & (złączenia) dwóch napisów:
stop
Y �! głowa(X) & Y
 alama &  2koty =  alama2koty
Po zakończeniu
X �! ogon(X )
Dla dowolnego napisu T zachodzi tożsamość:
działania ma być:
głowa(T) & ogon(T) = T
Y = odwrócone (T)
Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 15 Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 16
Wybór punktów
start
Asercja 1: Aby wykazać częściową poprawność algorytmu należy
kontrolnych i
T jest napisem
kolejno udowodnić prawdziwość następujących implikacji:
przydział asercji:
X �! T
Y �!  
Asercja 2 (niezmiennik): 1. Jeżeli asercja 1. jest prawdziwa, to asercja 2. przed
T = odwrócone(Y) & X
rozpoczęciem iteracji jest prawdziwa,
2. Jeżeli w pewnym kroku iteracji asercja 2. jest prawdziwa,
TAK
X =  
Asercja 3:
to w następnym kroku też jest ona prawdziwa (warunek z
Y = odwrócone(T)
asercji 2. stanie się wtedy niezmiennikiem iteracji),
NIE
stop 3. Jeżeli w ostatnim kroku iteracji asercja 2. jest prawdziwa, to
Y �! głowa(X) & Y
asercja 3. jest też prawdziwa (osiągnięto założony wynik).
X �! ogon(X )
Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 17 Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 18
3
Schemat wykazujący, że
Jeżeli T jest napisem (dopuszczalną daną wejściową), to
odwrócone(Y) & X = odwrócone(głowa(X) & Y) & ogon(X)
przed rozpoczęciem iteracji asercja 2. jest prawdziwa, bo
zachodzi oczywista równość:
Y: AMALA X: 2KOTY
odwrócone(  ) & T = T , dla Y =   i X = T
Jeżeli założymy, że po wykonaniu pewnej liczby iteracji zachodzi
T = odwrócone(Y) & X dla pewnego Y i X `"   , to aby wykazać, odwrócone(Y) & X: ALAMA 2KOTY
że ten warunek nadal będzie spełniony po wykonaniu następnej
odwrócone(głowa(X) & Y) & ogon(X): ALAMA2 KOTY
iteracji, wystarczy pokazać, że
odwrócone(Y) & X = odwrócone(głowa(X) & Y) & ogon(X) ,
głowa(X) & Y: 2AMALA ogon(X): KOTY
bo nowa wartość Y po wykonaniu iteracji jest równa głowa(X) & Y,
głowa(X): 2 Y: AMALA
a nowa wartość X jest równa ogon(X).
Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 19 Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 20
Aby wykazać teraz całkowitą poprawność algorytmu trzeba
Zatem po wykonaniu kolejnej iteracji zachodzi
wykazać, że dla dowolnego napisu T punkt kontrolny 2. jest
T = odwrócone(głowa(X) & Y) & ogon(X),
przechodzony tylko skończoną liczbę razy, tzn. 3. punkt
czyli asercja 2. pozostaje prawdziwa bez względu na liczbę
kontrolny jest zawsze osiągany.
powtórzeń iteracji  jest jej niezmiennikiem.
Wybieramy w tym celu zbieżnik, którym może być długość napisu
Jeżeli po ostatnim powtórzeniu iteracji prawdziwa jest asercja 2., to
będącego aktualną wartością zmiennej X.
T = odwrócone(Y) & X dla X =   , czyli T = odwrócone(Y).
Przed rozpoczęciem iteracji X = T, czyli wartość zbieżnika równa
Z oczywistej równości
jest długości napisu T (liczba całkowita nieujemna).
odwrócone(T) = odwrócone(odwrócone(Y)) = Y
Po każdym powtórzeniu iteracji wartość zbieżnika maleje o 1,
bo X �! ogon(X ).
wynika prawdziwość asercji 3.
Wartość zbieżnika (długość napisu) nie może być mniejsza od
Wykazana została częściowa poprawność algorytmu:
zera, a zatem iteracja może zostać powtórzona tylko skończoną
liczbę razy i algorytm osiągnie punkt kontrolny 3.
jeżeli T jest napisem, to Y = odwrócone(T) w punkcie kontrolnym 3.
Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 21 Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 22
Wykazana została całkowita poprawność algorytmu:
Rozwiązanie z 1976 r. (Appel i Haken)
dla każdego napisu T algorytm znajdzie się w punkcie
Twierdzenie:
kontrolnym 3. z wynikiem Y = odwrócone(T).
Cztery barwy zawsze wystarczą do pokolorowania dowolnej
płaskiej mapy, tak aby każdy z dwóch sąsiadujących obszarów
Przykład do czego prowadzą trudności w stosowaniu metody
różnił się kolorem.
niezmienników i zbieżników
Problem kolorowania mapy płaskiej z 1852 r. (de Morgan) Dowód
Zbudowano algorytmy rozwiązujące problem kolorowania w
szczególnych przypadkach map, które wyczerpują wszystkie
możliwe typy map płaskich.
Nikt formalnie nie udowodnił całkowitej poprawności tych
algorytmów!
Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 23 Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 24
4
Dla większości algorytmów rekurencyjnych dowód ich
Iteracyjny algorytm dla problemu wież Hanoi
całkowitej poprawności może być przeprowadzony po
usunięciu najpierw rekurencji z algorytmu  zastąpieniu go
1. Powtarzaj, co następuje:
równoważnym algorytmem opartym na iteracjach 
1.1. przenieś najmniejszy z dostępnych krążków z kołka, na
i zastosowaniu potem metody niezmienników i zbieżników.
którym się znajduje, na kołek następny w kierunku ruchu
Przykład usunięcia rekurencji z algorytmu  wieże Hanoi
wskazówek zegara,
1.2. jeżeli na kołku C znajdują się już wszystkie krążki, to
Ustaw trzy kołki na okręgu
zakończ działanie,
1.3. wykonaj jedyne możliwe przeniesienie nie zmieniające
A
położenia najmniejszego krążka, który został przeniesiony
w kroku 1.1.
C B
Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 25 Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 26
A A A A
1. 2. 3. 4.
C B C B C B C B
(1.1) (1.2) (1.1)
A B A C B C



A A A A
5. 6. 7. 8.
C B C B C B C B
(1.2) (1.1) (1.2) (1.1)
A B C A C B A B



Jarosław Sikorski - BUDOWA i ANALIZA ALGORYTMÓW, WIT 2006 r. 27
5