SpecVer/IloczynSkalarny: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
(Algorytm)
(Narzędzia)
Linia 3: Linia 3:
 
== Narzędzia ==
 
== Narzędzia ==
 
W dowodzie wykorzystamy własności instrukcji '''for'''
 
W dowodzie wykorzystamy własności instrukcji '''for'''
# for i := 1 to 0 do K od <math> \alpha \equiv \alpha </math>
+
 
# for i:= n to n do K od <math> \alpha \equiv</math> [i:=n] <math> \alpha</math>
+
<math>  \begin{array}{l}
# for i := 1 to n+1 do K od <math> \alpha \equiv </math>[for i := 1 to n+1 do K od; i:=n+1; K ] <math>\ \alpha</math>
+
(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>
 
oraz własności sumy <math> \sum</math>
  
# <math> \sum\limits_1^0 \omega(i) = 0</math>
+
<math>   \begin{array}{l}
# <math> \sum\limits_1^1 \omega(i) = \omega(i/1)</math>
+
(s1)\ \sum\limits_1^0 \omega(i) = 0 \\
# <math> \sum\limits_1^{n+1} \omega(i) = \sum\limits_1^{n} \omega(i) +\omega(i/n+1)</math>
+
(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 ==
 
== Dowód poprawności ==

Wersja z 21:04, 13 lut 2013

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]

Uwagi końcowe