How precise to be when describing a Turing machine?

Question

I'm kind of new to the theory of computation and I was working on this problem:

We say that a Turing machine $M$ uses $k$ squares of tape for an input string $w$ if and only if there exists a configuration $(q, u\underline{a}v)$ of $M$, such that starting with input $w$, $M$ yields $(q, u\underline{a}v)$ and $|uav| \geq k$.

Now show that the following problem is solveable: Given a Turing machine $M$, an input string $w$ and a number $k$ does $M$ use $k$ squares of tape with input $w$?

So the solution I came up with is this:

If it is solvable there has to be a Turing machine $M^*$ that decides $$U = \{\ll M\gg\ll w \gg \ll k\gg\ :M\ \text{uses}\ k\ \text{squares of tape with input}\ w\}$$

And I describe such a machine:

$M^*$ writes in it's tape $w$ and starts operating as $M$ would. After each step of $M$, $M^*$ counts the number consecutive squares of tape from the start of the tape until it finds an empty square, and if that number is $\geq k$ it goes into an accept state and halts. If not, it continues its operation as M would. If $M$ halts without having used at least $k$ steps, $M^*$ goes into a reject state. So $M^*$ decides $U$, and thus the problem is solveable.

So my questions are these:

Is my solution correct?, and

Is my description of $M^*$ precise, or say, good enough?

Answer 1

You are asking two different questions: whether your solution is correct, and whether the level of description of your Turing machine is appropriate. I will answer them separately.

Correctness Your Turing machine $M^*$ is not guaranteed to halt. In other words, your solution is incorrect. The missing observation is that if a Turing machine uses only space $k$, then there is an upper bound on the number of steps that it can run without getting into an infinite loop.

Level of description Here you should be asking two questions:

1. What does it mean to describe a Turing machine?
2. How do I prove that a certain language is decidable?

The level of description of Turing machines is a touchy subject. Usually they are described quite informally. The level of description should be such that in principle you could convert the informal description into a formal Turing machine. In practice, I suggest looking at some examples to get the general feel.

As to how to prove that a language is decidable, there is no need to describe a Turing machine. Decidability can be proved using any model of computation. In particular, you can use the "English" model of computation, in which you describe how to decide the problem in the English language (or in any other language). For example, you could say "Simulate $M$ on $w$, and if it ever uses more than $k$ space, immediately reject; otherwise, once $M$ halts, accept". (This is just your incorrect solution.)