SpecVer/IloczynSkalarny: Różnice pomiędzy wersjami
(→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''' | ||
| − | + | ||
| − | + | <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> | 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 == | == Dowód poprawności == | ||
Wersja z 21:04, 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]
