SpecVer/IloczynSkalarny: Różnice pomiędzy wersjami
(→Dowód poprawności) |
(→Dowód poprawności) |
||
| Linia 30: | Linia 30: | ||
Dowód przebiega przez indukcję ze względu na wielkość upper(A)-lower(A). | Dowód przebiega przez indukcję ze względu na wielkość upper(A)-lower(A). | ||
| − | 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 [ | ||
| Linia 63: | Linia 63: | ||
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. | ||
| − | Załóżmy, że nasza formuła jest prawdziwa dla upper(A)-lower(A)=n i zbadajmy prawdziwość formuły | + | (Krok indukcji) Załóżmy, że nasza formuła jest prawdziwa dla <math>upper(A)-lower(A)=n</math> i zbadajmy prawdziwość formuły |
<math> \alpha \Rightarrow \left [ | <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}\ 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> | ||
| + | |||
| + | 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> | ||
| + | |||
| + | 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}; \\ | ||
| + | \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> | ||
== Uwagi końcowe == | == Uwagi końcowe == | ||
Wersja z 22:12, 13 lut 2013
Spis treści
Algorytm
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) \\ (s3)\ \sum\limits_1^{n+1} \omega(i) = \sum\limits_1^{n} \omega(i) +\omega(i/n+1) \end{array} [/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.
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 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), (s2) i aksjomat instrukcji przypisania
[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; \\ \ s\ :=\ s+A[lower(A)] * B[lower(A)] \end{array}\right ] \left( s=A_{lower(A)} * B_{lower(A)} \right)[/math]
i jeszcze raz aksjomat instrukcji przypisania
[math] \alpha \Rightarrow \left [ s\ :=\ 0+A[lower(A)] * B[lower(A)] \right ] \left( s=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]upper(A)-lower(A)=n[/math] i zbadajmy prawdziwość formuły
[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]
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]
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}; \\ \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]
