Given a while loop and a predicate, show that if the predicate is true before entry to the loop, then it is also true after exit from the loop.
predicate: m^3 > n^2
while (m ≥ 0 and m ≤ 100) do
m := 3 · m
n := 5 · n
end while
I tried to plug the $m$ and $n$ values into the predicate, but just got '27m^3>25n^2`.
Well: The loop shall execute $k$ times, where the integer $k$ is $0$ or greater (NB: if $m=0$ the loop shall be endless). At the end of the loop, the registers for $m$ and $n$ shall be multiplied by $3$ and $5$ (respectively) raised to the $k$ eth power.
EG: $m_\textsf{out}=3^k\cdot m_\textsf{in}$, $n_\textsf{out}=5^k\cdot n_\textsf{in}$
So you are asked to show that if $m_\textsf{in}^3>n_\textsf{in}^2$, then $3^{3k}m_\textsf{in}^3>5^{2k}n_\textsf{in}^2$
Well, that's on the right track: every time you go through the loop, $m$ gets $3$ times as large, and $n$ gets $5$ times as large. So, if beforehand we have that $m^3 > n^2$, then afterwards we have that $(3m)^3= 27m^3 > 27n^2 > 25 n^2 = (5n)^2$. That is: the new $m$ raised to the power of $3$ will still be bigger than the new $n$ raised to the power of $2$. So, if the predicate holds before any pass through the loop, then it will hold after that pass as well. Indeed, the loop could go on indefinitely, and the predicate will still hold.
