Iterative Correctness

I missed a couple of lectures on iterative correctness and it took last week's test to get me up to speed. It is, as Danny had mentioned, definitely harder than recursive correctness. I found the use of induction here to be more traditional when compared with recursive correctness. Recursive programs are broken down into smaller parts and so we had to assume those smaller parts were true and then conclude that it implied the full size. But in iterative programs we use induction over 'i' which is each iteration of the loop and then prove a formula which is the loop invariant. So to me this seems much more like normal induction.
However, the hard part is actually figuring out what the loop invariant is. I seem to always have trouble with this unless it's a really simple program. The example that Danny showed in class about the counting down in base 7 bothers me even now. I don't think I'd have been able to figure out the loop invariant would be 7a instead of 6a.
Another thing I don't understand is the necessity to prove the termination of the program. The necessity to prove the termination of the loop itself is fine, so that it doesn't iterate infinitely. But if it's needed to prove the termination of the program in this case then why was it not necessary to do so in recursive correctness? Maybe it's simply because unless there is a loop then it's trivial to see that it will terminate, but formally speaking should we mention it in recursive correctness as well since if there is no base case then quite possibly that could recurse forever as well?