SpecVer/Winograd
Spis treści
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. [math] \begin{algorithmic}[1] \STATE $\mathbf{signal}\ Niezgoda;$ \STATE $\mathbf{unit}\ Winograd:\ \mathbf{procedure}(A,B: \mathbf{array\_of\ array\_of}\ real;\ \ \mathbf{output}\ C: \mathbf{array\_of\ array\_of}\ real);$ \REQUIRE wymagaj by A i B były macierzami kwadratowymi rozmiaru n x n \ENSURE zapewnij, że obliczona macierz C jest produktem macierzy A i B, C = A * B \STATE $\mathbf{var}\ i,j,k,n,m: \mathbf{integer},\ W,V: \mathbf{array\_of\ real}, p: \mathbf{boolean}, s: \mathbf{real}; $ \STATE $\mathbf{begin}$ \\ \COMMENT{ \textit{ustalić czy macierze mogą być mnożone tzn. czy ilość wierszy w A = ilosc kolumn w B?} } \\ \COMMENT{ \textit{ustalić czy n jest parzyste?} } \\ \COMMENT{\textit{ obliczyc preprocessing} } \\ \hrulefill \COMMENT{ dynamiczne sprawdzanie precondition } \IF {lower(A) $\neq$ lower(B)\ \OR\ lower(A)$\neq$ 1\ \OR\ upper(A)$\neq$ upper(B)\ } \STATE $raise\ Niezgoda$ \FI; \STATE i := upper(A); \STATE j := lower(A); \STATE n := i-j+1; \FOR {$l : = j$ \TO $i$ } \IF {lower(A(l)) $\neq$ lower(B(l))\ \OR\ lower(A(l))$\neq$ 1\ \OR\ upper(A(l))$\neq$ upper(B(l) \OR upper(A(l)$\neq$upper(A)} \STATE raise Niezgoda \FI; \OD; \ASSERTION sprawdzono: macierze są kwadratowe, rozmiaru n x n \\ \hrulefill \COMMENT { można mnożyć } \\ %\STATE $n := k+1;$ \STATE $p := (n\ mod\ 2) = 0;$ % (* p = n jest parzyste? *) \STATE $m := n\ div\ 2;$ \STATE $\mathbf{array}\ W\ \mathbf{dim} (1:n);$ \STATE $\mathbf{array}\ V\ \mathbf{dim} (1:n);$ \STATE $ \mathbf{array} \ C\ \mathbf{dim} (1:n);$ \FOR { i := 1 to n} %do \STATE $ \mathbf{array}\ C(i)\ \mathbf{dim} (1:n)$ \OD; \\ \hrulefill \\ %\begin{verbatim} \COMMENT { obliczanie "preprocessingu" } \FOR { j:= 1 to n} %do \STATE s:=0; \FOR {i := 1 to m } % do \STATE $ s := A[j,2*i-1] * A[j,2*i] +s;$ \OD; %od; \STATE W[j] := s; \OD; %od; \ltmath\gt\fbox{ \textbf{Assertion 1:} \ Dla każdego $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 \STATE s:=0;
\FOR {i := 1 to m }
%do
\STATE { s := B[2*i-1,j] * B[2*i,j] +s; }
\OD; %od; \STATE V[j] := s;
\OD;
\fbox {\textbf{Assertion 2:} \ \ Dla każdego $j, 1 \leq j \leq n,\qquad V_j=\sum\limits_{i=1}^{n \div 2} B_{2i-1,j}*B_{2*i,j}$ } \bigskip \\ \hrulefill
\COMMENT {obliczanie iloczynu macierzy } \FOR {$i := 1$ to $n$} %\COMMENT { dla każdego 1$\leq$ i $\leq$ n }
%do
\FOR {$j := 1$ to $n$} %{* dla każdego $1\leq j \leq n$ }
%do
\STATE s:= 0;
\FOR {$k:= 1$ to $m$}
% do
\STATE s:= (A[i,2*k-1]+B[2*k,j]) * (B[2*k-1,j]+A[i,2*k]) +s;
\OD; \\
\fbox{\textbf{Assertion 3:} \
$\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}) $ }
\STATE $ C[i,j] :=s-W[i]-V[j];$
\fbox{\textbf{Assertion 4:}\ $\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} ) $}
\IF {\NOT p}
%then
\STATE $C[i,j] := C[i,j] + A[i,n]*B[n,j];$
\COMMENT { poprawiamy - gdy n jest nieparzyste }
\FI; \\
\OD; \{ j \}
\OD; \{ i \} \\ \fbox{\textbf{Assertion 5:} \ Dla każdych wartości $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} ) $} \\ \STATE $\mathbf{end} Winograd;$ \end{algorithmic} </math>
Dowód poprawności
Naszym zadaniem jest wykazać nastepującą implikację [math]\[\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. \\
\noindent Do algorytmu Winograd wstawiliśmy asercje. Mają one za zadanie: \begin{enumerate}
\item umożliwić sygnalizację naruszenia warunku asercji w trakcie wykonywania programu,
\item ułatwić argumentację na rzecz tezy o poprawności algorytmu. \end{enumerate} 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ą\\ \[ \mathbf{if}\ warunek\_ asercji\ \mathbf{then}\ \mbox{wrzuć\_ wyjątek}\ \mathbf{fi} \] 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. \\
\noindent Natomiast asercje możemy zastąpić lematami i udowodnić je \begin{lemat} Dla każdego $j, 1\leq j \leq n$, i $m=n \div 2$ zachodzi \[K: \left \{ \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 ) \]
\end{lemat}
\begin{lemat} Dla każdego $j, 1\leq j \leq n$, i $m=n \div 2$ zachodzi \[ \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 ) \]
\end{lemat} Kolejny lemat \begin{lemat} $\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]) \\
\qquad * (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 )$
\end{lemat} \begin{lemat} \quad \\ 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 \medskip \\ \[\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]) \\
\qquad * (B[2*k-1,j]+A[i,2*k]) +s;\\
\mathbf{od};\\
C[i,j] := s -W[i] -V[j]; \\
\end{array} \right \} \left (s = \sum\limits_{k=1}^{2*(n \div 2)} A_{i,k}*B_{k,j} \right )\]
\end{lemat} \newpage \begin{lemat}\quad \\
Z prawdziwości lematów 1 i 2 wynika, że następująca formuła jest prawdziwa \medskip \\
$\left \{ \begin{array}{l} \mathbf{for} \ i:=1\ to \ n \\ \mathbf{do} \\ \quad \mathbf{for} \ j:=1\ to \ n \\ \quad \mathbf{do} \\ \quad \quad s:= 0; \\ \quad \quad \mathbf{for} \ $k:= 1$\ \mathbf{to}\ $m$ \\ \quad \quad \mathbf{do} \\ \quad \quad \quad s:= (A[i,2*k-1]+B[2*k,j]) \\ \quad \quad \qquad * (B[2*k-1,j]+A[i,2*k]) +s;\\ \quad \quad \mathbf{od};\\ \quad \quad C[i,j] := s -W[i] -V[j]; \\ \quad \quad \mathbf{if} \ \mathbf{not} \ p \\ \quad \quad \mathbf{then} \\ \quad \quad \qquad C[i,j] :=C[i,j] + A[i,n]*B[n,j]\\ \quad \quad \mathbf{fi}; \\ \quad \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 )$
\end{lemat}
\section{Dowody lematów} \subsection{Dowód lematu 1} W dowodzie wykorzystujemy następującą własność programów \textbf{for}: \\ niech napis $\omega(i)$ oznacza wyrażenie arytmetyczne (zmienna $i$ może, ale nie musi, w nim wystepować) \[\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 ) \] Pozostaje skorzystać z aksjomatu instrukcji przypisania \[\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 ) \] \begin{flushright} $\Box$ \end{flushright} Dowody lematów 2 i 3 przebiegają podobnie. \subsection{Dowód lematu 4} Należy udowodnić \[(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}) \] Rozwińmy mnożenie i zastosujmy rozdzielność mnożenia wzgledem dodawania \[\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} \] Skorzystamy z lematów 1 oraz 2 \[ \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} A_{i,2k-1}*A_{i,2k}+ %\sum\limits_{k=1}^{n \div 2} B_{2k,j}*B_{2*k,j}+ \sum\limits_{k=1}^{n \div 2} B_{2k,j}*A_{i,2k} \] Wykorzystujemy przemienność mnożenia i łączność dodawania \[ \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_{2*k,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} %+
%\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_{2*k,j}+ %\sum\limits_{k=1}^{n \div 2} B_{2k,j}*A_{i,2k} \] \cbdo \subsection{Dowód lematu 5} Trzeba wykazać, że \[(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} ) \] Pamiętamy, że p= (n mod 2 =0). Jeżeli n jest liczbą parzystą to $2(n \div 2)=n$. \[C_{i,j} = \sum\limits_{k=1}^{n} A_{i,k} *B_{k,j} \] W przeciwnym przypadku (tzn. gdy \textbf{not} $p$) sumowanie zakonczyło się dla $k=n-1$. Trzeba więc dodać wartość $A[i,n]*B[n,j]$ \cbdo \hrulefill \\
