Metody dowodzenia poprawności cz I 2

Etapy działania algorytmu:

Y    = n | 0 czyli Y = n X = os

Y    = on X = s

Y    = son X = 0

Zdefiniowanie asercii dla naszego algorytmu:

I — zbiór zawierający wszystkie skończone napisy S

Asercia początkowa:

Asercja 1: Sjest napisem

Asercia końcowa:

Niech R relacja określająca prawidłowe działanie algorytmu Postać relacji R:

Y = odwrócenie (S) wynik    dane wejściowe

Asercja 3: Y = odwrócenie (S)

Jeśli ta asercja jest prawdziwa to algorytm jest poprawny względem I oraz R.

Asercia wewnętrzna:

Tworzymy ją tak, by w każdej iteracji pętli styyierdzała, iż spełniony jest warunek, że S jest początkowym napisem.

Ma ona postać:

Asercja 2: S = odwrócenie (Y) | X

Ponieważ w każdej chwili pętli Y stanowi odwrócenie początkowe części napisu, a Xjego nie odwróconąjeszcze część dalszą, więc w istocie S jest początkowym napisem w Asercji 2.

Algorytm no wstawieniu asercii: odwrócenie (S)

{Asercja 1: Sjest napisem}

X: = S;

Y: = 0; etykieta:

{asercja 2: S = odwrócenie (Y) | X} ifX= 0 then odwrócenie: = Y;

STOP {Asercja 3: Y = odwrócenie (S)} eise

Y: = głowa (X) | Y;

X: = ogon (X); go to etykieta; end odwrócenie;