SpecVer/IloczynSkalarny: Różnice pomiędzy wersjami
Z Lem
(→Dowód poprawności) |
(→Algorytm) |
||
| Linia 1: | Linia 1: | ||
== Algorytm == | == Algorytm == | ||
| + | |||
| + | == Narzędzia == | ||
| + | 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> | ||
| + | # 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> | ||
| + | |||
| + | oraz własności sumy <math> \sum</math> | ||
| + | |||
| + | # <math> \sum\limits_1^0 \omega(i) = 0</math> | ||
| + | # <math> \sum\limits_1^1 \omega(i) = \omega(i/1)</math> | ||
| + | # <math> \sum\limits_1^{n+1} \omega(i) = \sum\limits_1^{n} \omega(i) +\omega(i/n+1)</math> | ||
== Dowód poprawności == | == Dowód poprawności == | ||
Wersja z 20:34, 13 lut 2013
Spis treści
Algorytm
Narzędzia
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]
- 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]
oraz własności sumy [math] \sum[/math]
- [math] \sum\limits_1^0 \omega(i) = 0[/math]
- [math] \sum\limits_1^1 \omega(i) = \omega(i/1)[/math]
- [math] \sum\limits_1^{n+1} \omega(i) = \sum\limits_1^{n} \omega(i) +\omega(i/n+1)[/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]
