SpecVer/IloczynSkalarny

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]