Prove that the following algorithm has STOP property (number of steps is finite) Prove that the following algorithm has STOP property. I am not sure if this term is widely know, so the definition of STOP property that I got during classes looks as follows:


  STOP property (for all input data satisfying $ \alpha $ the computation halts - the number of steps is finite)


$\alpha: x \in N $

void BB(int x)
{
    int y = x;
    int z = 0;
    while((z != 0) || (y &lt;= 300))
    {
        if(y &lt;= 300)
        {
            y = y + 3;
            z = z + 1;
        }
        else
        {
            y = y - 2;
            z = z - 1;
        }
    }
}


I do not really have any idea how to approach such a problem. I was thinking about using the method of loop counters, but I couldn't success with it.
You have three possible cases:


$y &gt; 300$. Since $z = 0$ initially, the algorithm terminates.
$y = 300$ and $z = 0$.
You enter the first if and you get $y = 303$ and $z = 1$. Then you enter the second if and you get $y = 301$ and $z = 0$. Since $y &gt; 300$ and $z = 0$  the algorithm stops.
$y &lt; 300$ and $z = 0$.
After $k$ iterations $y = 301$ or $y = 302$ or $y=303$ and $z = k$. By executing the algorithm for each $y$ you can see that $y$ only takes values in a specific range while $z$ is always decreasing and will eventually reach 0 (or it will become less than 0). For example, let $y = 301$ and $z = k$. By executing the algorithm you get the following values:

${\bf y = 301, z = k} \\
y = 299, z=k-1 \\
y=302, z = k\\
y = 300, z = k-1 \\
y = 303, z = k \\
{\bf y = 301, z = k-1}\\
y = 299, z = k-2 \\
y=302, z = k-1\\
y = 300, z = k-2 \\
y = 303, z = k-1 \\
{\bf y = 301, z = k-2}\\$

Obviously each time you reach $y = 301$, z is decreased by 1. After showing that the same thing happens for the other two possible values of $y$ you have proved that for every possible starting value, the algorithm stops after a finite number of steps.