SpecVer/IloczynSkalarny - Historia wersji

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

2015-11-26T12:58:44Z

‎Dowód poprawności

AndrzejSalwicki: /* Narzędzia */

2015-11-26T12:55:45Z

‎Narzędzia

AndrzejSalwicki: /* Algorytm */

2015-11-26T12:04:37Z

‎Algorytm

AndrzejSalwicki: /* Algorytm */

2015-11-26T12:02:08Z

‎Algorytm

AndrzejSalwicki: /* Narzędzia */

2015-11-26T11:40:38Z

‎Narzędzia

AndrzejSalwicki: /* Narzędzia */

2015-11-26T11:39:55Z

‎Narzędzia

AndrzejSalwicki: /* Narzędzia */

2015-11-26T11:38:13Z

‎Narzędzia

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

2015-11-26T11:30:32Z

‎Dowód poprawności

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

2015-11-26T11:25:03Z

‎Dowód poprawności

AndrzejSalwicki: Anulowanie wersji nr 1268 utworzonej przez AndrzejSalwicki (dyskusja)

2014-03-20T11:05:21Z

Anulowanie wersji nr 1268 utworzonej przez AndrzejSalwicki (dyskusja)

@@ Linia 54: / Linia 54: @@
 \begin{array}{l} s:=0; \\ \mathbf{for}\ i\ :=\ lower(A)\ \mathbf{to}\ upper(A)\ \mathbf{do}\ s\ :=\ s+A[i] * B[i]\ \mathbf{od} \end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{upper(A)}A_i * B_i \right)</math>
-Dowód przebiega przez indukcję ze względu na wielkość długość tablic tzn. wielkość upper(A)-lower(A).
+Dowód przebiega przez indukcję ze względu na długość  tablic tzn. wielkość ''upper(A)-lower(A)''.
-(''Podstawa indukcji'') Gdy lower(A)=upper(A) to należy udowodnić
+(''Podstawa indukcji'') Gdy ''lower(A)=upper(A)'' to należy udowodnić
 <math> \alpha \Rightarrow \left [
@@ Linia 90: / Linia 90: @@
 Wszystkie kroki polegały na przejściu od formuły do formuły jej równoważnej. W ten sposób udowodniliśmy bazę indukcji.
-(''Krok indukcji'') Załóżmy, że nasza formuła jest prawdziwa dla <math>n=upper(A)-lower(A)</math> i zbadajmy prawdziwość formuły dla n+1.
+(''Krok indukcji'') Załóżmy, że nasza formuła jest prawdziwa dla <math>n=upper(A)-lower(A)</math> i zbadajmy prawdziwość formuły dla ''n+1''.
 <math> \alpha \Rightarrow \left [

@@ Linia 42: / Linia 42: @@
 :::<math>\color{blue}\alpha(x/\tau)\equiv[x := \tau]\alpha   </math>
-gdzie typ(x) = typ(<math>\tau</math>), wyrażenie <math>\alpha</math> jest formułą, a wyrażenie <math>\alpha(x/\tau)</math> powstaje z formuły <math>\alpha</math> przez równoczesne zastapienie wszystkich wolnych wystąpień zmiennej <math>x</math> przez <math>\tau</math>.
+gdzie typy zmiennej <math>x</math> i wyrażenia <math>\tau</math> są zgodne, typ(x) = typ(<math>\tau</math>), wyrażenie <math>\alpha</math> jest formułą, a wyrażenie <math>\alpha(x/\tau)</math> powstaje z formuły <math>\alpha</math> przez równoczesne zastapienie wszystkich wolnych wystąpień zmiennej <math>x</math> przez wyrażenie  <math>\tau</math>.
 == Dowód poprawności ==

@@ Linia 10: / Linia 10: @@
 :'''array''' A '''dim''' (1:n);
 : (* wypełnij tablice A oraz B np.*)
-:'''for''' i := 1 '''to''' n '''do''' A[i]:= ??; B[i]:=?? '''od''';
+:'''for''' i := 1 '''to''' n '''do''' read(A[i]);  readln(B[i]) '''od''';
 :(* --------------------------------- *)
 :s:=0;

@@ Linia 1: / Linia 1: @@
 == Algorytm ==
-program Iloczyn_skalarny;
+'''program''' Iloczyn_skalarny;
-: var n: integer,
+: '''var''' n: integer,
 ::s: real,
-::A, B: arrayof real;
+::A, B: '''arrayof''' real;
-begin
+'''begin'''
 :(* pobierz wartość n i utwórz tablice A i B  *)
 :readln(n);
-:array A dim (1:n);
+:'''array''' A '''dim''' (1:n);
-:array A dim (1:n);
+:'''array''' A '''dim''' (1:n);
 : (* wypełnij tablice A oraz B np.*)
-:for i := 1 to n do A[i]:= ??; B[i]:=?? od;
+:'''for''' i := 1 '''to''' n '''do''' A[i]:= ??; B[i]:=?? '''od''';
 :(* --------------------------------- *)
 :s:=0;
-:for i := 1 to n do
+:'''for''' i := 1 '''to''' n '''do'''
 ::s := s+ A[i]*B[i]
-:od;
+:'''od''';
 :(* --------------------------------- *)
 :(* wydrukuj wynik *)
 :writeln(s)
-end
+'''end'''
 == Narzędzia ==

@@ Linia 34: / Linia 34: @@
 <math>   \begin{array}{l}
 (s1)\ \sum\limits_1^0 \omega(i) = 0 \\
-(s2)\  \sum\limits_1^1 \omega(i) = \omega(i/1)   \mbox{w wyrażeniu }\omega \mbox{ wszystkie wystąpienia zmiennej i zastąp liczbą 1}\\
+(s2)\  \sum\limits_1^1 \omega(i) = \omega(i/1)   \qquad \mbox{w wyrażeniu }\omega \mbox{ wszystkie wystąpienia zmiennej i zastąp liczbą 1}\\
-(s3)\  \sum\limits_1^{n+1} \omega(i) = \sum\limits_1^{n} \omega(i) +\omega(i/n+1)   \mbox{w wyrażeniu }\omega \mbox{ wszystkie wystąpienia zmiennej i zastąp przez } n+1
+(s3)\  \sum\limits_1^{n+1} \omega(i) = \sum\limits_1^{n} \omega(i) +\omega(i/n+1)  \qquad \mbox{w wyrażeniu }\omega \mbox{ wszystkie wystąpienia zmiennej i zastąp przez } n+1
 \end{array} </math>

@@ Linia 45: / Linia 45: @@
 == Dowód poprawności ==
-'''Precondition''' <math>\alpha</math>: typ(A) jest arrayof real i typ(B) jest array of real i lower(A) = lower(B) i upper(A) = upper(B) i typ(i) jest integer i typ(s) jest real. Czyli wielkości A i B są tablicami o jednakowym rozmiarze.
+'''Precondition''' <math>\alpha</math>: typ(A) jest arrayof real i typ(B) jest array of real i lower(A) = lower(B) i upper(A) = upper(B) i typ(i) jest integer i typ(s) jest real. Czyli wielkości A i B są jednowymiarowymi tablicami liczb rzeczywistych o jednakowym rozmiarze upper(A)-lower(A)+1.
 '''Postcondition''' <math>\beta</math>: <math>s=\sum\limits_{i=lower(A)}^{upper(A)}A_i * B_i</math>

@@ Linia 45: / Linia 45: @@
 == Dowód poprawności ==
-'''Precondition''' <math>\alpha</math>: typ(A) jest arrayof real i typ(B) jest array of real i lower(A) = lower(B) i upper(A) = upper(B) i typ(i) jest integer i typ(s) jest real.
+'''Precondition''' <math>\alpha</math>: typ(A) jest arrayof real i typ(B) jest array of real i lower(A) = lower(B) i upper(A) = upper(B) i typ(i) jest integer i typ(s) jest real. Czyli wielkości A i B są tablicami o jednakowym rozmiarze.
 '''Postcondition''' <math>\beta</math>: <math>s=\sum\limits_{i=lower(A)}^{upper(A)}A_i * B_i</math>
@@ Linia 54: / Linia 54: @@
 \begin{array}{l} s:=0; \\ \mathbf{for}\ i\ :=\ lower(A)\ \mathbf{to}\ upper(A)\ \mathbf{do}\ s\ :=\ s+A[i] * B[i]\ \mathbf{od} \end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{upper(A)}A_i * B_i \right)</math>
-Dowód przebiega przez indukcję ze względu na wielkość upper(A)-lower(A).
+Dowód przebiega przez indukcję ze względu na wielkość długość tablic tzn. wielkość upper(A)-lower(A).
-(Podstawa indukcji) Gdy lower(A)=upper(A) to należy udowodnić
+(''Podstawa indukcji'') Gdy lower(A)=upper(A) to należy udowodnić
 <math> \alpha \Rightarrow \left [
@@ Linia 87: / Linia 87: @@
 formułę oczywiście prawdziwą.
 Wszystkie kroki polegały na przejściu od formuły do formuły jej równoważnej. W ten sposób udowodniliśmy bazę indukcji.
-(Krok indukcji) Załóżmy, że nasza formuła jest prawdziwa dla <math>upper(A)-lower(A)=n</math> i zbadajmy prawdziwość formuły
+(''Krok indukcji'') Załóżmy, że nasza formuła jest prawdziwa dla <math>n=upper(A)-lower(A)</math> i zbadajmy prawdziwość formuły dla n+1.
 <math> \alpha \Rightarrow \left [
-\begin{array}{l} s:=0; \\ \mathbf{for}\ i\ :=\ lower(A)\ \mathbf{to}\ upper(A)+1\ \mathbf{do}\ s\ :=\ s+A[i] * B[i]\ \mathbf{od} \end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{upper(A)+1}A_i * B_i \right)</math>
+\begin{array}{l} s:=0; \\ \mathbf{for}\ i\ :=\ lower(A)\ \mathbf{to}\ lower(A)+n+1\ \mathbf{do}\ s\ :=\ s+A[i] * B[i]\ \mathbf{od} \end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{lower(A)+n+1}A_i * B_i \right)</math>
 Teraz zastosujemy własność (f3)
 <math> \alpha \Rightarrow \left [
-\begin{array}{l} s:=0; \\ \mathbf{for}\ i\ :=\ lower(A)\ \mathbf{to}\ upper(A)\ \mathbf{do}\ s\ :=\ s+A[i] * B[i]\ \mathbf{od}; \\ i := upper(A)+1; \\ s\ :=\ s+A[i] * B[i]\end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{upper(A)+1}A_i * B_i \right)</math>
+\begin{array}{l} s:=0; \\ \mathbf{for}\ i\ :=\ lower(A)\ \mathbf{to}\ lower(A)+n\ \mathbf{do}\ s\ :=\ s+A[i] * B[i]\ \mathbf{od}; \\ i := lower(A)+n+1; \\ s\ :=\ s+A[i] * B[i]\end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{lower(A)+n+1}A_i * B_i \right)</math>
 Z założenia indukcyjnego wiemy, że po wykonaniu dwu pierwszych instrukcji spełniona jest asercja
 <math> \alpha \Rightarrow \left [
-\begin{array}{l} s:=0; \\ \mathbf{for}\ i\ :=\ lower(A)\ \mathbf{to}\ upper(A)\ \mathbf{do}\ s\ :=\ s+A[i] * B[i]\ \mathbf{od}; \\
+\begin{array}{l} s:=0; \\ \mathbf{for}\ i\ :=\ lower(A)\ \mathbf{to}\ lower(A)+n\ \mathbf{do}\ s\ :=\ s+A[i] * B[i]\ \mathbf{od}; \\
-\left( \mathbf{Asercja }\ s=\sum\limits_{i=lower(A)}^{upper(A)} A_i * B_i  \right) \\ i := upper(A)+1; \\ s\ :=\ s+A[i] * B[i]\end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{upper(A)+1}A_i * B_i \right)</math>
+\left( \mathbf{Asercja }\ s=\sum\limits_{i=lower(A)}^{lower(A)+n} A_i * B_i  \right) \\ i := lower(A)+n+1; \\ s\ :=\ s+A[i] * B[i]\end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{upper(A)+1}A_i * B_i \right)</math>
-co pozwala nam zastąpić tę formułę formułą jej równoważną
+co pozwala nam zastąpić tę formułę, formułą jej równoważną
 <math> \alpha \Rightarrow \left [
 \begin{array}{l}
-  i := upper(A)+1; \\ s\ :=\ \left(\sum\limits_{i=lower(A)}^{upper(A)} A_i * B_i\right)+A[i] * B[i] \end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{upper(A)+1}A_i * B_i \right)</math>
+  i := lower(A)+n+1; \\ s\ :=\ \left(\sum\limits_{i=lower(A)}^{lower(A)+n} A_i * B_i\right)+A[i] * B[i] \end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{lower(A)+n+1}A_i * B_i \right)</math>
 ponownie stosujemy aksjomat instrukcji przypisania
 <math> \alpha \Rightarrow \left [
-  s\ :=\ \left(\sum\limits_{i=lower(A)}^{upper(A)} A_i * B_i\right)+A[upper(A)+1] * B[upper(A)+1] \right ] \left( s=\sum\limits_{i=lower(A)}^{upper(A)+1}A_i * B_i \right)</math>
+  s\ :=\ \left(\sum\limits_{i=lower(A)}^{lower(A)+n} A_i * B_i\right)+A[lower(A)+n+1] * B[lower(A)+n+1] \right ] \left( s=\sum\limits_{i=lower(A)}^{lower(A)+n+1}A_i * B_i \right)</math>
 i jeszcze raz, by otrzymać
-<math> \alpha \Rightarrow  \left( \left(\sum\limits_{i=lower(A)}^{upper(A)} A_i * B_i\right)+A[upper(A)+1] * B[upper(A)+1]=\sum\limits_{i=lower(A)}^{upper(A)+1}A_i * B_i \right)</math>
+<math> \alpha \Rightarrow  \left( \left(\sum\limits_{i=lower(A)}^{lower(A)+n} A_i * B_i\right)+A[lower(A)+n+1] * B[lower(A)+n+1]=\sum\limits_{i=lower(A)}^{lower(A)+n+1}A_i * B_i \right)</math>
 zastosujemy własność (s3) sumy
-<math> \alpha \Rightarrow  \left( \sum\limits_{i=lower(A)}^{upper(A)+1} A_i * B_i =\sum\limits_{i=lower(A)}^{upper(A)+1}A_i * B_i \right)</math>
+<math> \alpha \Rightarrow  \left( \sum\limits_{i=lower(A)}^{lower(A)+n+1} A_i * B_i =\sum\limits_{i=lower(A)}^{lower(A)+n+1}A_i * B_i \right)</math>
 co kończy dowód.