1 Grażyna Mirkowska PJWSTK 15 listopad 2000Metody Analizy Programów Wykład 04 Metoda Floyda badania poprawności programu Grażyna Mirkowska PJWSTK 15 listopad 2000 Metody Analizy Programów Wykład 04

2 Metody Analizy Programów Wykład 04Przypomnienie Przykład while xy do if x>y then x:=x-y else y := y-x fi od Różne specyfikacje tego algorytmu: y , x=y > < k|x and k|y , ky > Definicja Program P jest częściowo poprawny ze względu na specyfikację w strukturze danych M wttw dla każdych danych w strukturze M, jeżeli warunek początkowy a specyfikacji jest spełniony przez dane i program zatrzymuje się po skończonej liczbie kroków, to warunek końcowy b jest spełniony przez wyniki programu, tzn. Dla każdego wartościowania v w strukturze M, M,v |= (a and Ptrue ) => Pb Integer = < {min,...,max}, +, *, -, |, div, mod, , = > Definicja Specyfikacją algorytmu programu będziemy nazywali parę warunków(formuł) . Intuicyjnie odpowiadają one warunkowi, które powinny spełniać dane (warunkowi początkowemu) i warunkowi, który powinien być spełniony po zakończeniu algorytmu (warunkowi końcowemu). Metody Analizy Programów Wykład 04

3 Floyd (1967) : Podzielić program na jak najmniejsze moduły, których częściowa poprawność jest łatwa do udowodnienia, a następnie korzystając z tych informacji udowodnić częścio- wą poprawność całego programu. Dokładniej: Dla danego programu skonstruować diagram przepływu (schemat blokowy) każdej krawędzi przyporządkować formułę, w taki sposób, by w czasie realizacji algorytmu (programu), wa- runki przypisane dowolnej krawędzi były spełnione przez wartościowanie, które obowiązuje w chwili przejścia przez tę krawędź. Metoda Floyda Flowdiagram programu P: START x:=1;y:=1 x=1, y=1 Przykład 2. Niech P będzie następujacym programem: begin x:=1; y:=1; while y < n do x:= x+2y+1; y := y+1 od end Niech R będzie strukturą, w której interpretujemy ten program. y TAK NIE y y=n, y N, x=n2 STOP x := x+(2y+1) y+1 y := y+1 y Metody Analizy Programów Wykład 04

4 Metody Analizy Programów Wykład 04Definicja Schemat blokowy programu P wraz z przypisanymi jego krawędziom formułami nazywamy opisem programu P. Powiemy, że opis programu P w strukturze M jest poprawny (akceptowalny) wttw gdy dla każdego wykonania programu P, w chwili przejścia przez dowolną krawędź, odpowiadająca jej formuła jest spełniona przez aktualne wartościowanie. x>0 y*y= x x>0 x>y START y:= sqrt(x) STOP START y:= sqrt(x) STOP Ten opis jest akceptowalny w R, a ten opis nie jest akceptowalny w R Twierdzenie Jeżeli program P ma akceptowalny opis w strukturze M taki, że a jest formułą przypisaną jego wejściowej krawędzi, a b jest formuła przypisaną krawędzi wyjściowej, to program P jest w strukturze M częściowo poprawny ze względu na specyfikację <, b >, tzn. M |= (( Ptrue)  P b) Metody Analizy Programów Wykład 04

5 Jak uzyskać akceptowalny opis programu?Niech będą akceptowalne opisy programów P1 i P2 w strukturze M Akceptowalny opis instrukcji przypisania START START a1 a2 a(x/t) Twierdzenie Jeżeli program Pi jest częściowo poprawny ze względu na specyfikację w strukturze danych M, gdzie i=1,2 oraz M |= (b1 g)  (g  a2) , to program P= begin P1; P2 end jest częściowo poprawny w M ze względu na specyfikację . a(x) P2 P1 START x:= t STOP b2 b1 Wtedy następujący opis złożenia programów begin P1;P2 end jest akceptowalny w strukturze M, o ile spełniony jest warunek (*) STOP STOP warunek(*) M |= (b1 g)  (g  a2) START P1 P2 STOP a1 g b2 Metody Analizy Programów Wykład 04

6 c.d. Konstrukcja akceptowalnych opisów.Niech będą akceptowalne opisy programów P1 i P2 w strukturze M Wtedy następujący opis instrukcji warunkowej if g then P1 else P2 fi jest akceptowalny w strukturze M, o ile spełniony jest warunek (**) Twierdzenie Jeżeli program Pi jest częściowo poprawny ze względu na specyfikację < ai, bi> w strukturze M dla i =1,2, oraz jeżeli formuła ((a  g )  a1 ) ((a  g )  a2) jest prawdziwa w M, to program P=if g then P1 else P2 fi jest częściowo poprawny w M ze względu na specyfikację < a ,( b1b2 ) >. START START START a1 a2 a g P2 P1 TAK NIE (a1 g) (a2 g) b2 b1 STOP STOP P2 P1 Warunek(**) M |= (a  g )  a1 M |= (a  g )  a2 (b1 b2) STOP Metody Analizy Programów Wykład 04

7 c.d. Konstrukcja akceptowalnego opisu programu.Wtedy następujący opis instrukcji pętli while g do P1 od jest akceptowalny w strukturze M, pod warunkiem (***) Niech będzie akceptowalny opis programu P1 w strukturze M Twierdzenie Jeżeli program P1 jest częściowo poprawny w strukturze M ze względu na specyfikację < a1,b1> oraz M |= ((a  g)  a1) (b1  b) ((b  g)  a1 ), to program P= while g do P1 od jest częściowo poprawny ze względu na specyfikację < a, ((a  b) g)> START START a1 a b g P1 TAK NIE (a1 g) b1 ((a  b) g) STOP Warunek (***) M |= (a  g)  a1 M |= (b1  b) M |= (b  g)  a1 P1 STOP b Metody Analizy Programów Wykład 04

8 Przykład 3 Przedstawiony opis jest akceptowalny w strukturze liczb naturalnych. START x>0, y>0 begin q := 0; r := x; while y > r do r := r - y; q := q od end Rozważmy ten program w strukturze liczb naturalnych. q:=0; r :=x q=0, r=x, x>0, y>0 q>0, r  0, x=qy+r r  y TAK NIE q  0, r  y , x=qy+r q  0, r r := r-y Program jest częściowo poprawny ze względu na warunek początkowy x>0, y>0 i warunek końcowy q= x div y , r = x mod p. STOP q  0, r  0, x=qy+r+y q := q+1 q>0, r  0, x=qy+r Metody Analizy Programów Wykład 04

9 Przykład 4 START x>0 Ostatecznie, przedstawiony program jest częściowo poprawny ze względu na warunek początkowy x>0 i warunek końcowy y= x- sqrt(x) 2 begin y := 1; i := 0; z := x; while z-y >0 do i := i+1; z := z-y; y := y+2 od; if z=y then y := 0 else y := z fi; end y :=1; i :=0; z:= x i=0, z=x, x>0, y=1 z > y TAK NIE y= 2i+1, z  y , x=i2+z y= 2i+1 ,z y, x=i2+z i := i+1 z=y y= 2i-1, z  y , x=(i-1)2+z= i2+z-y TAK NIE x=(i+1)2 z := z-y y:=0 y:=z y= 2i-1, z  0 , x=i2+z y= x- i2 y := y+2 STOP y= 2i+1, z  0 , x=(i-1)2+z+y-2 Metody Analizy Programów Wykład 04

10 Twierdzenie Jeżeli program P jest częściowo poprawny ze względu na specyfikację w strukturze M , oraz formuły ( a*  a), ( b  b*) są prawdziwe w M, to program P jest częściowo poprawny ze względu na specyfikację Fakt, że program jest częściowo poprawny w strukturze M ze względu na warunek początkowy a i warunek końcowy b przyjęto zapisywać w postaci M |= {a} P {b} Stosując powyższą notację twierdzenie możemy zapisać w postaci: Jeżeli M |= {a} P {b} , M|=(a*  a), M |= (b  b*) to M |= {a*} P {b*}. Metody Analizy Programów Wykład 04

11 Metody Analizy Programów Wykład 04Algorytm znajdowania tranzytywnego domknięcia grafu. Przykład 5 Algorytm Warshall’a. for k := 1 to n do for i := 1 to n do for j := 1 to n do P(i,j) := P(i,j)  (P(i,k)  P(k,j)) od od od Metody Analizy Programów Wykład 04

12 Metody Analizy Programów Wykład 04Przykład 6 Algorytm pozwala obliczyć długość najkrótszej ścieżki od i do j for k :=1 to n do for i := 1 to n do for j :=1 ton do P(i,j) := min(P(i,j), P(i,k) + P(k,j)) od od od; Metody Analizy Programów Wykład 04

13 Metody Analizy Programów Wykład 04Przykład 7 For k :=1 to n do for i :=1 to n do for j :=1 ton do P(i,j) := max(P(i,j), min(P(i,k), P(k,j))) od od od Algorytm pozwala wyliczyć maksymalny ciężar jaki może być przetransportowany z punktu i do punktu j. Metody Analizy Programów Wykład 04

14 Metody Analizy Programów Wykład 04Przykład 8 Niech V będzie zbiorem wierzchołków pewnego skończonego, etykietowanego drzewa rzędu rz, o korzeniu w wierzchołku v. Rozważmy program P, działający w strukturze Stosów Program pozwala przeglądać drzewo w porządku „w głąb”. P: begin x := włóż(v, x); while not pusty(x) do v := pierwszy(x); wypisz_etykietę(v); x := usuń(x); for i := 1 to rz do x := włóż(v.syn(i),x) od; od; end; Metody Analizy Programów Wykład 04

15 Metody Analizy Programów Wykład 04Jeżeli zaimplementowano STR jako strukturę KOLEJEK, to program realizuje przeglądanie grafu poziomami. Przykład 9 P: begin x := włóż(v, x); while not pusty(x) do v := pierwszy(x); wypisz_etykietę(v); x := usuń(x); for i := 1 to rz do x := włóż(v.syn(i),x) od; od; end; Metody Analizy Programów Wykład 04

16 Metody Analizy Programów Wykład 04Przykład 10 Niech P będzie programem działającym w strukturze liczb całkowitych Algorytm Euklidesa begin r := n mod m; while r0 do n := m; m := r; r := n mod m od; wynik := m; end; Metody Analizy Programów Wykład 04

17 Metody Analizy Programów Wykład 04Przykład 11 Rozważmy następujący program P działający w strukturze kolejek priorytetowych Algorytm SORTUJE wczytany ciąg elementów! P: begin for i :=1 to n do read(e); pq := włóż(e,pq) od; while not pusty(pq) do e := pierwszy(pq); wypisz(e); pq := usuń(pq) od end Metody Analizy Programów Wykład 04

18 Metody Analizy Programów Wykład 04Niech q będzie kolejką priorytetową wszystkich krawędzi pewnego niezorientowanego, spójnego grafu G=, dla którego jest określona funkcja kosztu c : E R+, i niech p0 będzie podziałem początkowym zbioru V. Przykład 12 while card(p) >1 do Algorytm Kruskala: begin p := p0; while not empty(q) do kr := first(q); q := delete(q); A := Find(p,k.początek); B := Find(p,k.koniec) if A =/= B then p := Union(p,A,B); wypisz(k) fi od end Algorytm pozwala znaleźć minimalne drzewo rozpinające grafu. Metody Analizy Programów Wykład 04

19 Metody Analizy Programów Wykład 04Przykład 13 Rozważmy algorytm P w strukturze danych złożonej ze struktury Kolejek i struktury Find-Union. P: begin p := p0; while not empty(q) do kr := first(q); q := delete(q); A := Find(p,k.początek); B := Find(p,k.koniec) if A =/= B then p := Union(p,A,B); fi od; wypisz(p) end Niech będzie dany graf G= i niech q będzie kolejką wszystkich krawędzi, a p0 podziałem początkowym zbioru wierzchołków tego grafu . Algorytm pozwala znaleźć spójne składowe danego grafu. Algorytm znajduje klasy abstrakcji najmniejszej relacji równoważności zawierającej E. Metody Analizy Programów Wykład 04