CMIMC 2017 Power Problem 5

[system]

An algorithm is a set of instructions for performing a task. For instance, the following two algorithms determine if a nonnegative integer is odd or even:

\textbf{Data}: a nonnegative integer n
\textbf{Result}: whether n is odd or even
\textbf{while} n \geq 0 \textbf{do}
\quad \textbf{if} n=0 \textbf{then}
\quad \quad \textbf{return} n is even
\quad \textbf{end}
\quad \textbf{else if} n=1 \textbf{then}
\quad \quad \textbf{return} n is odd
\quad \textbf{end}
\quad \textbf{else}
\quad \quad n \leftarrow n-2
\quad \textbf{end}
\textbf{end}

\textbf{Data}: a nonnegative integer n
\textbf{Result}: whether n is odd or even
\textbf{for} i=0,2,4,6, \ldots \textbf{do}
\quad \textbf{if} n=i \textbf{then}
\quad \quad \textbf{return} n is even
\quad \textbf{end}
\quad \textbf{else if} n=i+1 \textbf{then}
\quad \quad \textbf{return} n is odd
\quad \textbf{end}
\textbf{end}

We will now detail a common convention in writing algorithms called pseudocode. It is not required that you follow these conventions, but you must be able to clearly describe the steps of your algorithms. There are only a few conventions that we need to introduce:

\begin{array}{|l|l|} \hline \text{[variable name]} \leftarrow \text{[value]} & \text{Assigns (or reassigns) } \text{[value]} \text{ to } \text{[variable name]} \\ \textbf{if} \ \text{[condition]} \ \textbf{then} & \text{Perform the indented instruction if } \text{[condition]} \text{ is satisfied} \\ \textbf{else if} \ \text{[condition]} \ \textbf{then} & \text{Perform the indented instruction if the previous } \textbf{if} \text{ condition isn't satisfied} \\ & \text{but } \text{[condition]} \text{ is satisfied} \\ \textbf{else} & \text{Perform the indented instruction if none of the previous } \textbf{if} \text{ conditions are satisfied} \\ \textbf{while} \ \text{[condition]} \ \textbf{do} & \text{Iteratively perform the indented instruction as long as } \text{[condition]} \text{ is satisfied} \\ \textbf{for} \ \text{[variable name] = [sequence]} \ \textbf{do} & \text{Iteratively perform the indented instruction for each value of } \text{[variable name]} \\ & \text{in the sequence} \\ \text{return} \ \text{[value]} & \text{The output of the algorithm} \\ \hline \end{array}

Algorithms generally require correctness - the algorithm always outputs the right answer - and termination - the algorithm doesn’t run infinitely.

Prove that the above two algorithms are correct and always terminate.