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

Wersja z 09:06, 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.

\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;

[math]\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}