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

Z Lem
Skocz do: nawigacji, wyszukiwania
(Uwagi końcowe)
(Uwagi końcowe)
 
(Nie pokazano 12 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 30: Linia 30:
 
'''unit''' Winograd: procedure(A,B: arrayof arrayof real;
 
'''unit''' Winograd: procedure(A,B: arrayof arrayof real;
 
output C: arrayof arrayof real);
 
output C: arrayof arrayof real);
+
::::<span style="color: blue">'''Precondition''': A i B są macierzami dwuwymiarowymi o tym samym rozmiarze ''n x n''
 +
</span>
 +
::::<span style="color: blue">'''Postcondition''': macierz C jest produktem macierzy A i B, C=A x B
 +
</span>
 
::  '''var''' i,j,k,n,m: integer, W,V: '''arrayof''' real,
 
::  '''var''' i,j,k,n,m: integer, W,V: '''arrayof''' real,
 
::      p: boolean,
 
::      p: boolean,
Linia 73: Linia 76:
 
:od;
 
:od;
  
:::::  '''Assertion 1''': Dla każdego <math>\color{blue} j, 1\leq j \leq n,\qquad W_j=\sum\limits_{i=1}^{n \div 2} A_{j,2i-1}*A_{j,2i}   
+
:::::  <span style="color: blue">'''Assertion 1''': Dla każdego </span><math>\color{blue} j, 1\leq j \leq n,\qquad W_j=\sum\limits_{i=1}^{n \div 2} A_{j,2i-1}*A_{j,2i}   
 
</math>
 
</math>
  
Linia 87: Linia 90:
 
:od;
 
:od;
  
:::::'''Assertion 2:''' Dla każdego <math>\color{blue} 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>
+
:::::<span style="color: blue">'''Assertion 2:''' Dla każdego </span><math>\color{blue} 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 *)
 
:(* obliczanie iloczynu macierzy *)
Linia 100: Linia 103:
 
:::    od;
 
:::    od;
  
:::::'''Assertion 3'''  <math>\color{blue} \forall_{1\leq i \leq n},\forall_{1\leq j \leq n}, \qquad
+
:::::<span style="color: blue">'''Assertion 3'''  </span><math>\color{blue} \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>
 
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);
 
:::    C(i,j) :=s-W(i)-V(j);
  
:::::'''Assertion 4:''' <math>\color{blue} \forall_{1\leq i \leq n},\forall_{1\leq j \leq n} \qquad
+
:::::<span style="color: blue">'''Assertion 4:''' </span><math>\color{blue} \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>
 
  C_{i,j} = \sum\limits_{k=1}^{2(n\div2)} (A_{i,k} *B_{k,j} ) </math>
  
Linia 116: Linia 119:
 
:'''od''';   
 
:'''od''';   
  
:::::'''Assertion 5''':    Dla każdych wartości <math>\color{blue} i,j, 1\leq i \leq n, 1\leq j \leq n,
+
:::::<span style="color: blue">'''Assertion 5''':    Dla każdych wartości</span> <math>\color{blue} 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>
 
\qquad C_{i,j} = \sum\limits_{k=1}^{ n } (A_{i,k} *B_{k,j} ) </math>
 
      
 
      
Linia 126: Linia 129:
 
Naszym zadaniem jest wykazać prawdziwość następującej implikacji
 
Naszym zadaniem jest wykazać prawdziwość następującej implikacji
  
:::: <math>\color{blue} \mathrm{Precondition} \Rightarrow \mathbf{[}\mathrm{Algorytm\ Winograda}\mathbf{]}\mathrm{Postcondition</math>  
+
:::: <span style=color:blue> '''Precondition''' <math>\Rightarrow </math> [Algorytm_Winograda]'''Postcondition''' </span>
  
 
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''.
 
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.
 
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<ref>W loglanie'82 dwuwymiarowej tablicy możemy nadać kształt trójkątny, wstęgowy i oczywiście kształt kwadratowy</ref>.  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. \\
+
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<ref>W loglanie'82 dwuwymiarowej tablicy możemy nadać kształt trójkątny, wstęgowy i oczywiście kształt kwadratowy</ref>.  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:
+
Do algorytmu Winograd wstawiliśmy asercje. Podstawowa koncepcja asercji jest taka: ''ilekroć podczas wykonywania programu dochodzimy do miejsca wystąpienia asercji, to bieżący stan pamięci spełnia warunek asercji''. To jest tylko postulat, hipoteza. Jak taki postulat sprawdzić? Nie istnieje ogólna metoda, którą można by np. wbudować do kompilatora.
 +
 
 +
Przyjmuje się więc, że asercje mają za zadanie:
 
# umożliwić sygnalizację naruszenia warunku asercji w trakcie wykonywania programu,
 
# umożliwić sygnalizację naruszenia warunku asercji w trakcie wykonywania programu,
 
# ułatwić argumentację na rzecz  tezy o poprawności algorytmu.
 
# ułatwić argumentację na rzecz  tezy o poprawności algorytmu.
W tym przypadku trudno mówić o dynamicznej 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ą
+
W naszym przypadku trudno mówić o dynamicznej weryfikacji: ażeby sprawdzić warunek wyliczony w asercji trzeba powtórzyć obliczenia -- a 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>
+
:::'''if''' '''not'''(warunek asercji) '''then'''   wrzuć wyjątek '''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.  
+
zapewnia tylko tyle, że podczas wykonywania algorytmu może zostać  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
+
Proponujemy by asercje zastąpić lematami i udowodnić je, statycznie, raz na zawsze.
  
 
'''Lemat''' 1  
 
'''Lemat''' 1  
Linia 218: Linia 223:
 
  \mathbf{do} \\
 
  \mathbf{do} \\
 
  \quad s:= 0; \\
 
  \quad s:= 0; \\
  \quad    \mathbf{for} \ $k:= 1$\ \mathbf{to}\ $m$ \\
+
  \quad    \mathbf{for} \ k:= 1\ \mathbf{to}\ m \\
 
  \quad    \mathbf{do} \\
 
  \quad    \mathbf{do} \\
 
  \quad    \quad s:= (A[i,2*k-1]+B[2*k,j]) \\
 
  \quad    \quad s:= (A[i,2*k-1]+B[2*k,j]) \\
Linia 238: Linia 243:
 
W dowodzie wykorzystujemy następującą własność programów '''for''':  
 
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ć)
+
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}
 
:::<math>\left \{ \begin{array}{l}
 
             s := 0\\
 
             s := 0\\
Linia 250: Linia 255:
 
Pozostaje skorzystać z aksjomatu instrukcji przypisania
 
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>\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>
 
   </math>
  
Linia 297: Linia 302:
 
\end{array} \right \}(s= \sum\limits_{k=1}^{n} A_{i,k}*B_{k,j} )  </math>
 
\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>.
+
Pamiętamy, że p= (n mod 2 =0). Jeżeli n jest liczbą parzystą to <math>2(n \div 2)=n</math> i obliczona wartość <math>C_{i,j}</math> jest poprawna.
 +
W przypadku gdy n jest liczbą nieparzystą, tzn. gdy '''not''' p, wartością wyrażenia <math>2*(n \div 2)</math> jest <math>n-1</math>. Po wykonaniu instrukcji '''if''' '''not''' p ...
  
 +
zachodzi
 +
 
<math>C_{i,j} =  
 
<math>C_{i,j} =  
 
\sum\limits_{k=1}^{n} A_{i,k} *B_{k,j}  </math>
 
\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>.
+
::::::::::c.b.d.o
Trzeba więc dodać wartość <math>A[i,n]*B[n,j]</math>
+
c.b.d.o
+
  
 
== Uwagi końcowe ==
 
== Uwagi końcowe ==
Linia 310: Linia 316:
 
Zauważ, że udowodniliśmy twierdzenie o poprawności całej klasy algorytmów.
 
Zauważ, że udowodniliśmy twierdzenie o poprawności całej klasy algorytmów.
  
algorytm ten pozwala mnożyć macierze liczb zespolonych, ...
+
algorytm ten pozwala mnożyć macierze liczb zespolonych, macierzy, których elementami są macierze, macierzy wielomianów, ...
 
Zmieńmy nagłówek procedury
 
Zmieńmy nagłówek procedury
  
Linia 325: Linia 331:
 
# kolejne trzy argumenty są nazwami funkcji, dwuargumentowych ze zbioru |T| obiektów typu T w zbiór |T|,
 
# kolejne trzy argumenty są nazwami funkcji, dwuargumentowych ze zbioru |T| obiektów typu T w zbiór |T|,
 
# następne dwa argumenty to nazwy tablic kwadratowych jednakowego rozmiaru n x n,
 
# następne dwa argumenty to nazwy tablic kwadratowych jednakowego rozmiaru n x n,
# ostatni argument także jest nazwą tablicy, tablica ta zostanie przekazana wywołującemu  
+
# ostatni argument także jest nazwą tablicy, tablica ta zostanie przekazana wywołującemu procedurę Winograd_Generic,
procedurę Winograd\_Generic,
+
 
# zbiór |T| obiektów klasy T wraz z operacjami add, mult i subt jest ''pierścieniem''.
 
# zbiór |T| obiektów klasy T wraz z operacjami add, mult i subt jest ''pierścieniem''.
  
Linia 332: Linia 337:
 
'''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>
 
'''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>
+
:::::<math> C_{i,j}= \sum\limits_{k=0}^{n}\ A_{i,k}.mult (B_{k,j}) </math>
  
znak <math>\sum </math> odnosi się do wykonywania operacji <math>add</math>.
+
System TeX wymusił na mnie zastosowanie znaku  <math>\sum </math> chociaż wolałbym w tym miejscu znak 'add',  <math>add</math>.
  
Można algorytm  zapisać jeszcze inaczej, w zasiegu deklaracji typu (klasy) T, a jeszcze lepiej w zasiegu interfejsu Pierscien.
+
Można algorytm  zapisać jeszcze inaczej, w zasięgu deklaracji typu (klasy) T, a jeszcze lepiej w zasięgu interfejsu Pierscien.
 
Wtedy nagłówki obu procedur będą identyczne.  
 
Wtedy nagłówki obu procedur będą identyczne.  
  
NAPISZ TO!
 
  
 
'''unit''' ring: '''class'''
 
'''unit''' ring: '''class'''
Linia 346: Linia 350:
 
::'''unit virtual''' mult: '''function'''(x: ring): ring;
 
::'''unit virtual''' mult: '''function'''(x: ring): ring;
 
::'''unit virtual''' zero: '''function'''(): ring;
 
::'''unit virtual''' zero: '''function'''(): ring;
::'''unit virtual''' zero: '''function'''(): ring;
+
::'''unit virtual''' one: '''function'''(): ring;
 
::(* AXIOMS of ring *)
 
::(* AXIOMS of ring *)
 
:::tu wpisać aksjomaty pierścieni
 
:::tu wpisać aksjomaty pierścieni
Linia 361: Linia 365:
  
 
Zastosowanie algorytmu Winograda w pewnym pierścieniu P wymaga  
 
Zastosowanie algorytmu Winograda w pewnym pierścieniu P wymaga  
# rozszerzenia tej klasy i zadeklarowania odpowiednich metod: add, sub, mult,
+
# rozszerzenia tej klasy i zadeklarowania odpowiednich metod: add, sub, mult,np.
 +
:::'''unit''' MM: '''extends''' rngeWinograd '''class''';
 
# stworzenia i wypełnienia tablic A i B,
 
# stworzenia i wypełnienia tablic A i B,
 
# wywołania procedury Winograd.
 
# wywołania procedury Winograd.
 +
 +
== Zobacz też ==
 +
* [[pierścień ]]
 +
 +
{{Uwagi}}
 +
 +
{{Przypisy}}
 +
<references/>

Aktualna wersja na dzień 18:18, 27 lis 2015

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

Precondition: A i B są macierzami dwuwymiarowymi o tym samym rozmiarze n x n

Postcondition: macierz C jest produktem macierzy A i B, C=A x B

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;
Assertion 1: Dla każdego [math]\color{blue} 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]\color{blue} 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]\color{blue} \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]\color{blue} \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]\color{blue} 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ść następującej implikacji

Precondition [math]\Rightarrow [/math] [Algorytm_Winograda]Postcondition

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[1]. 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. Podstawowa koncepcja asercji jest taka: ilekroć podczas wykonywania programu dochodzimy do miejsca wystąpienia asercji, to bieżący stan pamięci spełnia warunek asercji. To jest tylko postulat, hipoteza. Jak taki postulat sprawdzić? Nie istnieje ogólna metoda, którą można by np. wbudować do kompilatora.

Przyjmuje się więc, że asercje mają 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 naszym przypadku trudno mówić o dynamicznej weryfikacji: ażeby sprawdzić warunek wyliczony w asercji trzeba powtórzyć obliczenia -- a to niewiele nam daje. Ponadto, tu uwaga natury ogólnej, zamiana asercji na instrukcję warunkową

if not(warunek asercji) then wrzuć wyjątek fi

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

Proponujemy by asercje zastąpić lematami i udowodnić je, statycznie, raz na zawsze.

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] i obliczona wartość [math]C_{i,j}[/math] jest poprawna. W przypadku gdy n jest liczbą nieparzystą, tzn. gdy not p, wartością wyrażenia [math]2*(n \div 2)[/math] jest [math]n-1[/math]. Po wykonaniu instrukcji if not p ...

zachodzi

[math]C_{i,j} = \sum\limits_{k=1}^{n} A_{i,k} *B_{k,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, macierzy, których elementami są macierze, macierzy wielomianów, ... 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,
  5. 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}\ A_{i,k}.mult (B_{k,j}) [/math]

System TeX wymusił na mnie zastosowanie znaku [math]\sum [/math] chociaż wolałbym w tym miejscu znak 'add', [math]add[/math].

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


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 one: 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

Zastosowanie algorytmu Winograda w pewnym pierścieniu P wymaga

  1. rozszerzenia tej klasy i zadeklarowania odpowiednich metod: add, sub, mult,np.
unit MM: extends rngeWinograd class;
  1. stworzenia i wypełnienia tablic A i B,
  2. wywołania procedury Winograd.

Zobacz też

Uwagi

Przypisy

  1. W loglanie'82 dwuwymiarowej tablicy możemy nadać kształt trójkątny, wstęgowy i oczywiście kształt kwadratowy