Tekst źródłowy strony SpecVer/IloczynSkalarny

== 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>

i aksjomat instrukcji przypisania (schemat)

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

== 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>

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>

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>

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>

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>

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'''

::Jeśli wartości wyrażenia  <math>\tau(i)</math>  są nieujemne, to  <math>  \left[\begin{array}{l} s\ :=0; \\for\ i:=0\ to\ n\ do\ s := min(s, \tau(i))\ od  \end{array}  \right]\left(s= min_{i=1}^{n}\ \tau(i)  \right) </math>

'''Lemat'''

::Jeśli wartości wyrażenia  <math>\tau(i)</math>  są nieujemne, to  <math>  \left[\begin{array}{l} s\ :=0; \\for\ i:=0\ to\ n\ do\\ \quad if \ \alpha(i)\ then   j:= i; exit \ fi\\ od  \end{array}  \right]\left(\, j= \mu i  \{\alpha(i) \}  \right) </math>