What is the tips for construct invariant for simple program (like interview algorithm)?

I am always wondering how to prove the correctness of a simple program. For example, a interview problem like First Missing Positive. The program looks like this:

public class Solution{
    public int firstMissingPositive(int[] A){
        int i = 0;
        while(i < A.length){
            if(A[i] != (i+1) && A[i] >= 1 && A[i] <= A.length && A[A[i]-1] != A[i]){
                int tmp = A[A[i]-1];
                A[A[i]-1] = A[i];
                A[i] = tmp;
            }
            else{
                i++;
            }
        }
        for(i = 0; i < A.length; i++){
            if(A[i] != (i+1))
                retu i+1;
        }
        retu A.length+1;
    }
}

How to construct the invariant for this program? What is the general tips for construct the invariant for simple algorithm?