SpecVer/IloczynSkalarny: Różnice pomiędzy wersjami
Z Lem
(Utworzył nową stronę „== Algorytm == == Dowód poprawności == == Uwagi końcowe ==”) |
(→Dowód poprawności) |
||
| Linia 2: | Linia 2: | ||
== Dowód poprawności == | == 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 == | == Uwagi końcowe == | ||
Wersja z 20:04, 13 lut 2013
Algorytm
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]
