Using Primed Variables
lInstead
of assignment statements:
sum = sum + fd;
fd = fd + sd;
i = i+1;
use mathematical equations:
sumÕ == sum + fd
fdÕ == fd + sd
sdÕ == sd (no change)
iÕ == i+1
sum = sum + fd;
fd = fd + sd;
i = i+1;
use mathematical equations:
sumÕ == sum + fd
fdÕ == fd + sd
sdÕ == sd (no change)
iÕ == i+1
lIt
is easier to reason about equations:
lsum
== i2
ô i < n ô fd == 2*i+1 ô sd == 2
ô i < n
implies
ô i < n
implies
lsumÕ
== iÕ2 ô iÕ < n ô fdÕ == 2*iÕ+1 ô sdÕ == 2