How to show that the predicate of the loop holds before and after the loop?

Question

For example for this loop:

$Predicate = 2^n \le (n+2)!$

$while (n\ge 0 $ and $n \le 100)$

$n: = n +1$

$end$ $while$

I had this as base: $ n =0:$

$ 2^0 \le (0+2)!$

$1 \le 1 X 2$

which is true, but i didnt know how to proof the predicate at the end of the loop. Could someone help me?

And a small subquestion: how to do these loops in general. Cant find a good explanation.

Answer 1

At the beginning of the loop, i.e., immediately before the $n:=n+1$ statement, we know that $2^n\le (n+2)!$ and that $0\le n\le 100$. If we denote with $n'$ the value of $n$ after the loop (i.e., $n'=n+1$ and $n=n'-1$), then the above gives us that $2^{n'-1}\le (n'+1)!$ and $n'\ge 0$. Using $n'+2\ge 2$, we find $$ (n'+2)!=(n'+2)\cdot (n'+1)!\ge 2\cdot (n'+1)!\ge 2\cdot 2^{n'-1}=2^{n'}.$$