SpecVer/IloczynSkalarny

Narzędzia

W dowodzie wykorzystamy własności instrukcji for

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

1. [math] \sum\limits_1^0 \omega(i) = 0[/math]
2. [math] \sum\limits_1^1 \omega(i) = \omega(i/1)[/math]
3. [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]