Metody dowodzenia poprawności cz I 1

METODY DOWODZENIA POPRAWNOŚCI CZĘŚĆ I

1.    Odtąd mówiąc o poprawności będziemy myśleć o poprawności częściowej.

2.    Proces dowodzenia każdego konkretnego algorytmu polega na kontroli pewnych niezmienników — zdefiniujemy je za chwilę. Taka technika nosi nazwę metody Floyda.

Metoda Floyda:

Metoda Floyda polega na znalezieniu w strukturze pewnych punktów kontrolnych i umieszczeniu w nich specjalnych stwierdzeń logicznych tzw. aseicii indukcyjnych. Stwierdzenia te winny być prawdziwe (traktowane jako wyrażenia logiczne), aby algorytm mógł być uznany za poprawny. Dana asercja musi mieć zawsze tę samą wartość logiczną bez względu na to ile razy algorytm przechodzi przez ten punkt kontrolny. Stad nazywa się je często niezmiennikami algorytmu.

3.    Jak tworzyć asercie?

a.    aseicia początkowa — jeśli I jest zbiorem poprawnych danych wejściowych to asercja początkowa ma postać stwierdzenia: "dane należą do I"

b.    aseicia końcowa — jeśli Rjest oczekiwaną relacją między danymi wejściowymi a poprawnym wynikiem to asercja końcowa stwierdza "wyniki spełniają relację R"

c.    aseicie wewnatiz alaoiytmu — często trudne do sformułowania. Musza one się opierać na wartościach zmiennych obliczanych przez algorytm, ale trzeba je tak wykorzystać by zmieniające sie wartości zmiennych uiać w asercii w kształt uniwersalnego niezmiennika.

Rozważymy to na przykładach:

Przykład I:

Algorytm A do odwracania ciągu znaków S (wypisanie wyrazów odwrotnie)

Działanie tego algorytmu, który nazwiemy "odwrócenie"(anagram) odwrócenie (’nos‘) = "son"

Zapis algorytmu: odwrócenie (S)

X: = S;

Y: = 0; 0 — znak pusty (napis nie zwierający ani jednego znaku) etykieta:

ifk= 0 tfien odwrócenie: = Y; STOP else

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

X; = ogon (Xj; go to etykieta; er>d odwrócenie

"ogon" i "głowa" — to dwa inne dostępne algorytmy o działaniu głowa ('nas') = "n" ogon (’nas‘) = "as"

dodatkowo wprowadzono symbol konkatenacji (połączenie) n | os - nas