It seems like the proof that $A_{DFA}$ is decidable in Sipser (2nd ed.) assumes the computation will halt... and hence only really proves that $A_{DFA}$ is recognizable.
The language $A_{DFA}$ is defined by $A_{DFA} = \{\langle B, w \rangle \mid B \text{ is a } \mathsf{DFA} \text{ that accepts input string } w \}$.
Here is the passage (I've bolded the most relevant sentence):
First, let's examine the input $\langle B, w \rangle$. It is a representation of a $\mathsf{DFA}$ $B$ together with a string $w$. One reasonable representation of $B$ is simply a list of its five components, $Q$, $\Sigma$, $\delta$, $q_0$, and $F$. When $M$ receives its input, $M$ first determines whether it properly represents a $\mathsf{DFA}$ $B$ and a string $w$. If not, $M$ rejects.
Then $M$ carries out the simulation directly. It keeps track of $B$'s current state and $B$'s current position in the input $w$ by writing this information down on its tape. Initially, $B$'s current state is $q_0$ and $B$'s current input position is the leftmost symbol of $w$. The states and position are updated according to the specified transition function $\delta$. When $M$ finishes processing the last symbol of $w$, $M$ accepts the input if $B$ is in an accepting state; $M$ rejects the input if $B$ is in a nonaccepting state.
Am I missing something or is this proof bogus?
EDIT: Never mind, I think I see my problem. A Turing machine may move back and forth, never halting, but an automaton like $B$ given finite input $w$ finishes after $|w|$ steps, correct? So $M$ does halt. Feel free to post an answer explaining this yourself - I don't want anyone to miss out on a chance to answer by me deleting the question. If no one responds within a day, I'll post an answer myself.
