Metody dowodzenia poprawności cz I 3

Pokażemy, że asercie sa niezmiennikami:

czyli, że sa prawdziwe ilekroć algorytm do nich dotrze.

Odcinki między punktami kontrolnymi (asercjami) przebywane przez algorytm:

(1)    — (2) jeden raz

(2)    — (2) wiele razy (2) — (3) jeden raz

Wykazanie niezmienności wymaga pokazania, że jeśli asercia na początku odcinka jest prawdziwa, to i na końcu odcinka też.

Jeśli pierwsza asercja jest poprawna, a z prawdziwości asercji na początku odcinka wynika prawdziwość asercji na jego końcu, to prawdziwość sie propaguje

(1) — (2)— (2) — (3)

dostarczając prawdziwości asercji ostatniej, która stwierdza, iż wynik jest poprawny.

TAK DOWODZIMY POPRAWNOŚCI ALGORYTMU

Sprawdzanie zachoyyania prawdziwości asercji na odcinkach kontrolnych:

Odcinek — (2)

Asercja (1) stwierdza, że Sjest napisem. Potem wykonywane są operacje X: = S Y: = 0

Ponieważ Y jest puste, a X zawiera S w wersji nieodwróconej, więc wersja 2 jest oczywiście spełniona: asercja 2:

S =    odwrócenie    (Y) | X

odwrócenie zbioru pustego    poprawny (nieodwrócony) napis

Odcinek (2) — (3)

Jeśli spełniona jest asercja 2:S = odwrócenie (Y) | X i jeśli jest spełniony warunek X = 0 stanowiący bramkę na drodze do asercji 3, to oczywiście spełniona jest asercja 3:Y = odwrócenie (Ś)

Odcinek (2) — (2)

Ten odcinek nastręcza najwięcej problemów, bo dotyczy pętli. Mamy tu dwa założenia:

1.    prawdziwość asercji 2: S = odwrócenie (Y) | X na początku odcinka

2.    X # 0 warunek wejścia na drogę (2) — (2) czyli wykonywanie pętli Na tym odcinku wykonujemy:

(*)Y: = głowa (X) | Y; (odcinam "głowę"(pierwszy element) X, dołączam na początku Y)

X: = ogon (X); (reszta napisu staje się jego nową wartością)

Jeśli Y jest początkowo pusty, to asercja dwa jest oczywiście spełniona. Podobnie, gdy Y zawiera jeden znak a X resztę (odwrócenie znaku jest znakiem). Jeśli Y zawiera przynajmniej dwa znaki, to są to dwa pierwsze znaki napisu przedstawione w odwrotnej kolejności, zaś X mieści resztę napisu w oryginalnym porządku, zatem odwrócenie przywraca kolejność oryginalną, do tego jest dołączana reszta napisu w oryginalnym porządku, zatem asercja 2 jest spełniona.

Prawdziwość asercji 2 wymaga zatem, by spełniona była zależność: odwrócenie (Y) | X = odwrócenie (głowa (X) | Y) ogon (X), (wynika z podstawienia (*))

a tu warunkiem jest jedynie by X był niepusty, bo pusty zbiór nie ma głowy ani ogona, ale to gwarantuje nam założenie b) stanowiące przepustkę do wejścia na drogę (2) — (2).

To kończy dowód poprawności częściowej algorytmu.