Example Two

Suppose code is:

p:=1;i:=1
while(i =< n)
    {p:=p*i;
    i:=i+1}

Suppose the state space is $\mathbb{N}$   x$\mathbb{N}$   x$\mathbb{N}$, with $(p,i,n)$ a typical state. If input is $(p_0,i_0,4)$, where $p_0,i_0$ are any ``default values'', we get:

$$(p_0,i_0,4) \mapsto (1,i_0,4) \mapsto (1,1,4)$$ (2.1)

$$\mapsto (1,1,4) \mapsto (2,2,4)$$ (2.2)

$$\mapsto (1,2,4) \mapsto (2,3,4)$$ (2.3)

$$\mapsto (6,3,4) \mapsto (6,4,4)$$ (2.4)

$$\mapsto (24,4,4) \mapsto (24,5,4)$$ (2.5)

where 2.1 is after two assignments, 2.2 is after one loop, 2.3 is after two loops, 2.4 is after three loops and 2.5 is the output state after the exit condition is satisfied.

This piece of code seems to compute $p = n!$. How to proive this? How to assert it even?