# Proving the small-step semantics of factorial program

I am given the following command $C$:

$y:=1;$ while $\neg (x=1)$ do $y:= y*x;$ $x:= x - 1$.

I have to show that $[\![ C ]\!]_s(s) = \{x \mapsto 1, y \mapsto s(x)!\}$ if $s(x) \geq 1$ and undefined otherwise. Where $[\![ C ]\!]_s(s) = s'$ if $\langle C, s \rangle \rightarrow^* s'$ and undefined otherwise.

The proof is by induction on $s(x)$. My problem is to figure out the last step in the induction step. The induction hypothesis is that $[\![ C ]\!]_s(s) = \{x \mapsto 1, y \mapsto s(x)!\}$ for $s(x) \leq k$. For the induction step I assume that $s(x)=k+1$. Using the small step semantics rules I obtain a state $s''' = \{x \mapsto k, y \mapsto (k+1)\}$. Then I can apply the induction hypothesis and obtain $[\![ C ]\!]_s(s) = \{x \mapsto 1, y \mapsto k!\}$. Now I am stuck - can anybody give me a hint on how to arrive at $[\![ C ]\!]_s(s) = \{x \mapsto 1, y \mapsto (k+1)!\}$?

• Is there a typo in $s'''$? The value of $y$ looks strange. Please write down explicitly what statement you are trying to prove. In these kinds of proofs you always need to strengthen the original statement so that the induction goes through (essentially, you need to find the loop invariant). – Andrej Bauer Apr 27 '14 at 8:40
• Thank you for your comment. I have added the IH above. The value of $y$ in $s'''$ is actually $y \mapsto y * x$, but since $s''(x)= (k+1)$ and $s''(y) = 1$ at this point, $y \mapsto 1*(k+1)$ in $s'''$. – trojan Apr 27 '14 at 13:46
• You are still missing the loop invariant. Without the loop invariant, you won't be able to prove anything. If $X$ is the original value of $x$, the loop invariant should include the equation $yx! = X!$. This is the reason the C code works correctly. – Yuval Filmus Apr 27 '14 at 20:57