There are several classes of programs that can be proved to halt. Any non-recursive program without a loop halts. In addition to that, our research group in grad school showed that some looping programs can also be proved to halt as long as they are marked with loop termination clauses that can be proved to hold for the program in question. Look to Ohio State RSRG for more info.