SpecVer/IloczynSkalarny

Z Lem
Skocz do: nawigacji, wyszukiwania

Algorytm

Narzędzia

W dowodzie wykorzystamy własności instrukcji for

  1. for i := 1 to 0 do K od αα
  2. for i:= n to n do K od α
    [i:=n] α
  3. 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

  1. 01ω(i)=0
  2. 11ω(i)=ω(i/1)
  3. n+11ω(i)=n1ω(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)AiBi

Uwagi końcowe