Teaching loop invariant choice
Let's start with the term "Loop Invariance". It is a property of a loop that is true before and after each iteration, thus in-variant, non-changing. So then, what is the purpose of the loop invariance in proving algorithm correctness? That is, it is a predicate about what the loop is supposed to do. Thus with proof by induction on this predicate shows the correctness of this algorithm. I know this is still very theory heavy so let's break this down even more.

A simple insertion sort. The purpose of insertion sort is to sort an array. Therefore the loop invariance would be that after each i-th iteration, the array is sorted up to the i-th element. The magic here is that instead of looking at the nested for i, j, loops of the algorithm you are choosing the loop invariance that contributes to the goal of the algorithm.

To answer (1). There is no sure guarenteed way to choose the correct loop invariance unless you are very experienced in algorithm correctness through countless examples. The best approach is to choose the segment of code that is actually doing what the algorithm is trying to do. Such as the example above, sorted up to the i-th element.

(2). I believe this has to do with the proof itself, rather than understanding the loop invariance. Structurally, to prove that the algorithm is correct, you would have to use proof by induction (either simple, or complete) to pove the loop-invariance and the fact that the algorithm actually terminates. Usually proof of termination is a 1 liner, such as when i > array.length, loop will terminate.


  simply to look at the final item you are trying to prove, and figure out what property of the loop will mimic that statement.


I can tell you are very intelligent as this is something only someone who truly understands algorithms and proof of correctness can say. It is actually very difficult for younger students to see this as they are tunnel-visioned by the actual loops in the code instead of the bigger picture. Instead, I think what you are trying to convey is to look for "what part of the code is doing what the algorithm is meant to do"