SpecVer/IloczynSkalarny: Różnice pomiędzy wersjami
(→Dowód poprawności) |
(→Dowód poprawności) |
||
| (Nie pokazano 23 pośrednich wersji utworzonych przez tego samego użytkownika) | |||
| Linia 1: | Linia 1: | ||
== Algorytm == | == Algorytm == | ||
| + | '''program''' Iloczyn_skalarny; | ||
| + | : '''var''' n: integer, | ||
| + | ::s: real, | ||
| + | ::A, B: '''arrayof''' real; | ||
| + | '''begin''' | ||
| + | :(* pobierz wartość n i utwórz tablice A i B *) | ||
| + | :readln(n); | ||
| + | :'''array''' A '''dim''' (1:n); | ||
| + | :'''array''' A '''dim''' (1:n); | ||
| + | : (* wypełnij tablice A oraz B np.*) | ||
| + | :'''for''' i := 1 '''to''' n '''do''' read(A[i]); readln(B[i]) '''od'''; | ||
| + | :(* --------------------------------- *) | ||
| + | :s:=0; | ||
| + | :'''for''' i := 1 '''to''' n '''do''' | ||
| + | ::s := s+ A[i]*B[i] | ||
| + | :'''od'''; | ||
| + | :(* --------------------------------- *) | ||
| + | :(* wydrukuj wynik *) | ||
| + | :writeln(s) | ||
| + | '''end''' | ||
== Narzędzia == | == Narzędzia == | ||
| Linia 14: | Linia 34: | ||
<math> \begin{array}{l} | <math> \begin{array}{l} | ||
(s1)\ \sum\limits_1^0 \omega(i) = 0 \\ | (s1)\ \sum\limits_1^0 \omega(i) = 0 \\ | ||
| − | (s2)\ \sum\limits_1^1 \omega(i) = \omega(i/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) | + | (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> | \end{array} </math> | ||
| + | |||
| + | i aksjomat instrukcji przypisania (schemat) | ||
| + | |||
| + | :::<math>\color{blue}\alpha(x/\tau)\equiv[x := \tau]\alpha </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 == | == 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ą 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> | '''Postcondition''' <math>\beta</math>: <math>s=\sum\limits_{i=lower(A)}^{upper(A)}A_i * B_i</math> | ||
| Linia 28: | 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> | \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 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 [ | <math> \alpha \Rightarrow \left [ | ||
\begin{array}{l} s:=0; \\ \mathbf{for}\ i\ :=\ lower(A)\ \mathbf{to}\ lower(A)\ \mathbf{do}\ s\ :=\ s+A[i] * B[i]\ \mathbf{od} \end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{lower(A)}A_i * B_i \right)</math> | \begin{array}{l} s:=0; \\ \mathbf{for}\ i\ :=\ lower(A)\ \mathbf{to}\ lower(A)\ \mathbf{do}\ s\ :=\ s+A[i] * B[i]\ \mathbf{od} \end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{lower(A)}A_i * B_i \right)</math> | ||
| − | Wykorzystamy własność (f2) | + | Wykorzystamy własność (f2) |
<math> \alpha \Rightarrow \left [ | <math> \alpha \Rightarrow \left [ | ||
| − | \begin{array}{l} s:=0; \\ i\ :=\ lower(A);\ s\ :=\ s+A[i] * B[i] \end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{upper(A)}A_i * B_i \right)</math> | + | \begin{array}{l} s:=0; \\ i\ :=\ lower(A);\\ s\ :=\ s+A[i] * B[i] \end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{upper(A)}A_i * B_i \right)</math> |
własność (s2) | własność (s2) | ||
<math> \alpha \Rightarrow \left [ | <math> \alpha \Rightarrow \left [ | ||
| − | \begin{array}{l} s:=0; \\ i\ :=\ lower(A);\ s\ :=\ s+A[i] * B[i] \end{array}\right ] \left( s=A_{lower(A)} * B_{lower(A)} \right)</math> | + | \begin{array}{l} s:=0; \\ i\ :=\ lower(A);\\ s\ :=\ s+A[i] * B[i] \end{array}\right ] \left( s=A_{lower(A)} * B_{lower(A)} \right)</math> |
aksjomat instrukcji przypisania | aksjomat instrukcji przypisania | ||
<math> \alpha \Rightarrow \left [ | <math> \alpha \Rightarrow \left [ | ||
| − | \begin{array}{l} s:=0; \\ | + | \begin{array}{l} s:=0; \\ i\ :=\ lower(A);\\ \end{array}\right ] \left( s+A[i] * B[i] =A_{lower(A)} * B_{lower(A)} \right)</math> |
i jeszcze raz aksjomat instrukcji przypisania | i jeszcze raz aksjomat instrukcji przypisania | ||
<math> \alpha \Rightarrow \left [ | <math> \alpha \Rightarrow \left [ | ||
| − | s\ :=\ 0+A[lower(A)] * B[lower(A)] | + | s\ :=\ 0 \right ] \left( s +A[lower(A)] * B[lower(A)]=A_{lower(A)} * B_{lower(A)} \right)</math> |
kolejne zastosowanie aksjomatu instrukcji przypisania daje nam | kolejne zastosowanie aksjomatu instrukcji przypisania daje nam | ||
| Linia 61: | Linia 87: | ||
formułę oczywiście prawdziwą. | 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. | 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) | + | (''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 [ | <math> \alpha \Rightarrow \left [ | ||
| − | \begin{array}{l} s:=0; \\ \mathbf{for}\ i\ :=\ lower(A)\ \mathbf{to}\ | + | \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) | Teraz zastosujemy własność (f3) | ||
<math> \alpha \Rightarrow \left [ | <math> \alpha \Rightarrow \left [ | ||
| − | \begin{array}{l} s:=0; \\ \mathbf{for}\ i\ :=\ lower(A)\ \mathbf{to}\ | + | \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 | Z założenia indukcyjnego wiemy, że po wykonaniu dwu pierwszych instrukcji spełniona jest asercja | ||
<math> \alpha \Rightarrow \left [ | <math> \alpha \Rightarrow \left [ | ||
| − | \begin{array}{l} s:=0; \\ \mathbf{for}\ i\ :=\ lower(A)\ \mathbf{to}\ | + | \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)}^{ | + | \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 [ | <math> \alpha \Rightarrow \left [ | ||
\begin{array}{l} | \begin{array}{l} | ||
| − | i := | + | 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 | ponownie stosujemy aksjomat instrukcji przypisania | ||
<math> \alpha \Rightarrow \left [ | <math> \alpha \Rightarrow \left [ | ||
| − | s\ :=\ (\sum\limits_{i=lower(A)}^{ | + | 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ć | i jeszcze raz, by otrzymać | ||
| − | <math> \alpha \Rightarrow \left( (\sum\limits_{i=lower(A)}^{ | + | <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 | zastosujemy własność (s3) sumy | ||
| − | <math> \alpha \Rightarrow \left( \sum\limits_{i=lower(A)}^{ | + | <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. | co kończy dowód. | ||
== Uwagi końcowe == | == Uwagi końcowe == | ||
| + | Powyższy dowód przeprowadziliśmy tak szczegółowo by czytelnik mógł sam udowodnić kilka lematów | ||
| + | |||
| + | |||
| + | '''Lemat''' | ||
| + | |||
| + | ::<math>\left[\begin{array}{l}s:=0; \\for\ i:=0\ to\ n\ do\ s :=\ s+\omega(i)\ od \end{array} \right]\left(s=\sum\limits_{i=1}^{n}\ \omega(i) \right)</math> | ||
| + | |||
| + | '''Lemat''' | ||
| + | |||
| + | ::<math>\left[\begin{array}{l}s:=1; \\for\ i:=0\ to\ n\ do\ s :=\ s*\omega(i)\ od \end{array} \right]\left(s=\prod\limits_{i=1}^{n}\ \omega(i) \right)</math> | ||
| + | |||
| + | '''Lemat''' | ||
| + | |||
| + | ::<math>\left[\begin{array}{l}s:=false; \\for\ i:=0\ to\ n\ do\ s :=\ s\vee\alpha(i)\ od \end{array} \right]\left(s=\bigvee\limits_{i=1}^{n}\ \alpha(i) \right)</math> | ||
| + | |||
| + | '''Lemat''' | ||
| + | |||
| + | ::<math>\left[\begin{array}{l}s:=true; \\for\ i:=0\ to\ n\ do\ s :=\ s\wedge\alpha(i)\ od \end{array} \right]\left(s=\bigwedge\limits_{i=1}^{n}\ \alpha(i) \right)</math> | ||
| + | |||
| + | '''Lemat''' | ||
| + | |||
| + | ::Jeśli dla każdego <math>1 \leq i\leq n,</math> zachodzi <math>K(i)\alpha(i)</math> to <math> \left[\begin{array}{l} for\ i:=0\ to\ n\ do\ K\ od \end{array} \right]\left( \forall_{i=1}^{n}\ \alpha(i) \right)</math> | ||
| + | |||
| + | '''Lemat''' | ||
| + | |||
| + | :::<math>\frac{\{ K(i)\alpha(i)\}_{1\leq i\leq n} }{ \left[\begin{array}{l} for\ i:=0\ to\ n\ do\ K\ od \end{array} \right]\left( \forall_{1 \leq i\leq n}\, \alpha(i) \right)}</math> | ||
| + | |||
| + | '''Lemat''' | ||
| + | |||
| + | ::<math> \left[\begin{array}{l} s\ :=+\infty; \\for\ i:=0\ to\ n\ do\ s := min(s, \tau(i))\ od \end{array} \right]\left(s= min(\tau(1), \dots ,\tau(n)) \right) </math> | ||
| + | |||
| + | '''Lemat''' | ||
| + | |||
| + | ::<math> \left[\begin{array}{l} s\ :=0;\ j:=0; \\for\ i:=0\ to\ n\ do\\ \quad if \ \alpha(i)\ then \ j:= i; exit \ fi\\ od \end{array} \right]\ \left(\, j= (\mu i \leq n) \{\alpha(i) \} \right) </math> | ||
| + | |||
| + | '''Lemat''' | ||
| + | |||
| + | ::<math> \left[\begin{array}{l} i\ :=0; \\while\ \neg \alpha(i) do\\ \quad i:= i+1\\ od;\\ j:=i \end{array} \right]\left(\, j= \mu i \{\alpha(i) \} \right) </math> | ||
Aktualna wersja na dzień 13:58, 26 lis 2015
Spis treści
Algorytm
program Iloczyn_skalarny;
- var n: integer,
- s: real,
- A, B: arrayof real;
begin
- (* pobierz wartość n i utwórz tablice A i B *)
- readln(n);
- array A dim (1:n);
- array A dim (1:n);
- (* wypełnij tablice A oraz B np.*)
- for i := 1 to n do read(A[i]); readln(B[i]) od;
- (* --------------------------------- *)
- s:=0;
- for i := 1 to n do
- s := s+ A[i]*B[i]
- od;
- (* --------------------------------- *)
- (* wydrukuj wynik *)
- writeln(s)
end
Narzędzia
W dowodzie wykorzystamy własności instrukcji for
[math] \begin{array}{l} (f1) \ \mathbf{for}\ i\ := \ 1\ \mathbf{to}\ 0\ \mathbf{do}\ K\ \mathbf{od}\ \alpha \equiv \alpha \\ (f2)\ \mathbf{for}\ i\ :=\ n\ \mathbf{to}\ n\ \mathbf{do}\ K\ \mathbf{od}\ \alpha \equiv \{i:=n\}\ \alpha \\ (f3)\ \mathbf{for}\ i\ :=\ 1\ \mathbf{to}\ n+1\ \mathbf{do}\ K\ \mathbf{od}\ \alpha \equiv \{\mathbf{for}\ i\ :=\ 1\ \mathbf{to}\ n+1\ \mathbf{do}\ K\ \mathbf{od};\ i:=n+1;\ K \} \ \alpha \end{array} [/math]
oraz własności sumy [math] \sum[/math]
[math] \begin{array}{l} (s1)\ \sum\limits_1^0 \omega(i) = 0 \\ (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) \qquad \mbox{w wyrażeniu }\omega \mbox{ wszystkie wystąpienia zmiennej i zastąp przez } n+1 \end{array} [/math]
i aksjomat instrukcji przypisania (schemat)
- [math]\color{blue}\alpha(x/\tau)\equiv[x := \tau]\alpha [/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
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]
Należy udowodnić formułę
[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} \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 długość tablic tzn. wielkość upper(A)-lower(A).
(Podstawa indukcji) Gdy lower(A)=upper(A) to należy udowodnić
[math] \alpha \Rightarrow \left [ \begin{array}{l} s:=0; \\ \mathbf{for}\ i\ :=\ lower(A)\ \mathbf{to}\ lower(A)\ \mathbf{do}\ s\ :=\ s+A[i] * B[i]\ \mathbf{od} \end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{lower(A)}A_i * B_i \right)[/math]
Wykorzystamy własność (f2)
[math] \alpha \Rightarrow \left [ \begin{array}{l} s:=0; \\ i\ :=\ lower(A);\\ s\ :=\ s+A[i] * B[i] \end{array}\right ] \left( s=\sum\limits_{i=lower(A)}^{upper(A)}A_i * B_i \right)[/math]
własność (s2)
[math] \alpha \Rightarrow \left [ \begin{array}{l} s:=0; \\ i\ :=\ lower(A);\\ s\ :=\ s+A[i] * B[i] \end{array}\right ] \left( s=A_{lower(A)} * B_{lower(A)} \right)[/math]
aksjomat instrukcji przypisania
[math] \alpha \Rightarrow \left [ \begin{array}{l} s:=0; \\ i\ :=\ lower(A);\\ \end{array}\right ] \left( s+A[i] * B[i] =A_{lower(A)} * B_{lower(A)} \right)[/math]
i jeszcze raz aksjomat instrukcji przypisania
[math] \alpha \Rightarrow \left [ s\ :=\ 0 \right ] \left( s +A[lower(A)] * B[lower(A)]=A_{lower(A)} * B_{lower(A)} \right)[/math]
kolejne zastosowanie aksjomatu instrukcji przypisania daje nam
[math] \alpha \Rightarrow \left( A[lower(A)] * B[lower(A)=A_{lower(A)} * B_{lower(A)} \right)[/math]
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]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}\ 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}\ 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}\ lower(A)+n\ \mathbf{do}\ s\ :=\ s+A[i] * B[i]\ \mathbf{od}; \\ \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ą
[math] \alpha \Rightarrow \left [ \begin{array}{l} 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)}^{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)}^{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)}^{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.
Uwagi końcowe
Powyższy dowód przeprowadziliśmy tak szczegółowo by czytelnik mógł sam udowodnić kilka lematów
Lemat
- [math]\left[\begin{array}{l}s:=0; \\for\ i:=0\ to\ n\ do\ s :=\ s+\omega(i)\ od \end{array} \right]\left(s=\sum\limits_{i=1}^{n}\ \omega(i) \right)[/math]
Lemat
- [math]\left[\begin{array}{l}s:=1; \\for\ i:=0\ to\ n\ do\ s :=\ s*\omega(i)\ od \end{array} \right]\left(s=\prod\limits_{i=1}^{n}\ \omega(i) \right)[/math]
Lemat
- [math]\left[\begin{array}{l}s:=false; \\for\ i:=0\ to\ n\ do\ s :=\ s\vee\alpha(i)\ od \end{array} \right]\left(s=\bigvee\limits_{i=1}^{n}\ \alpha(i) \right)[/math]
Lemat
- [math]\left[\begin{array}{l}s:=true; \\for\ i:=0\ to\ n\ do\ s :=\ s\wedge\alpha(i)\ od \end{array} \right]\left(s=\bigwedge\limits_{i=1}^{n}\ \alpha(i) \right)[/math]
Lemat
- Jeśli dla każdego [math]1 \leq i\leq n,[/math] zachodzi [math]K(i)\alpha(i)[/math] to [math] \left[\begin{array}{l} for\ i:=0\ to\ n\ do\ K\ od \end{array} \right]\left( \forall_{i=1}^{n}\ \alpha(i) \right)[/math]
Lemat
- [math]\frac{\{ K(i)\alpha(i)\}_{1\leq i\leq n} }{ \left[\begin{array}{l} for\ i:=0\ to\ n\ do\ K\ od \end{array} \right]\left( \forall_{1 \leq i\leq n}\, \alpha(i) \right)}[/math]
Lemat
- [math] \left[\begin{array}{l} s\ :=+\infty; \\for\ i:=0\ to\ n\ do\ s := min(s, \tau(i))\ od \end{array} \right]\left(s= min(\tau(1), \dots ,\tau(n)) \right) [/math]
Lemat
- [math] \left[\begin{array}{l} s\ :=0;\ j:=0; \\for\ i:=0\ to\ n\ do\\ \quad if \ \alpha(i)\ then \ j:= i; exit \ fi\\ od \end{array} \right]\ \left(\, j= (\mu i \leq n) \{\alpha(i) \} \right) [/math]
Lemat
- [math] \left[\begin{array}{l} i\ :=0; \\while\ \neg \alpha(i) do\\ \quad i:= i+1\\ od;\\ j:=i \end{array} \right]\left(\, j= \mu i \{\alpha(i) \} \right) [/math]
