SpecVer/IloczynSkalarny
Z Lem
Wersja AndrzejSalwicki (dyskusja | edycje) z dnia 19:34, 13 lut 2013
Spis treści
[ukryj]Algorytm
Narzędzia
W dowodzie wykorzystamy własności instrukcji for
- for i := 1 to 0 do K od α≡α
- for i:= n to n do K od α≡[i:=n] α
- for i := 1 to n+1 do K od α≡[for i := 1 to n+1 do K od; i:=n+1; K ] α
oraz własności sumy ∑
- 0∑1ω(i)=0
- 1∑1ω(i)=ω(i/1)
- n+1∑1ω(i)=n∑1ω(i)+ω(i/n+1)
Dowód poprawności
Precondition α: 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 β: s=upper(A)∑i=lower(A)Ai∗Bi