SpecVer/Winograd - Historia wersji

AndrzejSalwicki: /* Uwagi końcowe */

2015-11-27T17:18:19Z

‎Uwagi końcowe

AndrzejSalwicki: /* Dowód poprawności */

2013-02-13T18:04:49Z

‎Dowód poprawności

AndrzejSalwicki: /* Uwagi końcowe */

2013-02-13T16:11:57Z

‎Uwagi końcowe

AndrzejSalwicki: /* Dowód poprawności */

2013-02-13T15:06:46Z

‎Dowód poprawności

AndrzejSalwicki: /* Uwagi końcowe */

2013-02-13T10:51:36Z

‎Uwagi końcowe

AndrzejSalwicki: /* Dowód lematu 5 */

2013-02-13T10:42:13Z

‎Dowód lematu 5

AndrzejSalwicki: /* Dowód lematu 5 */

2013-02-13T10:41:39Z

‎Dowód lematu 5

AndrzejSalwicki: /* Dowód lematu 5 */

2013-02-13T10:40:10Z

‎Dowód lematu 5

AndrzejSalwicki: /* Dowód lematu 1 */

2013-02-13T07:55:48Z

‎Dowód lematu 1

AndrzejSalwicki: /* Dowód lematu 1 */

2013-02-13T07:54:08Z

‎Dowód lematu 1

@@ Linia 316: / Linia 316: @@
 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
@@ Linia 350: / Linia 350: @@
 ::'''unit virtual''' mult: '''function'''(x: ring): ring;
 ::'''unit virtual''' zero: '''function'''(): ring;
-::'''unit virtual''' zero: '''function'''(): ring;
+::'''unit virtual''' one: '''function'''(): ring;
 ::(* AXIOMS of ring *)
 :::tu wpisać aksjomaty pierścieni

@@ Linia 223: / Linia 223: @@
   \mathbf{do} \\
   \quad s:= 0; \\
-  \quad     \mathbf{for} \ $k:= 1$\ \mathbf{to}\ $m$ \\
+  \quad     \mathbf{for} \ k:= 1\ \mathbf{to}\ m \\
   \quad     \mathbf{do} \\
   \quad     \quad s:= (A[i,2*k-1]+B[2*k,j]) \\

@@ Linia 339: / Linia 339: @@
 :::::<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 zasięgu deklaracji typu (klasy) T, a jeszcze lepiej w zasięgu interfejsu Pierscien.

@@ Linia 134: / Linia 134: @@
 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.
 # umożliwić sygnalizację naruszenia warunku asercji w trakcie wykonywania programu,
 # 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

← poprzednia wersja		Wersja z 10:51, 13 lut 2013
Linia 367:		Linia 367:
	# 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/>

@@ Linia 308: / Linia 308: @@
 \sum\limits_{k=1}^{n} A_{i,k} *B_{k,j}  </math>
-:::::::::::::::::::::::::::::c.b.d.o
+::::::::::c.b.d.o
 == Uwagi końcowe ==

@@ Linia 300: / Linia 300: @@
 \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.
 <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>.
+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

@@ Linia 253: / Linia 253: @@
 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>

@@ Linia 241: / Linia 241: @@
 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}
              s := 0\\