Loop invariants are simply the desired property in your iterations that you would want to maintain throughout the execution.
You could use this to prove program correctness. That is if you started off with a "correct state" and maintained it throughout the course of algorithm(invariant), then you know that you have a correct algorithm.
So you would need to show that you have a desired property, the invariance, in 3 steps:
i. Initialization: Can you show that you have the invariant property of the algorithm in the first step of the iteration of the loop?
ii. Maintenance: Are you maintaining the invariance? If it was true for the iteration up to that point, is it true for the next iteration?
iii.Termination: When your loop finally terminates, the invariant will be used to show that the algorithm you wrote is correct.
Let us take an example to prove that the algorithm below is correct. OR how do we know that building of max heap actually builds a max heap!
heap-size[A] = length[A]
for i : length[A]/2 to 1
Following our above intuition, we need to decide on a desired property that we maintain throughout the algorithm. What is the desired property in the MaxHeap? heap[i]>= heap[i*2]. No matter how much you mess around with the heap, if it still has that property, then it is a MaxHeap, right?
Initialization : Prior to the first iteration. Everything is a leaf so it is already a heap.
Maintainence : Let us assume that we have a working solution till now. The children of node i are numbered higher than i. MaxHeapify preserves the loop invariant as well. We maintain the invariance at each step.
Termination : Terminates when the i drops down to 0 and by the loop invariant, each node is the root of a max-heap.
Hence the algorithm you wrote is correct.
The basic idea is to figure out what is it that you want to achieve by maintaining the invariance and prove it in 3 steps.