The loop below computes the sum ${\displaystyle \underset{k=1}{\overset{n}{}}}{k}^2$ :

While $)(n$

sum :$=$ sum $+j^2$

$j$:$=j+1$

End$-$while

Pre$-$condition: $m$ and $n$ are non$-$negative integers. $j=1$ and sum $=0.$

Post$-$condition: ${\displaystyle \underset{?}{\overset{?}{}}}={\displaystyle \underset{k=1}{\overset{n}{}}}{k}^2.$

Loop$-$ invariant: $j$ is an integer, $jn+1,$ and ${\displaystyle \underset{?}{\overset{?}{}}}={\displaystyle \underset{k=1}{\overset{j-1}{}}}{k}^2.$

What facts are assumed in proving the post$-$condition?

$j$ is an integer

$jn$ and $jn$

${\displaystyle \underset{?}{\overset{?}{}}}={\displaystyle \underset{k=1}{\overset{j-1}{}}}{k}^2$

$j$ is an integer

$jn+1$ and $jn$

sum $={\displaystyle \underset{k=1}{\overset{j-1}{}}}{k}^2$

$j$ is an integer

$jn$ and $j>n$

${\displaystyle \underset{?}{\overset{?}{}}}={\displaystyle \underset{k=1}{\overset{j-1}{}}}{k}^2$

$j$ is an integer

$j=n$

${\displaystyle \underset{?}{\overset{?}{}}}={\displaystyle \underset{k=1}{\overset{j-1}{}}}{k}^2$