Matematyka Dyskretna
Andrzej Szepietowski
25 czerwca 2002 roku
Rozdział 1
Poprawność programów
Jeżeli projektujemy algorytmy lub piszemy programy, to ważne jest pytanie, czy nasz al-
gorytm lub program jest poprawny, czy nie zawiera błędów. Konkretniej, możemy spytać,
czy nasz program jest napisany zgodnie z regułami języka programowania i czy liczy to,
co chcemy.
1.1 Poprawność syntaktyczna
Jeżeli program jest napisany zgodnie z regułami języka programowania, to mówimy, że
jest poprawny pod względem syntaktycznym, a wykroczenia przeciwko składni języka
nazywają się błędami syntaktycznymi. Przykładami takich błędów w języku Pascal są:
użycie zmiennej, która wcześniej nie została zadeklarowana, lub postawienie średnika
przed słowemelsew instrukcji warunkowej.
Poprawność syntaktyczna nie jest wielkim problemem. Języki programowania mają
bardzo ścisłe reguły składni, określające, jak budować poprawne programy, i konstrukto-
rzy tych języków zadbali o to, aby można było łatwo wykryć błędy syntaktyczne. Istnie-
ją kompilatory, które automatycznie sprawdzają poprawność syntaktyczną programów.
Kompilatory niektórych języków są dość skomplikowanymi programami i oprócz komu-
nikatu o błędzie dają także wskazówki, jak błąd usunąć.
1.2 Poprawność semantyczna
Dużo poważniejszym problemem jest poprawność semantyczna, czyli stwierdzenie, czy
program lub algorytm liczy to, co powinien. Problem zaczyna się już wówczas, gdy spy-
tamy, co to znaczy liczy to, co powinien .
Zajmiemy się teraz jednym z możliwych podejść do problemu poprawności. Program
przekształca dane wejściowe w dane wyjściowe i dlatego możemy go traktować jak funk-
cję ze zbioru danych wejściowych w zbiór danych wyjściowych. Na przykład dla algo-
rytmu Euklidesa (porównaj rozdział o teorii liczb) danymi wejściowymi są pary liczb
3
4 Rozdział 1. Poprawność programów
naturalnych, a danymi wyjściowymi są pojedyncze liczby naturalne. W algorytmie sor-
tującym danymi wejściowymi i wyjściowymi są ciągi liczb. Żeby określić co program
robi definiuje się warunki: jeden warunek mówi, jakie powinny być dane wejściowe, a
drugi warunek określa, jakie powinny być dane wyjściowe.
Problem algorytmiczny możemy więc zdefiniować przez podanie:
zbioru danych wejściowych ,
zbioru danych wyjściowych ,
predykatu (funkcji zdaniowej) , który określa warunki początkowe; przyj-
muje wartość prawda, jeżeli dane wejściowe są poprawnie zbudowane,
predykatu , który określa relację pomiędzy danymi wyjściowymi i wejściowymi;
ma wartość prawda, jeżeli dane wyjściowe są prawidłową odpowiedzią
algorytmu na dane wejściowe .
W przykładzie algorytmu Euklidesa:
dane wejściowe to pary liczb naturalnych ,
dane wyjściowe to zbiór liczb naturalnych ,
warunek początkowy ,
relacja określa, że jest największym wspólnym dzielnikiem liczb i .
Zadanie algorytmiczne sortowania może być zdefiniowane w następujący sposób (dla
prostoty zakładamy, że sortujemy ciągi różnowartościowe):
i to zbiory wszystkich ciągów długości ,
warunek mówi, że ciąg jest różnowartościowy:
warunek określa, że ciąg jest rosnący i zawiera dokładnie te same ele-
menty co ciąg :
and
Takiego typu warunki nazywają się specyfikacją algorytmu lub programu. Jednym
słowem, specyfikacja mówi nam, co program ma robić. Program działa poprawnie, jeżeli
dla każdych danych wejściowych , spełniających warunek wejściowy , daje wynik
, który spełnia warunek wyjściowy .
Zwykle dowód poprawności programu rozbija się na dwa poddowody. Osobno dowo-
dzi się poprawności przy założeniu, że program zawsze się zatrzyma, a osobno dowodzi
się, że program zatrzymuje się dla każdych poprawnie zbudowanych danych wejścio-
wych.
1.3. Niezmienniki 5
Definicja 1.1 Program jest częściowo poprawny względem warunków i , gdy dla każ-
dych danych wejściowych spełniających zachodzi następująca implikacja: jeżeli
program zatrzymuje się na danych i daje wynik , to zachodzi warunek .
Program jest całkowicie poprawny, jeżeli jest częściowo poprawny i ponadto zatrzy-
muje się dla każdych danych wejściowych spełniających warunek .
Jedną z metod dowodzenia częściowej poprawności programu jest metoda niezmien-
ników lub asercji indukcyjnych.
1.3 Niezmienniki
Metoda niezmienników polega na wyznaczeniu w programie kilku punktów kontrolnych
i związaniu z tymi punktami asercji, czyli pewnych warunków. Wśród punktów kontrol-
nych dwa są szczególne: jeden punkt zaraz na początku programu z asercją początkową
i jeden punkt na końcu programu z asercją końcową. Asercja początkowa zwykle zawie-
ra sformułowania obejmujące warunki na dane początkowe . Asercja końcowa opisuje
relację wiążącą dane wejściowe z wyjściowymi. Po wyznaczeniu punktów i asercji
dowodzimy, że każda asercja jest spełniona zawsze wtedy, gdy wykonanie programu doj-
dzie do odpowiadającego jej punktu kontrolnego. W ten sposób dowodzimy, że jeżeli na
początku był spełniony warunek początkowy i potem program dojdzie do punktu koń-
cowego, to będzie spełniony warunek . Dowód poprawności może przebiegać w ten
sposób, że dla poszczególnych par punktów kontrolnych i (niekoniecznie różnych)
dowodzimy następującą implikację: jeżeli w punkcie spełniona jest asercja , a na-
stępnie wykonanie programu przejdzie z punktu do , to w punkcie będzie spełniona
asercja .
Niektóre punkty kontrolne mogą być w trakcie wykonywania programu osiągane wie-
lokrotnie (na przykład punkty znajdujące się wewnątrz pętli). Tak więc asercja powinna
być spełniona za każdym odwiedzeniem punktu kontrolnego. Z tego powodu asercje te
nazywamy niezmiennikami.
Sposób rozmieszczenia punktów kontrolnych i przypisania tym punktom asercji nie
jest prosty i nie ma uniwersalnych reguł w tym względzie. Podobnie jak z dowodzeniem
twierdzeń, sposób dowodu poprawności programu jest oryginalnym pomysłem autora do-
wodu. Istnieją w tym względzie pewne reguły heurystyczne, niektóre nawet bardzo zło-
żone, ale nie ma uniwersalnych reguł, które pozwolą udowodnić poprawność lub niepo-
prawność każdego programu.
1.4 Liczniki
Aby udowodnić, że algorytm zawsze się zatrzyma, możemy użyć liczników. Najpierw,
podobnie jak poprzednio, wyznaczamy punkty kontrolne i pewną zmienną, zwaną licz-
nikiem lub zbieżnikiem, która może przyjmować tylko wartości całkowite nieujemne.
Następnie dowodzimy, że po każdym odwiedzeniu jakiegoś punktu kontrolnego wartość
licznika maleje.
6 Rozdział 1. Poprawność programów
Nie ma miejsca w tej książce na rozwijanie teorii dowodzenia poprawności progra-
mu. Zajmiemy się tylko dwoma przykładami. Pierwszy to algorytm Euklidesa, który był
przedstawiony w rozdziale z teorii liczb i tam też przedstawiono dowód jego poprawności.
Teraz tylko sformułujemy go w języku asercji.
1.5 Algorytm Euklidesa jeszcze raz
Oto jeszcze raz algorytm Euklidesa opisany w języku Pascal:
var a,b,p,q:integer;
begin
readln(a,b);
{A}
p:=a;q:=b;
while p<>q do
{C}
if p>q then p:=p-q
else q:=q-p;
{B}
writeln( NWD( ,a, , ,b, )= ,p)
end.
W programie umieściliśmy trzy punkty kontrolne. Punkt na początku, zaraz za
instrukcją readln(a,b). Asercja związana z punktem orzeka, że i to dwie dodatnie
liczby całkowite.
Punkt znajduje się na końcu programu, tuż przed instrukcjąwriteln. Asercja
związana z tym punktem orzeka, że zawiera największy wspólny dzielnik liczb i .
Trzeci punkt kontrolny jest wewnątrz pętli, tuż przed instrukcją warunkową if.
Asercja orzeka, że para liczb i ma taki sam największy wspólny dzielnik co para
i .
Dowodzimy cztery implikacje:
jeżeli wykonanie programu jest w punkcie i spełniona jest asercja , a następ-
nie program przejdzie do punktu , to spełniona będzie asercja ,
jeżeli wykonanie programu jest w punkcie i spełniona jest asercja , a następ-
nie program ponownie przejdzie do punktu , to spełniona będzie asercja ,
jeżeli wykonanie programu jest w punkcie i spełniona jest asercja , a następ-
nie program przejdzie do punktu , to spełniona będzie asercja ,
jeżeli wykonanie programu jest w punkcie i spełniona jest asercja , a następ-
nie program przejdzie do punktu , to spełniona będzie asercja .
1.6. Potęgowanie 7
Naszkicujmy tylko dowód drugiej implikacji, pozostałe dowodzi się podobnie. Załóż-
my, że wykonanie programu znajduje się w punkcie i że zmienne i mają wtedy
wartości i . Jeżeli w wyniku dalszego wykonania program ponownie dojdzie do
punktu , to znaczy, że , bez straty ogólności możemy założyć, że .
Wtedy nowe wartości zmiennych i mają wartości oraz . Z faktu,
że wartości i spełniają asercję , wynika, że para i ma taki sam naj-
większy wspólny dzielnik jak para wejściowa i . W rozdziale o teorii liczb pokazano,
że para ma taki sam zbiór wspólnych dzielników jak para . Tak więc także para
ma taki sam największy wspólny dzielnik jak para , więc spełnia asercję .
Aby pokazać, że program zatrzymuje się dla każdych danych spełniających warunek
, wprowadzimy licznik dla punktu kontrolnego . Licznikiem tym jest wartość
. Jest jasne, że wartość licznika jest zawsze liczbą całkowitą nieujemną i że
zmniejsza się przy każdym ponownym odwiedzeniu punktu . Wykonanie programu nie
może więc trwać w nieskończoność.
1.6 Potęgowanie
Drugim przykładem niech będzie program na podnoszenie liczby dwa do potęgi .
var n,x,y:integer;
begin
readln(n);
{A}
y:=1;
x:=n;
while x>0 do
begin
{C}
x:=x-1;
y:=y+y
end;
{B}
writeln(y)
end.
W tym programie też są trzy punkty kontrolne. Punkt na początku, zaraz za instruk-
cjąreadln, z asercją:
Punkt na końcu programu, tuż przed instrukcjąwriteln, z asercją:
Trzeci punkt kontrolny jest wewnątrz pętli, tuż przed instrukcjąx:=x-1, z asercją:
8 Rozdział 1. Poprawność programów
Dowód poprawności programu polega teraz na dowodzie tych samych czterech impli-
kacji, które znajdują się w podrozdziale 10.5.
Aby udowodnić, że program zawsze się zatrzyma, wystarczy jako licznik przyjąć
zmienną , która przyjmuje wartości nieujemne i zmniejsza swoją wartość przy każdym
kolejnym odwiedzeniu punktu .
1.7 Czekery
W przypadku gdy udowodnimy, że jakiś program działa poprawnie, wówczas mamy pew-
ność, że dla każdych danych wejściowych uzyskany wynik będzie dobry. Inną metodą
sprawdzania, że program działa poprawnie, są czekery. Zamiast dowodzić, że program
zawsze zadziała dobrze, czekery sprawdzają, czy zadziałał on dobrze w konkretnych przy-
padkach. Do zadania algorytmicznego projektowane są dwa programy. Program główny
, który rozwiązuje zadanie, oraz program , zwany czekerem lub weryfikatorem, który
po każdym zadziałaniu programu sprawdza, czy odpowiedz programu jest popraw-
na. Zakłada się przy tym, że działanie czekera jest dużo prostsze niż działanie programu
. W dodatku program może być traktowany jak czarna skrzynka, gdzie nie mamy
wglądu w to, jak program działa, tylko dostajemy ostateczne odpowiedzi. Przyjrzyjmy
się pomysłowi czekerów na przykładach.
Wezmy znowu algorytm Euklidesa, ale teraz wygodniej jest wziąć wersję, gdzie pro-
gram bierze parę liczb i i zwraca trzy oraz i , takie że
liczby:
. Żeby sprawdzić, czy program dobrze obliczył dane wyjściowe, wystarczy
sprawdzić, czy dzieli i , oraz czy
Inny przykład to czeker dla programu obliczającego zaokrąglenie w górę pierwiastka
kwadratowego z liczby naturalnej . Przykład takiego programu przedstawiono w roz-
dziale 3.5. Jeżeli program główny oblicza dla wartości wejściowej wartość wyjściową
, to zadanie czekera polega na sprawdzeniu dwóch rzeczy, czy
oraz czy
1.8 Zadania
1. Udowodnij poprawność programu (przedstawionego w podrozdziale 6.6), który dla
danych liczb , oblicza oraz liczby całkowite , spełniające
równość .
Wyszukiwarka
Podobne podstrony:
Matematyka dyskretna 2002 09 Grafy nieskierowaneMatematyka dyskretna 2002 02 ArytmetykaMatematyka dyskretna 2002 08 Struktury danychMatematyka dyskretna 2002 07 RekurencjaLista zadan nr 3 z matematyki dyskretnej2002 11 Wyświetlacz widmowyAlgorytmy Matematyka Dyskretnamatematyka kl 6 1 EK2 11 inst11 Jezyki programowania Historia Przykładyid434Matematyka Dyskretna ZadaniaMatematyka Dyskretna Grafy Zadaniawięcej podobnych podstron