Why is the Halting problem decidable for Goto languages limited on the highest value of constants and variables?

Question

This is taken from an old exam of my university that I am using to prepare myself for the coming exam:

Given is a language $\text{Goto}_{17}^c \subseteq \text{Goto}$. This language contains exactly those $\text{Goto}$ programs in which no constant is ever above $17$ nor any variable ever above $c$.

$Goto$ here describes the set of all programs written in the $Goto$ language made up of the following elements:

With variables $v_i \in \mathbb{N}$ and constants $c \in \mathbb{N}$
Assignment: $x_i := c, x_i := x_i \pm c$
Conditional Jump: if(Comparison) goto $L_i$
Haltcommand: halt

I am currently struggling with the formalization of a proof, but this is what I have come to so far, phrased very casually: For any given program in this set we know that it is finite. A finite program contains a finite amount of variables and a finite amount of states, or lines to be in. As such, there is a finite amount of configurations in which this process can be. If we let this program run, we can keep a list of all configurations we have seen. That is, the combination of all used variable-values and the state of the program. If we let the program run, there must be one of two things that happens eventually: The program halts. In this case, we return YES and have decided that it halts. The program reaches a configuration that has been recorded before. As the language is deterministic, this means that we must have gone a full loop which will exactly repeat now.

No other case can exist as that would mean that we keep running forever on finite code without repeating a configuration. This means after every step, among our list of infinite steps, there is a new configuration. This would mean that there are infinite configurations, which is a contradiction.

Is this correct? Furthermore, how would a more formal proof look if it is? If not, how would a correct proof look?

Answer 1

There is a finite number of different states (the set of values of the variables and the program counter). Your "limited goto programs" are just a (messy) way to describe a deterministic finite automaton.

Or just reason that the program states being finite, it is certainly possible to map out all possible non-looping computations (by something like a breadth first search of the graph of states and neighbours).