# 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 <= 300))
{
if(y <= 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 > 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 > 300$$ and $$z = 0$$ the algorithm stops.
• $$y < 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.

A simple case: What happens if x > 300? (Think about it). So that was easy, the program stops.

What if x ≤ 300, including x = 0? First there is a phase where y is increased by 3 each time, and that will happen at least once (if x ≥ 298) and at most 101 times (if x = 0), so we end that phase with x ≤ 101, and y is 301, 302, or 303.

Now comes a second phase: We have y = 301, 302, or 303. If y = 301 (you think what the next two steps will be), and we have y = 302 and x unchanged. If y = 302 (you think what the next two steps will be), and we have y = 303 and x unchanged. But in the last case y = 303 (you think what the next three steps will be), and we have y = 301 and x is one less than before!

If x isn't 0 already, you figure out what will happen after every 7 iterations of the loop, and then it is obvious that the program stops.