SpecVer/Winograd: Różnice pomiędzy wersjami

Wersja z 17:54, 12 lut 2013

Przedstawiamy algorytm Winograda i dowód jego poprawności.

Wprowadzenie

Algorytm Winograda może być przydatny w obliczaniu iloczynu macierzy kwadratowych, szczególnie gdy elementami macierzy są obiekty reprezentujące jakieś ciało inne od ciała liczb rzeczywistych. Tzn. w przypadku gdy dane ciało [math]\mathcal{C}[/math] jest zaimplementowane w programie przez klasę [math]C[/math].

Drugim i ważniejszym powodem do skreślenia tej notatki jest potrzeba zwrócenia uwagi na znikomą przydatność asercji i tzw. programowania przez kontrakt (ang. design by contract). Asercje są przydatne jako notatki, ale nie stanowią rozwiązania problemu zapewnienia poprawności algorytmu.

Zapraszam do czytania, zwłaszcza rozdziału Dowód poprawności.

Algorytm

W tym rozdziale pojawiają się dwa warunki:

• warunek wstępny -- Precondition,
• warunek końcowy -- Postcondition, oraz
• algorytm -- algorytm Winograda.

Jak się upewnić, że algorytm jest poprawny ze względu na warunek początkowy i warunek końcowy? W literaturze proponowane są dwa podejścia:

• udowodnij częściową porawność sprawdzając pewne niezmienniki -- jest to tzw. metoda Floyda-Hoare'a,
• wykonaj pewną liczbę obliczeń testowych i zaufaj, że w trakcie eksploatacji algorytmu nie okaże się, że jest on niepoprawny.

W obliczeniach testowych można w trakcie obliczeń sprawdzać wcześniej wstawione warunki -- asercje. Czy rzeczywiście są one pomocne?

W następnym rozdziale pokażemy inną drogę - drogę dowodzenia lematów i w końcu twierdzenia o poprawności (całkowitej) algorytmu Winograda względem warunku początkowego Precondition i warunku końcowego Postcondition.

signal Niezgoda;

unit Winograd: procedure(A,B: arrayof arrayof real; output C: arrayof arrayof real);

var i,j,k,n,m: integer,

      W,V: arrayof real,
      p: boolean,
      s: real;
           

begin (* ustalic czy macierze moga byc mnozone tzn.

  czy ilosc wierszy w A = ilosc kolumn w B? *)

(* ustalic czy n jest parzyste? *)

(* obliczyc "preprocessing" *)

i := upper(A);

j := lower(A);

k := i-j;

i:= upper(B);

j:= lower(B);

if i-j <> k then raise Niezgoda fi;

(* mozna mnozyc *)

n := k+1;

p := (n mod 2) = 0;

m := n div 2;

array W dim (1:n);

array V dim (1:n);

array C dim (1:n);

for i := 1 to n

do

array C(i) dim (1:n)

od;

(* obliczanie "preprocessingu" *)

for j:= 1 to n

do

s:=0;

for i := 1 to m

do

s := A(j,2*i-1) * A(j,2*i) +s;

od;

W(j) := s;

od;

\textbf{Assertion 1:} \

Dla kazdego [math]j, 1\leq j \leq n,\qquad W_j=\sum\limits_{i=1}^{n \div 2} A_{j,2i-1}*A_{j,2i}  
[/math]

for j:= 1 to n

do

s:=0;

for i := 1 to m

do

s := B(2*i-1,j) * B(2*i,j) +s;

od;

V(j) := s;

od;

Assertion 2: Dla każdego [math]j, 1 \leq j \leq n,\qquad V_j=\sum\limits_{i=1}^{n \div 2} B_{2i-1,j}*B_{2*i,j}[/math]

(* obliczanie iloczynu macierzy *)

for i := 1 to n

do

for j := 1 to n

do

s:= 0;

for k:= 1 to m

do

s:= (A(i,2*k-1)+B(2*k,j)) * (B(2*k-1,j)+A(i,2*k)) +s;

od;

Assertion 3 [math]\forall_{1\leq i \leq n},\forall_{1\leq j \leq n}, \qquad s = \sum\limits_{k=1}^{n \div 2} (A_{i,2k-1}+B_{2k,j})*(B_{2*k-1,j}+A_{i,2k}) [/math]

C(i,j) :=s-W(i)-V(j);

Assertion 4: [math]\forall_{1\leq i \leq n},\forall_{1\leq j \leq n} \qquad C_{i,j} = \sum\limits_{k=1}^{2(n\div2)} (A_{i,k} *B_{k,j} ) [/math]

if not p

then

C(i,j) := C(i,j) + A(i,n)*B(n,j);

fi;

od;

od;

Assertion 5: \ Dla każdych wartości [math]i,j, 1\leq i \leq n, 1\leq j \leq n, \qquad C_{i,j} = \sum\limits_{k=1}^{ n } (A_{i,k} *B_{k,j} ) [/math]

end Winograd;

Dowód poprawności

Naszym zadaniem jest wykazać prawdziwość nastepującej implikacji

[math]\color{blue} \mathrm{Precondition} \Rightarrow [\mathrm{Algorytm\ Winograda}]\mathrm{Postcondition} [/math]

co się czyta tak: jeśli dane spełniają warunek wstępny to algorytm Winograda kończy obliczenia nie sygnalizując błędu i wyniki spełniają warunek końcowy.

Sprawdzenie czy warunek wstępny jest spełniony przez dane może być w części wykonane przez kompilator. Kompilator może sprawdzić czy parametry aktualne sa tablicami dwuwymiarowymi. Druga część warunku, że rozmiary tablic są równe [math]n \times n[/math] nie może być sprawdzona przed wywołaniem procedury Winograd, nie może też być udowodniona. Wobec tego wykonywanie procedury rozpoczynamy od (dynamicznego) sprawdzania kształtu i rozmiaru tablic\footnote{W loglanie'82 dwuwymiarowej tablicy możemy nadać kształt trójkatny, wstęgowy i oczywiście kształt kwadratowy}. Można rozważać czy nie dałoby się udowodnić, o programie stosującym procedurę Winograd, że warunek wstępny jest spełniony za każdym razem gdy procedura Winograd jest wywoływana w naszym programie. Ale czy można zagwarantować, że każdy program stosujący algorytm Winograda będzie sprawdzał warunek wstępny? lub go dowodził? Lepiej więc zostawić sprawdzanie warunku wstępnego procedurze Winograd. \\

Do algorytmu Winograd wstawiliśmy asercje. Mają one za zadanie:

1. umożliwić sygnalizację naruszenia warunku asercji w trakcie wykonywania programu,
2. ułatwić argumentację na rzecz tezy o poprawności algorytmu.

W tym przypadku trudno mówić o dynamiczej weryfikacji: ażeby sprawdzić warunek wyliczony w asercji trzeba powtórzyć obliczenia -- to niewiele nam daje. Ponadto, tu uwaga natury ogólnej, zamiana asercji na instrukcję warunkową

[math]\quad \mathbf{if} \ warunek \ asercji \ \mathbf{then} \ wrzuc \ wyjatek \ \mathbf{fi}[/math]

zapewnia tylko tyle, że podczas wykonywania algorytmu zostanie zasygnalizowany błąd. Nie mamy nawet gwarancji, że zdarzy się to zawsze gdy program zawiera błędy.

Natomiast asercje możemy zastąpić lematami i udowodnić je

Lemat 1 Dla każdego [math]j, 1\leq j \leq n[/math], i [math]m=n \div 2[/math] zachodzi

[math]\left \{ \color{red}K\color{black}: \begin{array}{l} \quad s:=0; \\ \quad \mathbf{for}\ i:=1\ \mathbf{to}\ m \\ \quad \mathbf{do} \\ \qquad s := A[j, 2*i-1] * A[j,2*i]+s; \\ \quad \mathbf{od} ; \\ \quad W[j]:=s; \end{array} \right \} \left (W_j=\sum\limits_{i=1}^{n \div 2} A_{j,2i-1}*A_{j,2i}\right ) [/math]

Lemat 2 Dla każdego [math]j, 1\leq j \leq n[/math], i [math]m=n \div 2[/math] zachodzi

[math] \left \{ \begin{array}{l} \quad s:=0; \\ \quad \mathbf{for}\ i:=1\ \mathbf{to}\ m \\ \quad \mathbf{do} \\ \qquad s := B[2*i-1,j] * B[2*i,j]+s; \\ \quad \mathbf{od} ; \\ \quad V[j]:=s; \end{array} \right \} \left (V_j=\sum\limits_{i=1}^{n \div 2} B_{2i-1,j}*B_{2i,j}\right ) [/math]

Kolejny lemat

Lemat 3 Dla każdych i, j

[math]\left \{ \begin{array}{l} s:= 0; \\ \mathbf{for} \ k:= 1\ \mathbf{to}\ m \\ \mathbf{do} \\ \quad s:= (A[i,2*k-1]+B[2*k,j]) * (B[2*k-1,j]+A[i,2*k]) +s; \\ \mathbf{od}; \end{array} \right \} \left (s = \sum\limits_{k=1}^{n \div 2} (A_{i,2k-1}+B_{2k,j})*(B_{2k-1,j}+A_{i,2k}) \right )[/math]

Lemat 4 Przy założeniu, że tablice A i B są macierzami kwadratowymi rozmiaru n x n i że zachodzą lematy 1 oraz 2, prawdziwa jest nastepująca formuła algorytmiczna

[math]\forall_{1\leq i \leq n},\forall_{1\leq j \leq n} \left \{ \begin{array}{l} s:= 0; \\ \mathbf{for} \ k:= 1\ \mathbf{to}\ m \\ \mathbf{do} \\ \quad s:= (A[i,2*k-1]+B[2*k,j]) \\ \quad * (B[2*k-1,j]+A[i,2*k]) +s;\\ \mathbf{od};\\ C[i,j] := s -W[i] -V[j]; \\ \end{array} \right \} \left (C_{i,j} = \sum\limits_{k=1}^{2*(n \div 2)} A_{i,k}*B_{k,j} \right )[/math]

Lemat 5 Z lematów 1 i 2 wynika, że następująca formuła jest prawdziwa

[math]\left \{ \begin{array}{l} \mathbf{for} \ i:=1\ to \ n \\ \mathbf{do} \\ \mathbf{for} \ j:=1\ to \ n \\ \mathbf{do} \\ \quad s:= 0; \\ \quad \mathbf{for} \ $k:= 1$\ \mathbf{to}\ $m$ \\ \quad \mathbf{do} \\ \quad \quad s:= (A[i,2*k-1]+B[2*k,j]) \\ \quad \qquad * (B[2*k-1,j]+A[i,2*k]) +s;\\ \quad \mathbf{od};\\ \quad C[i,j] := s -W[i] -V[j]; \\ \quad \mathbf{if} \ \mathbf{not} \ p \\ \quad \mathbf{then} \\ \quad \qquad C[i,j] :=C[i,j] + A[i,n]*B[n,j]\\ \quad \mathbf{fi}; \\ \mathbf{od} \\ \mathbf{od} \\ \end{array} \right \} \ \left (\forall_{1\leq i \leq n},\forall_{1\leq j \leq n}\ C_{i,j} = \sum\limits_{k=1}^{n} A_{i,k} *B_{k,j} \right )[/math]

Dowody lematów

Dowód lematu 1

W dowodzie wykorzystujemy następującą własność programów for:

niech napis [math]\omega(i)[/math] oznacza wyrażenie arytmetyczne (zmienna ,math>i</math> może, ale nie musi, w nim wystepować) [math]\left \{ \begin{array}{l} s := 0\\ \mathbf{for}\ i:= 1\ \mathbf{to}\ n \\ \mathbf{do} \\ \quad s := \omega(i) +s \\ \mathbf{od} \end{array} \right \}\left (s =\sum\limits_{i=0}^{n} \omega(i) \right ) [/math]

Pozostaje skorzystać z aksjomatu instrukcji przypisania [math]\left (s =\sum\limits_{i=0}^{n} \omega(i) \right )\implies \{ W[j] := s \}\left (W(j) =\sum\limits_{i=0}^{n} \omega(i) \right ) [/math]

Dowody lematów 2 i 3 przebiegają podobnie.

Dowód lematu 4

Należy udowodnić

[math](s = \sum\limits_{k=1}^{n \div 2} (A_{i,2k-1}+B_{2k,j})*(B_{2*k-1,j}+A_{i,2k})\implies (s-W[i]-V[j]=\sum\limits_{k=1}^{2(n \div 2)} A_{i,k}*B_{k,j}) [/math]

Rozwińmy mnożenie i zastosujmy rozdzielność mnożenia względem dodawania

[math]\begin{array}{l} \sum\limits_{k=1}^{n \div 2} (A_{i,2k-1}+B_{2k,j})*(B_{2*k-1,j}+A_{i,2k}) \\ \quad = \sum\limits_{k=1}^{n \div 2} [A_{i,2k-1}*B_{2*k-1,j}+ A_{i,2k-1}*A_{i,2k}+ B_{2k,j}*B_{2k-1,j}+ B_{2k,j}*A_{i,2k} ] \\ \quad = \sum\limits_{k=1}^{n \div 2} A_{i,2k-1}*B_{2*k-1,j}+ \sum\limits_{k=1}^{n \div 2} A_{i,2k-1}*A_{i,2k}+ \sum\limits_{k=1}^{n \div 2} B_{2k,j}*B_{2k-1,j}+ \sum\limits_{=1}^{n \div 2} B_{2k,j}*A_{i,2k} \\ \end{array} [/math]

Skorzystamy z lematów 1 oraz 2

[math] \sum\limits_{k=1}^{n \div 2} (A_{i,2k-1}+B_{2k,j})*(B_{2*k-1,j}+A_{i,2k})-W[i]-V[j]= \sum\limits_{k=1}^{n \div 2} A_{i,2k-1}*B_{2*k-1,j}+ \sum\limits_{k=1}^{n \div 2} B_{2k,j}*A_{i,2k} [/math]

Wykorzystujemy przemienność mnożenia i łączność dodawania

[math] \sum\limits_{k=1}^{n \div 2} A_{i,2k-1}*B_{2*k-1,j}+ \sum\limits_{k=1}^{n \div 2} B_{2k,j}*A_{i,2k}= \sum\limits_{k=1}^{2(n \div 2)} A_{i,k}*B_{k,j} [/math]

Dowód lematu 5

Trzeba wykazać, że

[math](s= \sum\limits_{k=1}^{2(n \div 2)} A_{i,k}*B_{k,j} )\implies \left \{ \begin{array}{l} \mathbf{if} \ \mathbf{not} \ p \\ \mathbf{then} \\ \qquad C[i,j] :=C[i,j] + A[i,n]*B[n,j]\\ \mathbf{fi}; \end{array} \right \}(s= \sum\limits_{k=1}^{n} A_{i,k}*B_{k,j} ) [/math]

Pamiętamy, że p= (n mod 2 =0). Jeżeli n jest liczbą parzystą to [math]2(n \div 2)=n[/math].

[math]C_{i,j} = \sum\limits_{k=1}^{n} A_{i,k} *B_{k,j} [/math]

W przeciwnym przypadku (tzn. gdy not p) sumowanie zakończyło się dla </math>k=n-1</math>. Trzeba więc dodać wartość [math]A[i,n]*B[n,j][/math] c.b.d.o

Uwagi końcowe

Zauważ, że udowodniliśmy twierdzenie o poprawności całej klasy algorytmów.

algorytm ten pozwala mnożyć macierze liczb zespolonych, ... Zmieńmy nagłówek procedury

unit Winograd_Generic: procedure( type T, function add(x,y:T):T, function mult(x,y:T):T,

function subt(x,y:T):T, A, B: array_of array_of' T, output C: array_of array_of T);

i odpowiednio w treści procedury zapiszmy add(u,v) zamiast u+v, mult(u,v) zmiast u*v, subt(u,v) zamiast u-v.,

Nasz warunek wstępny przybiera teraz inną postać

Precondition: Argumenty procedury Winograd_Generic spełniają następujące warunki

1. pierwszy argument jest nazwą klasy,
2. kolejne trzy argumenty są nazwami funkcji, dwuargumentowych ze zbioru |T| obiektów typu T w zbiór |T|,
3. następne dwa argumenty to nazwy tablic kwadratowych jednakowego rozmiaru n x n,
4. ostatni argument także jest nazwą tablicy, tablica ta zostanie przekazana wywołującemu

procedurę Winograd\_Generic,

1. zbiór |T| obiektów klasy T wraz z operacjami add, mult i subt jest pierścieniem.

Postcondition: Algorytm zwraca tablicę C obiektów typu T, taką, że dla każdych [math]i,j, \ 1\leq i \leq n, 1 \leq j \leq n[/math]

[math] C_{i,j}= \sum\limits_{k=0}^{n}\ mult(A_{i,k}, B_{k,j}) [/math]

znak [math]\sum [/math] odnosi się do wykonywania operacji [math]add[/math].

Można algorytm zapisać jeszcze inaczej, w zasiegu deklaracji typu (klasy) T, a jeszcze lepiej w zasiegu interfejsu Pierscien. Wtedy nagłówki obu procedur będą identyczne.

NAPISZ TO!

unit ring: class

unit virtual add: function(x: ring):ring;

unit virtual sub: function(x: ring):ring;

unit virtual mult: function(x: ring): ring;

unit virtual zero: function(): ring;

unit virtual zero: function(): ring;

(* AXIOMS of ring *)

tu wpisać aksjomaty pierścieni

endring

unit rngeWinograd: extends ring class;

unit Winograd: procedure(A, B: arrayof arrayof ring, output C: arrayof arrayof ring);

{* tu treść procedury *)

end Winograd

end rngeWinograd;

Komentarz