I was solving an exercise from the book "Complexity, computability and languages" which asks:
Write a program that computes $f(x)=1 \iff x$ is even, $f(x)=0\iff x$ is odd.
I wrote the following code, which I believe is correct:
$$ Z\leftarrow Z +1 \\ \quad\quad\text{IF X $\neq$ 0 GOTO A}\\ [C]Y \leftarrow Y+1\\ \quad\quad\text{IF Z $\neq$ 0 GOTO E}\\ [A] X\leftarrow X-1\\ \quad\quad\text{IF X$\neq$ 0 GOTO B}\\ \quad\quad\text{IF Z$\neq$0 GOTO E }\\ [B] X\leftarrow X-1\\ \quad\quad\text{IF X$\neq$ 0 GOTO A}\\ \quad\quad\text{IF Z$\neq$ 0 GOTO C}\\ $$ $X$ is the input variable. $Y$ is the output variable and $Z$ is an temporary variable. The latter 2 are initialized at $0$.
And I want to prove this code correctly computes $f$ (not part of the exercise), how hard is this?