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

Wersja z 17:11, 13 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);

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, ... 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 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

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ż

• pierścień

Uwagi

Przypisy